proposition: Lemma CompileWordList_push_spec : forall vtmp vhd vlst fpointer (env: Env QsADTs.ADTValue) ext tenv h (t: list W), GLabelMap.MapsTo fpointer (Axiomatic QsADTs.WordListADTSpec.Push) env -> PreconditionSet tenv ext [[[vtmp;vhd;vlst]]] -> {{ [[ NTSome (H := WrapInstance (H := QS_WrapWordList)) vlst ->> t as _ ]] :: [[ `vhd ->> h as _ ]] :: tenv }} Call vtmp fpointer (vlst :: vhd :: nil) {{ [[ NTSome (H := WrapInstance (H := QS_WrapWordList)) vlst ->> h :: t as _ ]] :: tenv }} ∪ {{ ext }} // env.
proof: Proof. intros. apply ProgOk_Remove_Skip_R. hoare. PreconditionSet_t. apply generalized CompileWordList_push; repeat (compile_do_side_conditions || Lifted_t). apply CompileDeallocW_discretely; try compile_do_side_conditions; apply ProgOk_Chomp_Some; try compile_do_side_conditions; intros. move_to_front vhd; apply CompileDeallocW_discretely; try compile_do_side_conditions; apply ProgOk_Chomp_Some; try compile_do_side_conditions; intros. apply CompileSkip. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core