fallout from FStarLang/FStar#3203

src/cbor/impl/CBOR.Spec.Format.fst

@@ -1337,6 +1337,8 @@ let serialize_initial_byte_compare
   let b2' = synth_bitsum'_recip initial_byte_desc b2 in
   serialize_u8_spec' b1';
   serialize_u8_spec' b2';
+  seq_to_list_length_one (serialize serialize_initial_byte b1);
+  seq_to_list_length_one (serialize serialize_initial_byte b2);  
   assert (bytes_lex_compare
       (serialize serialize_initial_byte b1)
       (serialize serialize_initial_byte b2) == byte_compare b1' b2'
@@ -1449,12 +1451,18 @@ let rec bytes_lex_compare_serialize_strong_prefix1
   end else begin
     let x = Seq.index mid1 0 in
     let x2 = Seq.index mid2 0 in
+    let mid1' = Seq.tail mid1 in
+    let mid2' = Seq.tail mid2 in
+    assert (mid1 `Seq.equal` Seq.cons x mid1');
+    assert (mid2 `Seq.equal` Seq.cons x2 mid2');
+    Seq.lemma_append_cons mid1 suff1;
+    Seq.lemma_append_cons mid2 suff2;
+    assert ((mid1 `Seq.append` suff1) == Seq.cons x (mid1' `Seq.append` suff1));
+    assert ((mid2 `Seq.append` suff2) == Seq.cons x2 (mid2' `Seq.append` suff2));
     let c = byte_compare x x2 in
     if c = 0
     then begin
       assert (x == x2);
-      let mid1' = Seq.tail mid1 in
-      let mid2' = Seq.tail mid2 in
       let sx = Seq.slice mid1 0 1 in
       assert (sx `Seq.equal` Seq.slice mid2 0 1);
       let pre' = pre `Seq.append` sx in
@@ -1648,6 +1656,10 @@ let serialized_lex_compare_simple_value
   Seq.append_assoc (serialize serialize_initial_byte b1) (serialize (serialize_long_argument b1) l1) (serialize (serialize_content h1) c1);
   Seq.append_assoc (serialize serialize_initial_byte b2) (serialize (serialize_long_argument b2) l2) (serialize (serialize_content h2) c2);
   bytes_lex_compare_serialize_strong_prefix serialize_initial_byte b1 b2 (serialize (serialize_long_argument b1) l1 `Seq.append` serialize (serialize_content h1) c1) (serialize (serialize_long_argument b2) l2 `Seq.append` serialize (serialize_content h2) c2);
+  seq_to_list_length_one (serialize serialize_initial_byte b1);
+  seq_to_list_length_one (serialize serialize_initial_byte b2);
+  seq_to_list_append (serialize (serialize_long_argument b1) l1) (serialize (serialize_content h1) c1);
+  seq_to_list_append (serialize (serialize_long_argument b2) l2) (serialize (serialize_content h2) c2);
   let (ty1, (info1, ())) = b1 in
   let (ty2, (info2, ())) = b2 in
   if (x1 `U8.lte` max_simple_value_additional_info || x2 `U8.lte` max_simple_value_additional_info)
@@ -1667,7 +1679,9 @@ let serialized_lex_compare_simple_value
     assert (serialize s1_pre l1 == serialize (serialize_filter serialize_u8 simple_value_long_argument_wf) (LongArgumentSimpleValue?.v l1));
     assert (serialize s1' l1 == serialize (serialize_filter serialize_u8 simple_value_long_argument_wf) (LongArgumentSimpleValue?.v l1));
     assert (serialize s1' l1 == Seq.create 1 x1');
+    seq_to_list_length_one (serialize s1' l1);
     assert (serialize (serialize_long_argument b1) l1 == Seq.create 1 (x1 <: U8.t));
+    seq_to_list_length_one (serialize (serialize_long_argument b1) l1);
     assert (b2 == (cbor_major_type_simple_value, (additional_info_long_argument_8_bits, ())));
     let LongArgumentSimpleValue _ x2' = l2 in
     assert (x2 == x2');
@@ -1681,7 +1695,9 @@ let serialized_lex_compare_simple_value
     assert (serialize s2_pre l2 == serialize (serialize_filter serialize_u8 simple_value_long_argument_wf) (LongArgumentSimpleValue?.v l2));
     assert (serialize s2' l2 == serialize (serialize_filter serialize_u8 simple_value_long_argument_wf) (LongArgumentSimpleValue?.v l2));
     assert (serialize s2' l2 == Seq.create 1 x2');
+    seq_to_list_length_one (serialize s2' l2);
     assert (serialize (serialize_long_argument b2) l2 == Seq.create 1 (x2 <: U8.t));
+    seq_to_list_length_one (serialize (serialize_long_argument b2) l2);
     bytes_lex_compare_serialize_strong_prefix serialize_header h1 h2 (serialize (serialize_content h1) c1) (serialize (serialize_content h2) c2)
   end
 

src/cbor/impl/CBOR.Spec.fst

@@ -54,7 +54,11 @@ let rec bytes_lex_compare_correct
   [SMTPat (bytes_lex_compare s1 s2)]
 = if Seq.length s1 = 0 || Seq.length s2 = 0
   then ()
-  else bytes_lex_compare_correct (Seq.tail s1) (Seq.tail s2)
+  else begin
+    Seq.cons_head_tail s1;
+    Seq.cons_head_tail s2;
+    bytes_lex_compare_correct (Seq.tail s1) (Seq.tail s2)
+  end
 
 let bytes_lex_compare_equal
   x1 x2

src/cbor/impl/CBOR.SteelST.Raw.Map.fst

@@ -301,6 +301,7 @@ let compare_u64
   : Tot I16.t
   = if x1 `U64.lt` x2 then -1s else if x2 `U64.lt` x1 then 1s else 0s
 
+(*
 #push-options "--z3rlimit 32 --ifuel 8"
 
 #restart-solver
@@ -342,3 +343,4 @@ let lex_compare_with_header
   end
 
 #pop-options
+*)

src/cbor/impl/CBOR.SteelST.Raw.Map.fsti

@@ -172,6 +172,7 @@ val jump_data_item
 
 (* Comparisons with unserialized values *)
 
+(*
 val lex_compare_with_header
   (ty: Ghost.erased major_type_t { ty `U8.lt` cbor_major_type_simple_value })
   (x: U64.t)
@@ -187,3 +188,4 @@ val lex_compare_with_header
       let s = serialize serialize_header vh.contents in
       bytes_lex_compare s0 s `same_sign` I16.v i
     )
+*)

src/lowparse/LowParse.Spec.Endianness.fst

@@ -51,6 +51,11 @@ let big_endian_lex_compare_eq
     E.n_to_be_inj n x y
   end else ()
 
+let seq_to_list_singleton (#t: Type) (x: t) : Lemma
+  (Seq.seq_to_list (Seq.create 1 x) == [x])
+  [SMTPat (Seq.seq_to_list (Seq.create 1 x))]
+= assert (Seq.create 1 x `Seq.equal` Seq.cons x Seq.empty)
+
 let rec big_endian_lex_compare_aux
   (n: nat)
   (compare: (U8.t -> U8.t -> int))

src/lowparse/LowParse.Spec.SeqBytes.fst

@@ -209,6 +209,14 @@ let bytes_lex_compare_append
   S.seq_to_list_append l2 l2';
   S.lex_compare_append byte_compare (Seq.seq_to_list l1) (Seq.seq_to_list l2) (Seq.seq_to_list l1') (Seq.seq_to_list l2')
 
+let seq_to_list_length_one (#t: Type) (s: Seq.seq t) : Lemma
+  (requires (Seq.length s == 1))
+  (ensures (
+    Seq.length s == 1 /\
+    Seq.seq_to_list s == [Seq.index s 0]
+  ))
+= assert (s `Seq.equal` (Seq.index s 0 `Seq.cons` Seq.empty))
+
 #push-options "--z3rlimit 16"
 #restart-solver
 
@@ -229,14 +237,20 @@ let rec bytes_lex_order_prefix_or_append
     Seq.lemma_split l2 1;
     let h1 = Seq.slice l1 0 1 in
     let t1 = Seq.slice l1 1 (Seq.length l1) in
+    let x1 = Seq.index h1 0 in
+    assert (l1 == Seq.cons x1 t1);
     Seq.append_assoc h1 t1 suff1;
     let h2 = Seq.slice l2 0 1 in
     let t2 = Seq.slice l2 1 (Seq.length l2) in
+    let x2 = Seq.index h2 0 in
+    assert (l2 == Seq.cons x2 t2);
     Seq.append_assoc h2 t2 suff2;
     if Seq.index l1 0 `FStar.UInt8.lt` Seq.index l2 0
-    then
+    then begin
+      seq_to_list_length_one h1;
+      seq_to_list_length_one h2;
       bytes_lex_compare_append h1 h2 (t1 `Seq.append` suff1) (t2 `Seq.append` suff2)
-    else begin
+    end else begin
       assert (Seq.index l1 0 = Seq.index l2 0);
       S.seq_to_list_append l1 suff1;
       S.seq_to_list_append l2 suff2;

src/lowparse/LowParse.Spec.Sorted.fst

@@ -437,6 +437,11 @@ let rec seq_to_list_append
   then begin
     assert ((s1 `Seq.append` s2) `Seq.equal` s2)
   end else begin
-    assert (Seq.slice (s1 `Seq.append` s2) 1 (Seq.length (s1 `Seq.append` s2)) `Seq.equal` (Seq.slice s1 1 (Seq.length s1) `Seq.append` s2));
-    seq_to_list_append (Seq.slice s1 1 (Seq.length s1)) s2
+    let h = Seq.head s1 in
+    let t = Seq.tail s1 in
+    assert (s1 == Seq.cons h t);
+    assert (s1 `Seq.append` s2 `Seq.equal` Seq.cons h (t `Seq.append` s2));
+    Seq.lemma_seq_to_list_cons h t;
+    Seq.lemma_seq_to_list_cons h (t `Seq.append` s2);
+    seq_to_list_append t s2
   end

src/lowparse/steel/LowParse.SteelST.SeqBytes.fst

@@ -135,8 +135,10 @@ let rec seq_all_bytes_to_nlist_byte
     I.parse_u8_spec' (AP.contents_of vl);
     parser_kind_prop_equiv I.parse_u8_kind I.parse_u8;
     noop ();
-    let _ = intro_aparse I.parse_u8 a in
-    let _ = intro_seq_all_bytes a' in
+    let vc = intro_aparse I.parse_u8 a in
+    let vr = intro_seq_all_bytes a' in
+    noop ();
+    assert (va.contents `Seq.equal` (vc.contents `Seq.cons` vr.contents));
     let _ = seq_all_bytes_to_nlist_byte n' a' in
     NL.intro_nlist_cons n I.parse_u8 n' a a'
   end