proposition: Lemma CompileNew : forall vret vsize vkey1 vkey2 fpointer (env: Env ADTValue) ext tenv N (k1 k2: W), GLabelMap.find fpointer env = Some (Axiomatic New) -> Lifted_MapsTo ext tenv vsize (wrap (Word.natToWord 32 N)) -> Lifted_MapsTo ext tenv vkey1 (wrap k1) -> Lifted_MapsTo ext tenv vkey2 (wrap k2) -> Lifted_not_mapsto_adt ext tenv vret -> vret ∉ ext -> Word.wlt k1 (Word.natToWord 32 N) -> Word.wlt k2 (Word.natToWord 32 N) -> ~ Word.wlt (Word.natToWord 32 N) (Word.natToWord 32 2) -> {{ tenv }} Call vret fpointer (vsize :: vkey1 :: vkey2 :: nil) {{ [[ NTSomeBag k1 k2 vret ->> @FiatWBagEmpty N as _ ]] :: DropName vret tenv }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t). facade_eauto. unfold BagConstructor. repeat f_equal; facade_eauto. facade_eauto. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.FiatBedrockLemmas CertifiedExtraction.Extraction.QueryStructures.CallRules.Core