proposition: Lemma CompileCallListSCALength {A}: forall {WrpList: FacadeWrapper (Value ADTValue) (BoundedList A (pow2 8))} (vlst varg : string) (tenv : Telescope ADTValue) (ext : StringMap.t (Value ADTValue)) env (lst : BoundedList A (pow2 8)) fLength tenv', PreconditionSet tenv' ext [[[vlst;varg]]] -> (exists sk: _ -> list W, (forall ls: BoundedList A (pow2 8), wrap ls = ADT (WordList (sk ls))) /\ (forall ls: BoundedList A (pow2 8), List.length (sk ls) = List.length (`ls))) -> GLabelMap.MapsTo fLength (Axiomatic WordListADTSpec.Length) env -> TelEq ext tenv ([[`vlst ->> lst as _]]::tenv') -> {{ tenv }} Call varg fLength [vlst] {{ [[ ` varg ->> BoundedListLength lst as _]]::tenv }} ∪ {{ ext }} // env.
proof: Proof. intros * ? ? (? & wrap_eq & length_eq) ? Heq; setoid_rewrite Heq; PreconditionSet_t; repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t || rewrite wrap_eq in *). facade_eauto. facade_eauto. repeat match goal with | [ H: ?a = ?a |- _ ] => clear dependent H | [ H: ADT (WordList (_ _)) = ADT _ |- _ ] => inversion' H end; rewrite length_eq; reflexivity. facade_eauto. rewrite remove_remove_comm by assumption; facade_eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat 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 Bedrock.Platform.Facade.examples.QsADTs