proposition: Theorem Ascii_decode_correct {P : CacheDecode -> Prop} (P_OK : forall b cd, P cd -> P (addD cd b)) : CorrectDecoder monoid (fun n => True) (fun n => True) eq format_ascii decode_ascii P format_ascii.
proof: Proof. apply_bijection_rule with (fun n => ascii_of_N (wordToN n)); intuition eauto using Word_decode_correct. rewrite NToWord_nat, wordToN_nat, wordToNat_natToWord_idempotent, Nnat.N2Nat.id, ascii_N_embedding; eauto. rewrite Nnat.N2Nat.id. clear. assert (N.lt (N_of_ascii s) 256). induction s; repeat (match goal with | B : bool |- _ => destruct B end); simpl; unfold N.lt; eauto. eauto. rewrite N_ascii_embedding, NToWord_nat, wordToN_nat, Nnat.Nat2N.id, natToWord_wordToNat; eauto. rewrite wordToN_nat. eapply Nomega.Nlt_in. rewrite Nnat.Nat2N.id. apply wordToNat_bound. derive_decoder_equiv. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Bedrock.Word Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Numbers.BinNums Coq.NArith.BinNat