proposition: Lemma aligned_decode_char_eq' {numBytes numBytes'} : forall (v : ByteBuffer.t (S numBytes' + numBytes)), WordOpt.decode_word' (monoidUnit := ByteString_QueueMonoidOpt) (8 * (S numBytes')) (build_aligned_ByteString v) = let (v', v'') := Vector_split (S numBytes') numBytes v in Some (VectorByteToWord v', build_aligned_ByteString v'').
proof: Proof. induction numBytes'. - intros; rewrite aligned_decode_char_eq. unfold Vector_split; simpl. repeat f_equal; generalize (Vector.hd v); intro; unfold char in c; shatter_word c. fold Nat.add. apply Eqdep_dec.eq_rect_eq_dec; eauto using Peano_dec.eq_nat_dec. - revert IHnumBytes'; generalize (S numBytes'); intros. match goal with |- ?k = _ => replace k with (`(w, v') <- Some (Vector.hd v, build_aligned_ByteString (Vector.tl v)); `(w', v'') <- WordOpt.decode_word' (8 * n) v'; Some (eq_rect _ word (Core.append_word w' w) _ (sym_eq (NPeano.Nat.mul_succ_r _ _)), v'')) end. simpl. rewrite IHnumBytes'; simpl. destruct (Vector_split n numBytes (Vector.tl v)); simpl; repeat f_equal; clear. unfold DecodeBindOpt at 1; unfold BindOpt, If_Opt_Then_Else. assert (8 + 8 * n = 8 * S n) by omega. rewrite <- eq_rect_decode_word with (H := H). assert (8 * n + 8 = 8 + 8 * n) by omega. match goal with |- context [decode_word' ?m (build_aligned_ByteString ?b) ] => replace (decode_word' m (build_aligned_ByteString b)) with (`(w, v') <- Some (hd b, build_aligned_ByteString (tl b)); `(w', v'') <- decode_word' (8 * n) v'; Some (eq_rect _ word (append_word w' w) _ H0, v'')) end. unfold DecodeBindOpt at 2; unfold BindOpt, If_Opt_Then_Else. destruct (decode_word' (8 * n) (build_aligned_ByteString (tl v))) as [ [? ?] | ]; try reflexivity. unfold DecodeBindOpt, If_Opt_Then_Else, BindOpt; simpl. rewrite Some_eq_rect_eq. rewrite <- transport_pp. repeat f_equal. apply Eqdep_dec.eq_proofs_unicity; try intros; omega. simpl; symmetry; apply None_eq_rect_eq. rewrite <- aligned_decode_char_eq. simpl. repeat (rewrite !DecodeBindOpt_assoc; simpl; apply DecodeBindOpt_under_bind; intros). clear. repeat f_equal. simpl in H0. revert a7 H0; generalize (n + (n + (n + (n + (n + (n + (n + (n + 0)))))))); clear; intros n0 w. induction w; simpl; intros. symmetry. apply Eqdep_dec.eq_rect_eq_dec; eauto using Peano_dec.eq_nat_dec. erewrite <- IHw; clear. erewrite WS_eq_rect_eq; reflexivity. Unshelve. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer Coq.Strings.String Coq.Vectors.Vector Fiat.Narcissus.Formats.WordOpt Fiat.Common.Equality