proposition: Lemma CompileMap_TuplesToWords : forall {N} (lst: list (FiatWTuple N)) vhead vhead' vtest vlst vret vtmp fpop fempty falloc fdealloc fcons facadeBody facadeCoda env (ext: StringMap.t (Value QsADTs.ADTValue)) tenv tenv' (f: FiatWTuple N -> W), GLabelMap.MapsTo fpop (Axiomatic (Pop)) env -> GLabelMap.MapsTo fempty (Axiomatic (Empty)) env -> GLabelMap.MapsTo falloc (Axiomatic (QsADTs.WordListADTSpec.New)) env -> GLabelMap.MapsTo fdealloc (Axiomatic (Delete)) env -> GLabelMap.MapsTo fcons (Axiomatic (QsADTs.WordListADTSpec.Push)) env -> PreconditionSet tenv ext [[[vhead; vhead'; vtest; vlst; vret; vtmp]]] -> BinNat.N.lt (BinNat.N.of_nat N) (Word.Npow2 32) -> {{ [[NTSome (H := WrapInstance (H := QS_WrapWordList)) vret ->> (revmap f lst) as _]] :: tenv }} facadeCoda {{ [[NTSome (H := WrapInstance (H := QS_WrapWordList)) vret ->> (revmap f lst) as _]] :: tenv' }} ∪ {{ ext }} // env -> (forall head (s: list (FiatWTuple N)) (s': list W), {{ [[`vhead ->> head as _]] :: tenv }} facadeBody {{ [[`vhead' ->> f head as _]] :: tenv }} ∪ {{ [vret |> wrap (FacadeWrapper := WrapInstance (H := QS_WrapWordList)) s'] :: [vtest |> wrap (bool2w false)] :: [vlst |> wrap s] :: ext }} // env) -> {{ [[`vlst ->> lst as _]] :: tenv }} (Seq (Call vret falloc nil) (Seq (Seq (Fold vhead vtest vlst fpop fempty (Seq facadeBody (Call vtmp fcons (vret :: vhead' :: nil)))) (Call vtest fdealloc (vlst :: nil))) facadeCoda)) {{ [[NTSome (H := WrapInstance (H := QS_WrapWordList)) vret ->> (revmap f lst) as _]] :: tenv' }} ∪ {{ ext }} // env.
proof: Proof. intros. setoid_rewrite <- revmap_fold_comp. apply CompileLoopalloc; eauto. PreconditionSet_t; eauto. eapply CompileWordList_new; compile_do_side_conditions. setoid_rewrite revmap_fold_comp; eassumption. intros. rewrite SameValues_Fiat_Bind_TelEq. move_to_front vret. apply miniChomp'; intros. hoare. apply ProgOk_Chomp_Some; loop_t; defunctionalize_evar; eauto. apply CompileWordList_push_spec; try compile_do_side_conditions. Qed.
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