proposition: Corollary encode_Word_decode_correct {P : CacheDecode -> Prop} (P_OK : cache_inv_Property P (fun P => forall b cd, P cd -> P (addD cd b))) : CorrectDecoder monoid (fun _ => True) (fun _ => True) eq (fun w ctx => ret (serialize w ctx)) decode_word P (fun w ctx => ret (serialize w ctx)).
proof: Proof. unfold CorrectDecoder; split; intros. - eapply Word_decode_correct; eauto. - eapply Word_decode_correct in H1; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.BaseFormats