proposition: Lemma CompileDelete_spec: forall (vtmp vtup vsize : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (tenv: Telescope QsADTs.ADTValue) ext N (fpointer : GLabelMap.key) (tup : FiatTuple N), vtup <> vtmp -> vtup <> vsize -> vsize <> vtmp -> vtmp ∉ ext -> vtup ∉ ext -> vsize ∉ ext -> NotInTelescope vtmp tenv -> NotInTelescope vtup tenv -> NotInTelescope vsize tenv -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> GLabelMap.MapsTo fpointer (Axiomatic Delete) env -> {{ [[ (NTSome (H := WrapInstance (H := FiatWrapper)) vtup) ->> tup as _]] :: tenv }} (Seq (Assign vsize (Const (Word.natToWord 32 N))) (Call vtmp fpointer (vtup :: vsize :: nil))) {{ tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. apply ProgOk_Remove_Skip_R; hoare. hoare. apply CompileConstant; try compile_do_side_conditions. apply CompileDeallocW_discretely; try compile_do_side_conditions. apply ProgOk_Chomp_Some; try compile_do_side_conditions; intros; computes_to_inv; subst; simpl. apply generalized CompileDelete; try (compile_do_side_conditions || Lifted_t). apply Lifted_MapsTo_Ext; compile_do_side_conditions. repeat match goal with | [ H: NotInTelescope _ _ |- _ ] => setoid_rewrite (DropName_NotInTelescope _ _ H) | _ => setoid_rewrite Propagate_anonymous_ret end. apply CompileDeallocW_discretely; try compile_do_side_conditions. apply CompileSkip. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core