Require Import Ascii List. Require Import ListUtil Object MultiByte Util SerializeSpec Pow SerializedList ProofUtil. Open Scope char_scope. Definition compact (xs : list object) : list ascii8 := List.flat_map (fun x => match x with FixRaw xs => xs | _ => [] end) xs. Fixpoint deserialize (n : nat) (xs : list ascii8) {struct xs} := match n with | 0 => match xs with | "192" :: ys => Nil::deserialize 0 ys | "194" :: ys => Bool false :: deserialize 0 ys | "195" :: ys => Bool true :: deserialize 0 ys | Ascii b1 b2 b3 b4 b5 b6 b7 false :: ys => PFixnum (Ascii b1 b2 b3 b4 b5 b6 b7 false) :: deserialize 0 ys | (Ascii b1 b2 b3 b4 b5 true true true) :: ys => NFixnum (Ascii b1 b2 b3 b4 b5 true true true) :: deserialize 0 ys | "204" :: c1 :: ys => Uint8 c1 :: deserialize 0 ys | "205" :: c1 :: c2 :: ys => Uint16 (c1, c2) :: deserialize 0 ys | "206" :: c1 :: c2 :: c3 :: c4 :: ys => Uint32 ((c1, c2), (c3, c4)) :: deserialize 0 ys | "207" :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: ys => Uint64 (((c1, c2), (c3, c4)), ((c5, c6), (c7, c8))) :: deserialize 0 ys | "208" :: c1 :: ys => Int8 c1 :: deserialize 0 ys | "209" :: c1 :: c2 :: ys => Int16 (c1, c2) :: deserialize 0 ys | "210" :: c1 :: c2 :: c3 :: c4 :: ys => Int32 ((c1, c2), (c3, c4)) :: deserialize 0 ys | "211" :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: ys => Int64 (((c1, c2), (c3, c4)), ((c5, c6), (c7, c8))) :: deserialize 0 ys | "202" :: c1 :: c2 :: c3 :: c4 :: ys => Float ((c1,c2), (c3, c4)) :: deserialize 0 ys | "203" :: c1 :: c2 :: c3 :: c4 :: c5 :: c6 :: c7 :: c8 :: ys => Double (((c1, c2), (c3, c4)), ((c5, c6), (c7, c8))) :: deserialize 0 ys | Ascii b1 b2 b3 b4 b5 true false true :: ys => let n := nat_of_ascii8 (Ascii b1 b2 b3 b4 b5 false false false) in let (zs, ws) := split_at n @@ deserialize n ys in FixRaw (compact zs) :: ws | "218" :: s1 :: s2 :: ys => let n := nat_of_ascii16 (s1,s2) in let (zs, ws) := split_at n @@ deserialize n ys in Raw16 (compact zs) :: ws | "219" :: s1 :: s2 :: s3 :: s4 :: ys => let n := nat_of_ascii32 ((s1,s2),(s3,s4)) in let (zs, ws) := split_at n @@ deserialize n ys in Raw32 (compact zs) :: ws | Ascii b1 b2 b3 b4 true false false true :: ys => let n := nat_of_ascii8 (Ascii b1 b2 b3 b4 false false false false) in let (zs, ws) := split_at n @@ deserialize 0 ys in FixArray zs :: ws | "220" :: s1 :: s2 :: ys => let n := nat_of_ascii16 (s1,s2) in let (zs, ws) := split_at n @@ deserialize 0 ys in Array16 zs :: ws | "221" :: s1 :: s2 :: s3 :: s4 :: ys => let n := nat_of_ascii32 ((s1, s2), (s3, s4)) in let (zs, ws) := split_at n @@ deserialize 0 ys in Array32 zs :: ws | Ascii b1 b2 b3 b4 false false false true :: ys => let n := nat_of_ascii8 (Ascii b1 b2 b3 b4 false false false false) in let (zs, ws) := split_at (2 * n) @@ deserialize 0 ys in FixMap (pair zs) :: ws | "222" :: s1 :: s2 :: ys => let n := nat_of_ascii16 (s1,s2) in let (zs, ws) := split_at (2 * n) @@ deserialize 0 ys in Map16 (pair zs) :: ws | "223" :: s1 :: s2 :: s3 :: s4 :: ys => let n := nat_of_ascii32 ((s1, s2), (s3, s4)) in let (zs, ws) := split_at (2 * n) @@ deserialize 0 ys in Map32 (pair zs) :: ws | _ => [] end | S m => match xs with | y::ys => FixRaw [ y ]::deserialize m ys | _ => [] end end. Definition DeserializeCorrect os bs := SerializedList os bs -> deserialize 0 bs = os. Lemma correct_bot : DeserializeCorrect [] []. Proof with auto. unfold DeserializeCorrect... Qed. Lemma correct_nil : forall os bs, DeserializeCorrect os bs -> DeserializeCorrect (Nil :: os) ("192"::bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H0. apply H in H3. rewrite <- H3... Qed. Lemma correct_false: forall os bs, DeserializeCorrect os bs -> DeserializeCorrect ((Bool false) :: os) ("194"::bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H0. apply H in H3. rewrite <- H3... Qed. Lemma correct_true: forall os bs, DeserializeCorrect os bs -> DeserializeCorrect ((Bool true) :: os) ("195"::bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H0. apply H in H3. rewrite <- H3... Qed. Lemma correct_pfixnum: forall os bs x1 x2 x3 x4 x5 x6 x7, DeserializeCorrect os bs -> DeserializeCorrect ((PFixnum (Ascii x1 x2 x3 x4 x5 x6 x7 false))::os) ((Ascii x1 x2 x3 x4 x5 x6 x7 false)::bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H0. apply H in H2. rewrite <- H2. destruct x1,x2,x3,x4,x5,x6,x7; reflexivity. Qed. Lemma correct_nfixnum: forall os bs x1 x2 x3 x4 x5, DeserializeCorrect os bs -> DeserializeCorrect ((NFixnum (Ascii x1 x2 x3 x4 x5 true true true))::os) ((Ascii x1 x2 x3 x4 x5 true true true)::bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H0. apply H in H2. rewrite <- H2. destruct x1,x2,x3,x4,x5; reflexivity. Qed. Lemma correct_uint8 : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Uint8 c)::os) ("204"::list_of_ascii8 c ++ bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H0. apply H in H2. rewrite <- H2... Qed. Lemma correct_uint16 : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Uint16 c)::os) ("205"::list_of_ascii16 c ++ bs). Proof with auto. unfold DeserializeCorrect. intros. destruct c. inversion H0. apply H in H2. rewrite <- H2... Qed. Lemma correct_uint32 : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Uint32 c)::os) ("206"::list_of_ascii32 c ++ bs). Proof with auto. unfold DeserializeCorrect. intros. destruct c. destruct a, a0. inversion H0. apply H in H2. rewrite <- H2... Qed. Lemma correct_uint64 : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Uint64 c)::os) ("207"::list_of_ascii64 c ++ bs). Proof with auto. unfold DeserializeCorrect. intros. destruct c. destruct a, a0. destruct a, a0, a1, a2. inversion H0. apply H in H2. rewrite <- H2... Qed. Lemma correct_int8 : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Int8 c)::os) ("208"::list_of_ascii8 c ++ bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H0. apply H in H2. rewrite <- H2... Qed. Lemma correct_int16 : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Int16 c)::os) ("209"::list_of_ascii16 c ++ bs). Proof with auto. unfold DeserializeCorrect. intros. destruct c. inversion H0. apply H in H2. rewrite <- H2... Qed. Lemma correct_int32 : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Int32 c)::os) ("210"::list_of_ascii32 c ++ bs). Proof with auto. unfold DeserializeCorrect. intros. destruct c. destruct a, a0. inversion H0. apply H in H2. rewrite <- H2... Qed. Lemma correct_int64 : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Int64 c)::os) ("211"::list_of_ascii64 c ++ bs). Proof. unfold DeserializeCorrect. intros. destruct c. destruct a, a0. destruct a, a0, a1, a2. inversion H0. apply H in H2. rewrite <- H2. reflexivity. Qed. Lemma correct_float : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Float c)::os) ("202"::list_of_ascii32 c ++ bs). Proof. unfold DeserializeCorrect. intros. destruct c. destruct a, a0. inversion H0. apply H in H2. rewrite <- H2. reflexivity. Qed. Lemma correct_double : forall os bs c, DeserializeCorrect os bs -> DeserializeCorrect ((Double c)::os) ("203"::list_of_ascii64 c ++ bs). Proof. unfold DeserializeCorrect. intros. destruct c. destruct a, a0. destruct a, a0, a1, a2. inversion H0. apply H in H2. rewrite <- H2. reflexivity. Qed. Lemma deserialize_take_length: forall xs ys, take (List.length xs) (deserialize (List.length xs) (xs ++ ys)) = List.map (fun x => FixRaw [ x ]) xs. Proof with auto. induction xs; [ reflexivity | intros ]. simpl. rewrite IHxs... Qed. Lemma deserialize_drop_length: forall xs ys, drop (List.length xs) (deserialize (List.length xs) (xs ++ ys)) = deserialize 0 ys. Proof with auto. induction xs; [ reflexivity | intros ]. simpl. rewrite IHxs... Qed. Lemma compact_eq : forall xs, compact (List.map (fun x => FixRaw [ x ]) xs) = xs. Proof with auto. induction xs; [ reflexivity | intros ]. simpl. rewrite IHxs... Qed. Lemma correct_fixraw: forall os bs cs b1 b2 b3 b4 b5, DeserializeCorrect os bs -> Ascii b1 b2 b3 b4 b5 false false false = ascii8_of_nat (List.length cs) -> List.length cs < pow 5 -> DeserializeCorrect (FixRaw cs :: os) ((Ascii b1 b2 b3 b4 b5 true false true) :: cs ++ bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H2. assert (bs0 = bs); [| rewrite_for bs0 ]. apply app_same in H11... apply H in H13. assert (length cs < pow 8). transitivity (pow 5); auto. apply pow_lt... destruct b1,b2,b3,b4,b5; ((replace (deserialize 0 _ ) with (let n := nat_of_ascii8 (ascii8_of_nat (length cs)) in let (zs, ws) := split_at n @@ deserialize n (cs++bs) in FixRaw (compact zs) :: ws)); [ unfold atat, split_at; rewrite nat_ascii8_embedding, deserialize_take_length, deserialize_drop_length, compact_eq, <- H13 | rewrite <- H7])... Qed. Lemma correct_raw16: forall os bs cs s1 s2, DeserializeCorrect os bs -> (s1, s2) = ascii16_of_nat (List.length cs) -> List.length cs < pow 16 -> DeserializeCorrect (Raw16 cs :: os) ("218" :: s1 :: s2 :: cs ++ bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H2. assert (bs0 = bs); [| rewrite_for bs0 ]. apply app_same in H8... apply H in H10. change (deserialize 0 _ ) with (let (zs, ws) := split_at (nat_of_ascii16 (s1,s2)) @@ deserialize (nat_of_ascii16 (s1,s2)) (cs++bs) in Raw16 (compact zs) :: ws). unfold atat, split_at. rewrite H7, nat_ascii16_embedding, deserialize_take_length, deserialize_drop_length, compact_eq, H10... Qed. Lemma correct_raw32: forall os bs cs s1 s2 s3 s4, DeserializeCorrect os bs -> ((s1, s2), (s3, s4)) = ascii32_of_nat (List.length cs) -> List.length cs < pow 32 -> DeserializeCorrect (Raw32 cs :: os) ("219" :: s1 :: s2 :: s3 :: s4 :: cs ++ bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H2. assert (bs0 = bs); [| rewrite_for bs0 ]. apply app_same in H10... apply H in H12. change (deserialize 0 _ ) with (let (zs, ws) := split_at (nat_of_ascii32 ((s1,s2),(s3,s4))) @@ deserialize (nat_of_ascii32 ((s1,s2),(s3,s4))) (cs++bs) in Raw32 (compact zs) :: ws). unfold atat, split_at. rewrite H7, nat_ascii32_embedding, deserialize_take_length, deserialize_drop_length, compact_eq, H12... Qed. Lemma correct_fixarray : forall os bs n xs ys b1 b2 b3 b4, DeserializeCorrect os bs -> (xs, ys) = split_at n os -> n < pow 4 -> Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat n -> DeserializeCorrect (FixArray xs :: ys) (Ascii b1 b2 b3 b4 true false false true :: bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H3. assert (os = os0); [| rewrite_for os0 ]. apply split_at_soundness in H0. apply split_at_soundness in H12. rewrite H0, H12... apply H in H9. assert (n0 < pow 8). transitivity (pow 4); auto. apply pow_lt... destruct b1, b2, b3, b4; (replace (deserialize 0 (_ :: bs)) with (let (zs, ws) := split_at (nat_of_ascii8 (ascii8_of_nat n0)) @@ deserialize 0 bs in FixArray zs :: ws); [ unfold atat; rewrite H9, nat_ascii8_embedding, <- H12 | rewrite <- H14])... Qed. Lemma correct_array16 : forall os bs n xs ys s1 s2 , DeserializeCorrect os bs -> n < pow 16 -> (s1, s2) = ascii16_of_nat n -> (xs, ys) = split_at n os -> DeserializeCorrect (Array16 xs :: ys) ("220" :: s1 :: s2 :: bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H3. assert (os = os0). apply split_at_soundness in H2. apply split_at_soundness in H10. rewrite H2, H10... rewrite_for os0. apply H in H9. assert ( n = nat_of_ascii16 (s1, s2)). rewrite H1. rewrite nat_ascii16_embedding... simpl. change (nat_of_ascii8 s1 * 256 + nat_of_ascii8 s2) with (nat_of_ascii16 (s1, s2)). rewrite <- H13. inversion H2. rewrite <- H9... Qed. Lemma correct_array32: forall os bs n xs ys s1 s2 s3 s4, DeserializeCorrect os bs -> (xs, ys) = split_at n os -> n < pow 32 -> ((s1, s2), (s3, s4)) = ascii32_of_nat n -> DeserializeCorrect (Array32 xs :: ys) ("221" :: s1 :: s2 :: s3 :: s4 :: bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H3. assert (os = os0). apply split_at_soundness in H0. apply split_at_soundness in H12. rewrite H0, H12... rewrite_for os0. apply H in H9. change (deserialize 0 ("221" :: s1 :: s2 :: s3 :: s4 :: bs)) with (let (zs, ws) := split_at (nat_of_ascii32 (s1, s2, (s3, s4))) (deserialize 0 bs) in Array32 zs :: ws). rewrite H9, H14, nat_ascii32_embedding, <- H12... Qed. Lemma correct_fixmap: forall os bs n xs ys b1 b2 b3 b4, DeserializeCorrect os bs -> (xs, ys) = split_at (2 * n) os -> length xs = 2 * n -> n < pow 4 -> Ascii b1 b2 b3 b4 false false false false = ascii8_of_nat n -> DeserializeCorrect (FixMap (pair xs) :: ys) (Ascii b1 b2 b3 b4 false false false true :: bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H4. assert ( n < pow 8). transitivity (pow 4); auto. apply pow_lt... assert ( n0 < pow 8). transitivity (pow 4); auto. apply pow_lt... assert (n0 = n); [| rewrite_for n0 ]. rewrite H3 in H16. apply ascii8_of_nat_eq in H16... assert (xs0 = xs); [| rewrite_for xs0 ]. rewrite <- (unpair_pair _ n xs), <- (unpair_pair _ n xs0); auto. rewrite H5... assert (os0 = os); [| rewrite_for os0 ]. apply split_at_soundness in H0. apply split_at_soundness in H13. rewrite H0, H13... apply H in H11. destruct b1, b2, b3, b4; (replace (deserialize 0 (_ :: bs)) with (let (zs, ws) := split_at (2 * (nat_of_ascii8 (ascii8_of_nat n))) @@ deserialize 0 bs in FixMap (pair zs) :: ws); [ unfold atat; rewrite nat_ascii8_embedding, H11, <- H13 | rewrite <- H16 ])... Qed. Lemma correct_map16: forall os bs n xs ys s1 s2, DeserializeCorrect os bs -> (xs, ys) = split_at (2 * n) os -> length xs = 2 * n -> n < pow 16 -> (s1, s2) = ascii16_of_nat n -> DeserializeCorrect (Map16 (pair xs) :: ys) ("222" :: s1 :: s2 :: bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H4. assert (n0 = n). rewrite H3 in H14. apply ascii16_of_nat_eq in H14... rewrite_for n0. assert (xs0 = xs). rewrite <- (unpair_pair _ n xs), <- (unpair_pair _ n xs0); auto. rewrite H5... rewrite_for xs0. assert (os0 = os). apply split_at_soundness in H0. apply split_at_soundness in H11. rewrite H0, H11... rewrite_for os0. apply H in H10. change (deserialize 0 ("222" :: s1 :: s2 :: bs)) with (let (zs, ws) := split_at (2 * nat_of_ascii16 (s1, s2)) @@ deserialize 0 bs in Map16 (pair zs) :: ws). unfold atat. rewrite H10, H14, nat_ascii16_embedding, <- H11... Qed. Lemma correct_map32: forall os bs n xs ys s1 s2 s3 s4, DeserializeCorrect os bs -> (xs, ys) = split_at (2 * n) os -> length xs = 2 * n -> n < pow 32 -> ((s1, s2), (s3, s4)) = ascii32_of_nat n -> DeserializeCorrect (Map32 (pair xs) :: ys) ("223" :: s1 :: s2 :: s3 :: s4 :: bs). Proof with auto. unfold DeserializeCorrect. intros. inversion H4. assert (n0 = n); [| rewrite_for n0 ]. rewrite H3 in H16. apply ascii32_of_nat_eq in H16... assert (xs0 = xs); [| rewrite_for xs0 ]. rewrite <- (unpair_pair _ n xs), <- (unpair_pair _ n xs0); auto. rewrite H5... assert (os0 = os); [| rewrite_for os0 ]. apply split_at_soundness in H0. apply split_at_soundness in H13. rewrite H0, H13... apply H in H11. change (deserialize 0 ("223" :: s1 :: s2 :: s3 :: s4 :: bs)) with (let (zs, ws) := split_at (2 * nat_of_ascii32 ((s1, s2),(s3,s4))) @@ deserialize 0 bs in Map32 (pair zs) :: ws). unfold atat. rewrite H16, H11, nat_ascii32_embedding, <- H13... Qed. Lemma correct_intro : forall os bs, (SerializedList os bs -> DeserializeCorrect os bs) -> DeserializeCorrect os bs. Proof with auto. unfold DeserializeCorrect. intros. apply H in H0... Qed. Theorem deserialize_correct : forall os bs, DeserializeCorrect os bs. Proof with auto. intros. apply correct_intro. intros. pattern os, bs. apply SerializedList_ind; intros; auto. apply correct_bot... apply correct_nil... apply correct_true... apply correct_false... apply correct_pfixnum... apply correct_nfixnum... apply correct_uint8... apply correct_uint16... apply correct_uint32... apply correct_uint64... apply correct_int8... apply correct_int16... apply correct_int32... apply correct_int64... apply correct_float... apply correct_double... apply correct_fixraw... simpl; apply correct_raw16... simpl; apply correct_raw32... apply correct_fixarray with (os:=os0) (n:=n)... apply correct_array16 with (os:=os0) (n:=n)... apply correct_array32 with (os:=os0) (n:=n)... apply correct_fixmap with (os:=os0) (n:=n)... apply correct_map16 with (os:=os0) (n:=n)... apply correct_map32 with (os:=os0) (n:=n)... Qed. Lemma app_nil: forall A (xs : list A), xs ++ [] = xs. Proof. induction xs. reflexivity. simpl. rewrite IHxs. reflexivity. Qed.