proposition: Theorem bool_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_bool decode_bool P format_bool.
proof: Proof. eapply format_decode_correct_EquivFormatAndView with (fun b => format_word (WS b WO)). unfold flip, EquivFormat. reflexivity. apply_bijection_rule with (whd (sz:=_)); intuition eauto using Word_decode_correct. rewrite <- (natToWord_wordToNat v). destruct (wordToNat v) eqn:?; reflexivity. unfold decode_word, decode_word'; derive_decoder_equiv. Qed.
imports: Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.BaseFormats