fact: Definition decode_obliviously {S T} {cache : Cache} {monoid : Monoid T} (decode : DecodeM (S * T) T) : T -> CacheDecode -> option (S * CacheDecode) := fun bs cd => option_map (fun abc => (fst (fst abc), snd abc)) (decode bs cd).
imports: Coq.Lists.List Fiat.Common Fiat.Computation.Core Fiat.Computation.Notations Fiat.Narcissus.Common.Notations Fiat.Narcissus.Common.Monoid Fiat.Narcissus.Stores.Cache