proposition: Lemma CompileCallAllocString {real_capacity}: forall (vcapacity vstream : string) (tenv tenv' : Telescope ADTValue) ext (env : GLabelMap.t (FuncSpec ADTValue)) capacity, let Wrp := WrapInstance (H := (@WrapListByte real_capacity)) in forall pNext pArg fAllocString, vcapacity <> vstream -> vstream ∉ ext -> NotInTelescope vstream tenv -> IL.goodSize (2 + Word.wordToNat capacity * 4) -> real_capacity = Word.wmult capacity (Word.natToWord 32 4) -> GLabelMap.MapsTo fAllocString (Axiomatic BytesADTSpec.New) env -> {{ [[ NTSome (H := Wrp) vstream ->> nil as _]]::tenv }} pNext {{ [[ NTSome (H := Wrp) vstream ->> nil as _]]::tenv' }} ∪ {{ ext }} // env -> {{ tenv }} pArg {{ [[ ` vcapacity ->> capacity as _ ]] :: tenv }} ∪ {{ ext }} // env -> {{ tenv }} Seq (Seq pArg (Call vstream fAllocString [vcapacity])) pNext {{ [[ NTSome (H := Wrp) vstream ->> nil as _]]::tenv' }} ∪ {{ ext }} // env.
proof: Proof. hoare; hoare; hoare. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t). facade_eauto. facade_eauto. congruence. facade_eauto. 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