proposition: Lemma ByteAlign_Decode_w_Measure_le {A} : forall (dec_a : ByteString -> CacheDecode -> option (A * ByteString * CacheDecode)) (n m : nat) (dec_a' : Vector.t (word 8) (m + (n - m)) -> A) (cd : CacheDecode) (f : CacheDecode -> CacheDecode) (b : Vector.t (word 8) n) decode_a_le (dec_fail : ~ (m <= n)%nat -> forall b cd, dec_a (build_aligned_ByteString (numBytes := n) b) cd = None), (forall b cd, dec_a (build_aligned_ByteString b) cd = Some (dec_a' b, build_aligned_ByteString (snd (Vector_split m (n - m) b)), f cd)) -> Decode_w_Measure_le dec_a (build_aligned_ByteString b) cd decode_a_le = match Compare_dec.le_dec m n with | left e => (Let a := dec_a' (Guarded_Vector_split m n b) in Some (a, le_B_Guarded_Vector_split b m, f cd)) | right _ => None end.
proof: Proof. intros. destruct (Compare_dec.le_dec m n). assert (m + (n - m) = n) by omega. assert (forall b, Decode_w_Measure_le dec_a (build_aligned_ByteString b) cd decode_a_le = Decode_w_Measure_le dec_a (build_aligned_ByteString ( eq_rect _ _ (Guarded_Vector_split m n b) _ H0)) cd decode_a_le). { revert l; clear; intros. destruct (Decode_w_Measure_le dec_a (build_aligned_ByteString b) cd decode_a_le) as [ [ [? [? ?] ] ?] | ] eqn: ?. apply Decode_w_Measure_le_eq' in Heqo. simpl in Heqo. destruct (Decode_w_Measure_le dec_a _ cd decode_a_le) as [ [ [? [? ?] ] ?] | ] eqn: ?. apply Decode_w_Measure_le_eq' in Heqo0. simpl in *. rewrite <- build_aligned_ByteString_eq_split in Heqo0 by eauto. rewrite Heqo0 in Heqo. injection Heqo; intros. rewrite H, H2; repeat f_equal. revert l0 l1. rewrite H1; intros; f_equal. f_equal; apply Core.le_uniqueness_proof. apply ByteString_id. eapply Decode_w_Measure_le_eq'' in Heqo0. rewrite <- build_aligned_ByteString_eq_split in Heqo0 by eauto. rewrite Heqo0 in Heqo. discriminate. apply ByteString_id. erewrite build_aligned_ByteString_eq_split in Heqo by eauto. rewrite Heqo; reflexivity. } rewrite H1. match goal with |- ?a = _ => destruct a as [ [ [? ?] ? ] | ] eqn: ? end. eapply Decode_w_Measure_le_eq' in Heqo. assert (dec_a (build_aligned_ByteString (Guarded_Vector_split m n b)) cd = Some (a, proj1_sig s, c)). { destruct s; simpl in *. rewrite <- Heqo. unfold build_aligned_ByteString; repeat f_equal; simpl. eapply ByteString_f_equal; simpl. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := sym_eq H0). clear H1. destruct H0; reflexivity. } rewrite H in H2; injection H2; intros. rewrite H3, H5; unfold LetIn; simpl. repeat f_equal. destruct s; simpl in *. unfold le_B_Guarded_Vector_split; simpl. clear H1; revert l0. rewrite <- H4; intros. f_equal; apply Core.le_uniqueness_proof. apply ByteString_id. apply Decode_w_Measure_le_eq'' in Heqo. pose proof (H (Guarded_Vector_split m n b) cd). assert (Some (dec_a' (Guarded_Vector_split m n b), build_aligned_ByteString (snd (Vector_split m (n - m) (Guarded_Vector_split m n b))), f cd) = None). { rewrite <- Heqo. rewrite <- H. repeat f_equal. eapply ByteString_f_equal; simpl. instantiate (1 := eq_refl _); reflexivity. instantiate (1 := sym_eq H0). clear H1. destruct H0; reflexivity. } discriminate. eapply dec_fail in n0; simpl. eapply Specs.Decode_w_Measure_le_eq' in n0. apply n0. 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