proposition: Lemma CompileNew : forall vret vsize fpointer (env: Env ADTValue) ext tenv N, GLabelMap.find fpointer env = Some (Axiomatic WBagOfTuples0ADTSpec.New) -> Lifted_MapsTo ext tenv vsize (wrap (Word.natToWord 32 N)) -> Lifted_not_mapsto_adt ext (tenv: Telescope ADTValue) vret -> vret ∉ ext -> ~ Word.wlt (Word.natToWord 32 N) (Word.natToWord 32 2) -> {{ tenv }} Call vret fpointer (vsize :: nil) {{ [[ `vret ->> FiatWBagEmpty N as _ ]] :: DropName vret tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. apply generalized CompileNew_helper; try eassumption. eapply TelEq_chomp_head_heterogeneous; repeat unfold wrap, WrapInstance, FiatWrapper, FacadeWrapper_Self, WBagOfTuples0ADTSpecParams.FieldType; try erewrite Empty_lift; reflexivity. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core