proposition: Lemma AlignedDecodeUnusedChars {C} {numBytes numBytes'} : forall (v : ByteBuffer.t (numBytes' + numBytes)) (k : _ -> option C) cd, BindOpt (decode_unused_word (monoidUnit := ByteString_QueueMonoidOpt) (sz := 8 * numBytes') (build_aligned_ByteString v) cd) k = k ((), build_aligned_ByteString (snd (Vector_split numBytes' _ v)), addD cd (8 * numBytes')).
proof: Proof. induction numBytes'. - Local Transparent Vector_split. simpl; intros; unfold Vector_split; simpl. reflexivity. - simpl. replace (8 * S numBytes') with (8 + 8 * numBytes') by omega. unfold decode_unused_word, WordOpt.decode_word, FMapFormat.Compose_Decode in *. unfold decode_unused_word; intros. rewrite decode_word_plus'. rewrite (@aligned_decode_char_eq ). simpl BindOpt. pose proof (IHnumBytes' (Vector.tl v) k (addD cd 8)). unfold Core.char. destruct (decode_word' (8 * numBytes') _) as [ [? ?] | ] eqn: ?; simpl in *; try discriminate. rewrite addD_addD_plus in H; simpl in H; rewrite H. fold plus. destruct ((Vector_split numBytes' numBytes _)) eqn: ?; simpl. reflexivity. rewrite addD_addD_plus in H; simpl in H; rewrite H. fold plus; destruct ((Vector_split numBytes' numBytes _)); simpl. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.QueryStructure.Specification.Representation.Notations Fiat.QueryStructure.Specification.Representation.Heading Fiat.QueryStructure.Specification.Representation.Tuple Fiat.Narcissus.BinLib.AlignedEncodeMonad Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Narcissus.BinLib.AlignedString Fiat.Narcissus.BinLib.AlignedDecodeMonad Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.WordOpt Fiat.Narcissus.Formats.NatOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.DomainNameOpt Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.Narcissus.Formats.IPChecksum Fiat.Narcissus.Common.ComposeCheckSum Bedrock.Word