proposition: Lemma CompileCallWrite8_base capacity : let Wrp := WrapInstance (H := @WrapListByte capacity) in forall (vtmp varg vstream : string) (stream : list byte) (n : byte) fWrite8 tenv ext env, (List.length stream + 1 <= wordToNat capacity)%nat -> GLabelMap.MapsTo fWrite8 (Axiomatic BytesADTSpec.Push) env -> Lifted_MapsTo ext tenv vstream (wrap (FacadeWrapper := Wrp) stream) -> Lifted_MapsTo ext tenv varg (wrap n) -> vtmp <> vstream -> vtmp ∉ ext -> vstream ∉ ext -> Lifted_not_mapsto_adt ext tenv vtmp -> {{ tenv }} Call vtmp fWrite8 (vstream :: varg :: nil) {{ [[ `vtmp ->> (Word.natToWord 32 0) as _ ]] :: [[ NTSome (H := Wrp) vstream ->> stream ++ n :: nil as _ ]] :: DropName vstream (DropName vtmp tenv) }} ∪ {{ ext }} // env.
proof: Proof. intros. repeat match goal with | _ => progress (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t) | [ |- context[IL.BtoW ?x] ] => rewrite (IL_BtoW_BtoW x) | [ H: context[IL.BtoW ?x] |- _ ] => rewrite (IL_BtoW_BtoW x) in H | [ H: BtoW _ = BtoW _ |- _ ] => learn (BtoW_inj _ _ H); subst end. facade_eauto. facade_eauto. repeat apply DropName_remove; facade_eauto. Qed.
imports: Fiat.CertifiedExtraction.Extraction.Extraction Fiat.CertifiedExtraction.Extraction.BinEncoders.Basics Fiat.CertifiedExtraction.Extraction.BinEncoders.Wrappers Fiat.CertifiedExtraction.Extraction.BinEncoders.Properties Coq.Program.Program Coq.Lists.List