proposition: Lemma CompileDeleteAny_spec: forall {N} (vtmp vtmp2 vsize vtest vlst vhead : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (tenv: Telescope QsADTs.ADTValue) ext (fpop fempty fdealloc ftdealloc : GLabelMap.key) (seq: (list (FiatWTuple N))), PreconditionSet tenv ext [[[vtmp; vtmp2; vsize; vhead; vtest; vlst]]] -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> GLabelMap.MapsTo fpop (Axiomatic (Pop)) env -> GLabelMap.MapsTo fempty (Axiomatic (Empty)) env -> GLabelMap.MapsTo fdealloc (Axiomatic (Delete)) env -> GLabelMap.MapsTo ftdealloc (Axiomatic (WTupleADTSpec.Delete)) env -> {{ [[ `vlst ->> seq as _]] :: tenv }} (Seq (Assign vtmp (Const (Word.natToWord 32 0))) (Seq (Seq (Fold vhead vtest vlst fpop fempty (Seq (Assign vsize (Const (Word.natToWord 32 N))) (Call vtmp2 ftdealloc [[[vhead; vsize]]]))) (Call (DummyArgument vtest) fdealloc [[[vlst]]])) Skip)) {{ tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. apply ProgOk_Remove_Skip_R. apply CompileSeq with ([[ ` vtmp ->> fold_left (fun acc x => acc) seq (Word.natToWord 32 0) as _]]::tenv). eapply (CompileLoopalloc_ret (vhead := vhead) (vtest := vtest)); try compile_do_side_conditions. apply CompileConstant; try compile_do_side_conditions. intros. apply ProgOk_Chomp_Some; try compile_do_side_conditions; intros. apply (WTupleCompilation.CompileDelete_spec (vtmp := vtmp2) (vsize := vsize)); try compile_do_side_conditions. apply CompileSkip. apply CompileDeallocW_discretely; try compile_do_side_conditions. apply CompileSkip. Defined.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core CertifiedExtraction.Extraction.External.Loops CertifiedExtraction.Extraction.External.FacadeLoops CertifiedExtraction.Extraction.External.Lists CertifiedExtraction.Extraction.QueryStructures.CallRules.Tuple GLabelMapFacts Fiat.CertifiedExtraction.Extraction.QueryStructures.CallRules.WordList CertifiedExtraction.Extraction.QueryStructures.CallRules.Tuple