fact: Definition CorrectDecoder_id (monoid : Monoid T) (Source_Predicate : S -> Prop) (format : FormatM) (decode : T -> CacheDecode -> option (S * T * CacheDecode)) (decode_inv : CacheDecode -> Prop) := (forall env env' xenv s t ext (env_OK : decode_inv env'), Equiv env env' -> Source_Predicate s -> format s env ∋ (t, xenv) -> exists xenv', decode (mappend t ext) env' = Some (s, ext, xenv') /\ Equiv xenv xenv' /\ decode_inv xenv') /\ (forall env env' xenv' s t ext, Equiv env env' -> decode_inv env' -> decode t env' = Some (s, ext, xenv') -> decode_inv xenv' /\ exists t' xenv, (format s env ∋ (t', xenv)) /\ t = mappend t' ext /\ Source_Predicate s /\ Equiv xenv xenv').
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache