From 8e9f09ab4e2dba50b6cd036a1d75094857c76e6f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Sun, 3 Dec 2023 11:21:12 -0800 Subject: [PATCH] Update tests --- tests/error-messages/Bug2021.fst.expected | 4 +- .../micro-benchmarks/ResolveImplicitsHook.fst | 7 +- tests/typeclasses/Bug3130b.fst | 3 + tests/typeclasses/Bug3130c.fst | 45 +++++ tests/typeclasses/Bug3130d.fst | 155 ++++++++++++++++++ 5 files changed, 210 insertions(+), 4 deletions(-) create mode 100644 tests/typeclasses/Bug3130c.fst create mode 100644 tests/typeclasses/Bug3130d.fst diff --git a/tests/error-messages/Bug2021.fst.expected b/tests/error-messages/Bug2021.fst.expected index 646b413f0a6..9dc9665b440 100644 --- a/tests/error-messages/Bug2021.fst.expected +++ b/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) diff --git a/tests/micro-benchmarks/ResolveImplicitsHook.fst b/tests/micro-benchmarks/ResolveImplicitsHook.fst index 13ac39dc3b0..306466a45b9 100644 --- a/tests/micro-benchmarks/ResolveImplicitsHook.fst +++ b/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) diff --git a/tests/typeclasses/Bug3130b.fst b/tests/typeclasses/Bug3130b.fst index a98c9c7e488..dd0a6493447 100644 --- a/tests/typeclasses/Bug3130b.fst +++ b/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 () diff --git a/tests/typeclasses/Bug3130c.fst b/tests/typeclasses/Bug3130c.fst new file mode 100644 index 00000000000..363ed916f81 --- /dev/null +++ b/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 = () diff --git a/tests/typeclasses/Bug3130d.fst b/tests/typeclasses/Bug3130d.fst new file mode 100644 index 00000000000..6b348d2d9e7 --- /dev/null +++ b/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); +}