proposition: Theorem 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 format_word decode_word P format_word.
proof: Proof. unfold CorrectDecoder, format_word, decode_word; split. - intros env env' xenv w w' ext env_OK Eeq _ ?. computes_to_inv; injections. generalize dependent sz. intros; rewrite decode_encode_word'; simpl. eexists _, _; split; intuition eauto using add_correct. - intros. destruct (decode_word' sz t) as [ [? ?] | ] eqn: ?; simpl in *; try discriminate. injections. apply decode_encode_word'_Some in Heqo; subst. split; eauto using add_correct. eexists _, _; repeat split. eauto using add_correct. 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