proposition: Lemma CompileCallWrite8 capacity : let Wrp := WrapInstance (H := @WrapListByte capacity) in forall (vtmp varg vstream : string) (stream : list byte) (tenv tenv' tenv'': Telescope ADTValue) (n : byte) ext env pArg pNext fWrite8, (List.length stream + 1 <= wordToNat capacity)%nat -> PreconditionSet tenv' ext [[[vtmp; vstream; varg]]] -> GLabelMap.MapsTo fWrite8 (Axiomatic BytesADTSpec.Push) env -> {{ [[ NTSome (H := Wrp) vstream ->> stream as _]]::tenv }} pArg {{ [[ NTSome (H := Wrp) vstream ->> stream as _]]::[[ ` varg ->> n as _]]::tenv' }} ∪ {{ ext }} // env -> {{ [[ NTSome (H := Wrp) vstream ->> stream ++ n :: nil as _]]::tenv' }} pNext {{ [[ NTSome (H := Wrp) vstream ->> stream ++ n :: nil as _]]::tenv'' }} ∪ {{ ext }} // env -> {{ [[ NTSome (H := Wrp) vstream ->> stream as _]]::tenv }} Seq pArg (Seq (Call vtmp fWrite8 [vstream; varg]) pNext) {{ [[ NTSome (H := Wrp) vstream ->> stream ++ n :: nil as _]]::tenv'' }} ∪ {{ ext }} // env.
proof: Proof. hoare; hoare; hoare. PreconditionSet_t; apply ProgOk_Remove_Skip_R; hoare; [ apply generalized CompileCallWrite8_base | ]; repeat repeat match goal with | _ => progress intros | _ => apply ProgOk_Chomp_Some | _ => apply CompileDeallocSCA_discretely | _ => progress (compile_do_side_conditions || Lifted_t) end; (assumption || apply CompileSkip). 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