proposition: Theorem Enum_decode_correct (tb_OK : NoDupVector tb) {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_enum decode_enum P format_enum.
proof: Proof. apply_bijection_rule' with (fun w => word_indexed w tb); intuition eauto using Word_decode_correct. eapply word_indexed_correct in tb_OK. destruct word_indexed eqn:?; subst; intuition eauto. symmetry. eauto using word_indexed_correct'. derive_decoder_equiv; rewrite Heqo0; intuition eauto. Qed.
imports: Fiat.Common.BoundedLookup Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Coq.Vectors.Vector Bedrock.Word