proposition: Theorem Nat_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 n => n < pow2 sz) (fun n => n < pow2 sz) eq format_nat decode_nat P format_nat.
proof: Proof. apply_bijection_rule; intuition eauto using Word_decode_correct, wordToNat_bound, natToWord_wordToNat. apply wordToNat_natToWord_idempotent. apply Nomega.Nlt_in. rewrite Npow2_nat. rewrite Nnat.Nat2N.id. auto. derive_decoder_equiv. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.Narcissus.Common.Specs Fiat.Narcissus.BaseFormats Fiat.Narcissus.Formats.WordOpt Coq.ZArith.ZArith Bedrock.Word