proposition: Corollary AlignedFormatNat {numBytes} : forall (n : nat) ce ce' (c : _ -> Comp _) (v : Vector.t _ numBytes), refine (c (addE ce 8)) (ret (build_aligned_ByteString v, ce')) -> refine (((format_nat 8 (monoidUnit := ByteString_QueueMonoidOpt) n) ThenC c) ce) (ret (build_aligned_ByteString (Vector.cons _ (natToWord 8 n) _ v), ce')).
proof: Proof. unfold format_nat; cbv beta; intros. rewrite <- AlignedFormatChar; eauto. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Strings.Ascii Coq.Strings.String Coq.Numbers.BinNums Fiat.Common Fiat.Computation.Notations Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Bedrock.Word Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.Bool Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Stores.EmptyStore Fiat.Narcissus.Automation.Solver Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedDecoders