proposition: Lemma ByteString2ListOfChar_format_checksum (w : word 16) : let b := format_checksum _ _ _ _ w in ByteString2ListOfChar (bin_measure b) b = [hi8 w; lo8 w]%list.
proof: Proof. simpl. assert (refine (format_word w ()) (ret (build_aligned_ByteString ([hi8 w; lo8 w]), ()))). { etransitivity. Focus 2. pose proof AlignedFormat2Char. apply H; eauto. higher_order_reflexivity. autorewrite with monad laws. higher_order_reflexivity. } unfold format_word, format_checksum in *. simpl in *. apply refine_ret_ret_eq in H. injections. rewrite H0. rewrite ByteString2ListOfChar_eq'; eauto. Unshelve. simpl. exact (). Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.Vectors.Vector Coq.ZArith.ZArith Fiat.Common.SumType Fiat.Common.EnumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedList Fiat.Narcissus.BinLib.AlignedDecoders Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.WordFacts Fiat.Narcissus.Common.ComposeCheckSum Fiat.Narcissus.Common.ComposeIf Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats Fiat.Narcissus.BaseFormats Fiat.Narcissus.Stores.EmptyStore Bedrock.Word