Update tests

tests/error-messages/Bug2021.fst.expected

@@ -36,8 +36,8 @@
 
 >>]
 >> Got issues: [
-* Error 66 at Bug2021.fst(37,13-37,14):
-  - Failed to resolved implicit argument ?11
+* Error 66 at Bug2021.fst(37,13-37,17):
+  - Failed to resolved implicit argument ?13
     of type Prims.int
     introduced for Instantiating implicit argument in application
   - See also Bug2021.fst(36,11-36,12)

tests/micro-benchmarks/ResolveImplicitsHook.fst

@@ -123,8 +123,11 @@ let resolve_tac_alt () : Tac unit =
 #push-options "--warn_error @348"
 
 //raises 348 for ambiguity in resolve_implicits
-// GM 2023-02-01: Used to raise 348 five times, but now it's 15 after some scoping fixes in Tc (why?)
-[@@expect_failure [348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 66]]
+// GM 2023-02-01: Used to raise 348 five times, but now it's 15 after
+// some scoping fixes in Tc (why?)
+// GM 2023-12-03: Now 21 times, whatever. It's probably due to slight
+// differences in the messages which decrease deduplication.
+[@@expect_failure [348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 348; 66]]
 let test3 (b:bool)
   : cmd (r1 ** r2 ** r3 ** r4 ** r5)
         (r1 ** r2 ** r3 ** r4 ** r5)

tests/typeclasses/Bug3130b.fst

@@ -19,5 +19,8 @@ let test5 (y : it 6) = let p : Type0 = y == mk6 in ()
 let test6 () = let p : Type0 = mk5 == mk6 in ()
 let test7 () = let p : Type0 = mk6 == mk5 in ()
 
+(* These are ambiguous. They only work since we are running the meta
+args in contexts with yet-unresolved uvars, which is somewhat shady to
+do. If we forbid that, and these break, it's not too bad. *)
 let test8 (x:_) = let p : Type0 = mk5 == x /\ x == mk6 in ()
 let test9 (x:_) = let p : Type0 = mk6 == x /\ x == mk5 in ()

tests/typeclasses/Bug3130c.fst

@@ -0,0 +1,45 @@
+module Bug3130c
+
+open FStar.Tactics.Typeclasses
+
+class typeclass1 (a:Type0) = {
+  x: unit;
+}
+
+class typeclass2 (bytes:Type0) {|typeclass1 bytes|} (a:Type) = {
+  y:unit;
+}
+
+assume val bytes: Type0
+assume val bytes_typeclass1: typeclass1 bytes
+instance bytes_typeclass1_ = bytes_typeclass1
+assume val t: Type0 -> Type0
+assume val t_inst: t bytes
+
+assume val truc:
+  #bytes:Type0 -> {|typeclass1 bytes|} ->
+  #a:Type -> {|typeclass2 bytes a|} ->
+  t bytes -> a ->
+  Type0
+
+noeq
+type machin (a:Type) {|typeclass2 bytes a|} = {
+  pred: a -> prop;
+  lemma:
+    content:a ->
+    Lemma
+    (ensures truc t_inst content)
+  ;
+}
+
+let pre (#a:Type) {|d : typeclass2 bytes a|}
+        (m : machin a) (x : a)
+        = m.pred x
+
+val bidule:
+  #a:Type -> {|typeclass2 bytes a|} ->
+  m:machin a -> x:a ->
+  Lemma
+  (requires m.pred x)
+  (ensures True)
+let bidule #a #tc2 m x = ()

tests/typeclasses/Bug3130d.fst

@@ -0,0 +1,155 @@
+module Bug3130d
+
+(* Taken from Comparse *)
+
+open FStar.Mul
+
+type nat_lbytes (sz:nat) = n:nat{n < normalize_term (pow2 (8*sz))}
+
+assume
+val nat_lbytes_helper: sz:nat -> Lemma (normalize_term (pow2 (8*sz)) == pow2 (8*sz))
+[SMTPat (nat_lbytes sz)]
+
+/// Minimal interface to manipulate symbolic bytes.
+/// Here are the explanations for a few design decisions:
+/// - We don't require that only `empty` has length zero, e.g. we may have `concat empty empty <> empty`.
+/// - We implement `split` and not `slice`, because `slice` causes trouble in the symbolic case:
+///   with `slice`, how do you get the left and right part of `concat empty (concat empty empty)`?
+/// - `split` returns an option, hence can fail if the indices are not on the correct bounds.
+///   * We require `split` to succeed on the bound of a `concat` (see `split_concat_...`).
+///   * This is useful to state the `concat_split` lemma in a way which would be correct on symbolic bytes.
+/// - To compensate the first fact, and the fact that we don't require decidable equality,
+///   we need a function that recognize the `empty` bytes.
+/// - The `to_nat` function can fail, if the bytes are not public for example
+
+class bytes_like (bytes:Type0) = {
+  length: bytes -> nat;
+
+  empty: bytes;
+  empty_length: unit -> Lemma (length empty == 0);
+  recognize_empty: b:bytes -> res:bool{res <==> b == empty};
+
+  concat: bytes -> bytes -> bytes;
+  concat_length: b1:bytes -> b2:bytes -> Lemma (length (concat b1 b2) == (length b1) + (length b2));
+
+  split: b:bytes -> i:nat -> option (bytes & bytes);
+  split_length: b:bytes -> i:nat -> Lemma (
+    match split b i with
+    | Some (b1, b2) -> length b1 == i /\ i+length b2 == length b
+    | None -> True
+  );
+
+  split_concat: b1:bytes -> b2:bytes -> Lemma (split (concat b1 b2) (length b1) == Some (b1, b2));
+
+  concat_split: b:bytes -> i:nat -> Lemma (
+    match split b i with
+    | Some (lhs, rhs) -> concat lhs rhs == b
+    | _ -> True
+  );
+
+  to_nat: b:bytes -> option (nat_lbytes (length b));
+  from_nat: sz:nat -> nat_lbytes sz -> b:bytes{length b == sz};
+
+  from_to_nat: sz:nat -> n:nat_lbytes sz -> Lemma
+    (to_nat (from_nat sz n) == Some n);
+
+  to_from_nat: b:bytes -> Lemma (
+    match to_nat b with
+    | Some n -> b == from_nat (length b) n
+    | None -> True
+  );
+}
+
+/// This type defines a predicate on `bytes` that is compatible with its structure.
+/// It is meant to be used for labeling predicates, which are typically compatible with the `bytes` structure.
+
+let bytes_pre_is_compatible (#bytes:Type0) {|bytes_like bytes|} (pre:bytes -> prop) =
+    (pre empty) /\
+    (forall b1 b2. pre b1 /\ pre b2 ==> pre (concat b1 b2)) /\
+    (forall b i. pre b /\ Some? (split b i) ==> pre (fst (Some?.v (split b i))) /\ pre (snd (Some?.v (split b i)))) /\
+    (forall sz n. pre (from_nat sz n))
+
+let bytes_pre_is_compatible_intro
+  (#bytes:Type0) {|bytes_like bytes|} (pre:bytes -> prop)
+  (empty_proof:squash(pre empty))
+  (concat_proof:(b1:bytes{pre b1} -> b2:bytes{pre b2} -> Lemma (pre (concat b1 b2))))
+  (split_proof:(b:bytes{pre b} -> i:nat{Some? (split #bytes b i)} -> Lemma (pre (fst (Some?.v (split b i))) /\ pre (snd (Some?.v (split b i))))))
+  (from_nat_proof:(sz:nat -> n:nat_lbytes sz -> Lemma (pre (from_nat sz n))))
+  : squash (bytes_pre_is_compatible pre)
+  =
+  FStar.Classical.forall_intro_2 concat_proof;
+  FStar.Classical.forall_intro_2 split_proof;
+  FStar.Classical.forall_intro_2 from_nat_proof
+
+type bytes_compatible_pre (bytes:Type0) {|bytes_like bytes|} =
+  pre:(bytes -> prop){bytes_pre_is_compatible pre}
+
+let seq_u8_bytes_like: bytes_like (Seq.seq UInt8.t) = {
+  length = Seq.length;
+
+  empty = (Seq.empty);
+  empty_length = (fun () -> ());
+  recognize_empty = (fun b ->
+    assert(Seq.length b = 0 ==> b `Seq.eq` Seq.empty);
+    Seq.length b = 0
+  );
+
+  concat = (fun b1 b2 -> Seq.append b1 b2);
+  concat_length = (fun b1 b2 -> ());
+
+  split = (fun b i ->
+    if i <= Seq.length b then
+      Some (Seq.slice b 0 i, Seq.slice b i (Seq.length b))
+    else
+      None
+  );
+
+  split_length = (fun b i -> ());
+  split_concat = (fun b1 b2 ->
+    assert(b1 `Seq.eq` (Seq.slice (Seq.append b1 b2) 0 (Seq.length b1)));
+    assert(b2 `Seq.eq` (Seq.slice (Seq.append b1 b2) (Seq.length b1) (Seq.length (Seq.append b1 b2))))
+  );
+  concat_split = (fun b i ->
+    if i <= Seq.length b then
+      assert(b `Seq.eq` Seq.append (Seq.slice b 0 i) (Seq.slice b i (Seq.length b)))
+    else ()
+  );
+
+  to_nat = (fun b ->
+    FStar.Endianness.lemma_be_to_n_is_bounded b;
+    Some (FStar.Endianness.be_to_n b)
+  );
+  from_nat = (fun sz n ->
+    FStar.Endianness.n_to_be sz n
+  );
+
+  from_to_nat = (fun sz n -> ());
+  to_from_nat = (fun b -> ());
+}
+
+let refine_bytes_like (bytes:Type0) {|bytes_like bytes|} (pre:bytes_compatible_pre bytes): bytes_like (b:bytes{pre b}) = {
+  length = (fun (b:bytes{pre b}) -> length #bytes b);
+
+  empty = empty #bytes;
+  empty_length = (fun () -> empty_length #bytes ());
+  recognize_empty = (fun b -> recognize_empty #bytes b);
+
+  concat = (fun b1 b2 -> concat #bytes b1 b2);
+  concat_length = (fun b1 b2 -> concat_length #bytes b1 b2);
+
+  split = (fun b i ->
+    match split #bytes b i with
+    | None -> None
+    | Some (b1, b2) -> Some (b1, b2)
+  );
+  split_length = (fun b i -> split_length #bytes b i);
+
+  split_concat = (fun b1 b2 -> split_concat #bytes b1 b2);
+  concat_split = (fun b i -> concat_split #bytes b i);
+
+  to_nat = (fun b -> to_nat #bytes b);
+  from_nat = (fun sz n -> from_nat #bytes sz n);
+
+  from_to_nat = (fun sz n -> from_to_nat #bytes sz n);
+  to_from_nat = (fun b -> to_from_nat #bytes b);
+}