proposition: Lemma CompileDelete: 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 -> vtmp ∉ ext -> vtup ∉ ext -> Lifted_MapsTo ext tenv vtup (wrap (FacadeWrapper := WrapInstance (H := FiatWrapper)) tup) -> Lifted_MapsTo ext tenv vsize (wrap (Word.natToWord 32 N)) -> Lifted_not_mapsto_adt ext tenv vtmp -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> GLabelMap.MapsTo fpointer (Axiomatic Delete) env -> {{ tenv }} Call vtmp fpointer (vtup :: vsize :: nil) {{ [[`vtmp ->> (Word.natToWord 32 0) as _]] :: (DropName vtmp (DropName vtup tenv)) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t || PreconditionSet_t). autorewrite with call_helpers_db; facade_eauto. facade_eauto. repeat apply DropName_remove; eauto 1. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core