fact: Definition CorrectDecoder {V} (monoid : Monoid T) (Source_Predicate : S -> Prop) (View_Predicate : V -> Prop) (view : S -> V -> Prop) (format : FormatM) (decode : T -> CacheDecode -> option (V * T * CacheDecode)) (decode_inv : CacheDecode -> Prop) (view_format : V -> CacheFormat -> Comp (T * CacheFormat)) := (forall env env' xenv s t ext (env_OK : decode_inv env'), Equiv env env' -> Source_Predicate s -> format s env ∋ (t, xenv) -> exists v xenv', decode (mappend t ext) env' = Some (v, ext, xenv') /\ view s v /\ (view_format v env ∋ (t, xenv)) /\ Equiv xenv xenv' /\ decode_inv xenv') /\ (forall (env : CacheFormat) (env' xenv' : CacheDecode) (v : V) (t t' : T), Equiv env env' -> decode_inv env' -> decode t env' = Some (v, t', xenv') -> decode_inv xenv' /\ exists (t'' : T) (xenv : CacheFormat), (view_format v env ∋ (t'', xenv)) /\ t = mappend t'' t' /\ View_Predicate v /\ 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