proposition: Lemma decode_string_aligned_ByteString {sz sz'} : forall (b : t (word 8) (sz + sz')) (cd : CacheDecode), FixStringOpt.decode_string sz (build_aligned_ByteString b) cd = Some (BytesToString (fst (Vector_split sz sz' b)), build_aligned_ByteString (snd (Vector_split sz sz' b)), addD cd (8 * sz)).
proof: Proof. induction sz; intros. - simpl; repeat f_equal. - simpl. assert (forall A n b, exists a b', b = Vector.cons A a n b') by (clear; intros; pattern n, b; apply caseS; eauto). destruct (H _ _ b) as [? [? ?] ]; subst; simpl. unfold AsciiOpt.decode_ascii, DecodeBindOpt2. rewrite BindOpt_assoc; simpl. etransitivity. unfold BindOpt at 1. rewrite AlignedDecodeChar; simpl. rewrite IHsz. higher_order_reflexivity. simpl. destruct (Vector_split sz sz' x0); simpl. unfold LetIn. rewrite addD_addD_plus; repeat f_equal. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Strings.Ascii Coq.Strings.String Coq.Arith.Mult Coq.Vectors.Vector Fiat.Common.SumType Fiat.Common.BoundedLookup Fiat.Common.ilist Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Formats.FixStringOpt Fiat.Narcissus.Formats.StringOpt Fiat.Narcissus.Formats.EnumOpt Fiat.Narcissus.Formats.FixListOpt Fiat.Narcissus.Formats.SumTypeOpt Fiat.Narcissus.Formats.AsciiOpt Fiat.Narcissus.BinLib.AlignedByteString Fiat.Narcissus.BinLib.AlignWord Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Bedrock.Word