chore(bounded-ints): refresh snapshot

hacspec · Jun 24, 2024 · cf6012d · cf6012d
1 parent ebd667a
commit cf6012d
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 28 deletions.
diff --git a/hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.fst b/hax-bounded-integers/proofs/fstar/extraction/Hax_bounded_integers.fst
@@ -38,30 +38,3 @@ let t_BoundedU8 (v_MIN v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX}
 
 ///Bounded usize integers. This struct enforces the invariant that values are greater or equal to `MIN` and less or equal to `MAX`.
 let t_BoundedUsize (v_MIN v_MAX: usize) = x: usize{x >=. v_MIN && x <=. v_MAX}
-
-let t_Test (v_B: usize) =
-  x:
-  i16
-    { x >=. (Core.Ops.Arith.Neg.neg (cast (v_B <: usize) <: i16) <: i16) &&
-      x <=. (cast (v_B <: usize) <: i16) }
-
-let tests (_: Prims.unit) : Prims.unit =
-  let (zzz: t_Test (sz 123)):t_Test (sz 123) = (-122s) <: t_Test (sz 123) in
-  let zzz:t_Test (sz 123) = Core.Ops.Arith.f_add_assign #(t_Test (sz 123)) #i16 zzz 32s in
-  let (x: t_BoundedU8 0uy 5uy):t_BoundedU8 0uy 5uy = 2uy <: t_BoundedU8 0uy 5uy in
-  let (y: t_BoundedU8 5uy 10uy):t_BoundedU8 5uy 10uy = x +! x <: t_BoundedU8 5uy 10uy in
-  let _:u8 = x >>! 3uy in
-  let _:u8 = x >>! (3uy <: t_BoundedU8 0uy 5uy) in
-  let _:u8 = x /! y in
-  let _:u8 = x *! y in
-  let _:u8 = x +! y in
-  let _:u8 = y -! x in
-  let _:u8 = x /! 1uy in
-  let _:u8 = x *! 1uy in
-  let _:u8 = x +! 1uy in
-  let _:u8 = x -! 1uy in
-  let _:u8 = 4uy /! y in
-  let _:u8 = 4uy *! y in
-  let _:u8 = 4uy +! y in
-  let _:u8 = 4uy -! y in
-  ()
diff --git a/hax-bounded-integers/src/lib.rs b/hax-bounded-integers/src/lib.rs
@@ -363,7 +363,7 @@ const _: () = {
 #[test]
 fn tests() {
     refinement_int!(
-        Test<const B: usize>(i16, 2, |x| x >= -(B as i16) && x <= (B as i16))
+        Test<const B: usize>(i16, 2, |x| B < 32768 && x >= -(B as i16) && x <= (B as i16))
     );
 
     use hax_lib::*;