From 59ff7cd63958b175a348e3b1432eacc823341e71 Mon Sep 17 00:00:00 2001
From: Karthikeyan Bhargavan <karthik.bhargavan@gmail.com>
Date: Sun, 2 Feb 2025 13:18:30 +0100
Subject: [PATCH 1/3] lib extensions

---
 proof-libs/fstar/core/Core.Array.fsti | 2 +-
 proof-libs/fstar/core/Core.Num.fsti   | 2 ++
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/proof-libs/fstar/core/Core.Array.fsti b/proof-libs/fstar/core/Core.Array.fsti
index e02274be0..b2b2f3e97 100644
--- a/proof-libs/fstar/core/Core.Array.fsti
+++ b/proof-libs/fstar/core/Core.Array.fsti
@@ -8,6 +8,6 @@ let impl_23__map #a n #b (arr: t_Array a n) (f: a -> b): t_Array b n
 
 let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 
-val from_fn #a len (f: usize -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))
+val from_fn #a len (f: (x:usize{x <. len}) -> a): Pure (t_Array a len) (requires True) (ensures (fun a -> forall i. Seq.index a i == f (sz i)))
     
 
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
index 2521af35f..d9d6b115c 100644
--- a/proof-libs/fstar/core/Core.Num.fsti
+++ b/proof-libs/fstar/core/Core.Num.fsti
@@ -2,6 +2,8 @@ module Core.Num
 open Rust_primitives
 
 let impl_u16__MAX: u16 = mk_u16 (maxint u16_inttype)
+let impl_i32__MAX: i32 = mk_i32 (maxint i32_inttype)
+let impl_i32__MIN: i32 = mk_i32 (minint i32_inttype)
 
 let impl_u8__wrapping_add: u8 -> u8 -> u8 = add_mod
 let impl_u8__wrapping_sub: u8 -> u8 -> u8 = sub_mod

From e1aeb7bdc0b36e8056981a5437dda43ad8e18128 Mon Sep 17 00:00:00 2001
From: Karthikeyan Bhargavan <karthik.bhargavan@gmail.com>
Date: Mon, 3 Feb 2025 08:30:51 +0100
Subject: [PATCH 2/3] added Int trait impls

---
 hax-lib/src/dummy.rs | 46 +++++++++++++++++++++++++++++++++++++++-----
 1 file changed, 41 insertions(+), 5 deletions(-)

diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs
index 2d462f547..1ebef1715 100644
--- a/hax-lib/src/dummy.rs
+++ b/hax-lib/src/dummy.rs
@@ -58,7 +58,9 @@ pub trait RefineAs<RefinedType> {
 }
 
 pub mod int {
-    #[derive(Clone, Copy)]
+    use core::ops::*;
+
+    #[derive(Copy, Clone, Eq, PartialEq, Ord, PartialOrd)]
     pub struct Int(pub u8);
 
     impl Int {
@@ -70,10 +72,37 @@ pub mod int {
         }
     }
 
-    impl Int {}
-    impl Int {}
-    impl Int {}
-    impl Int {}
+    impl Add for Int {
+    	type Output = Self;
+
+    	fn add(self, other: Self) -> Self::Output {
+           Int(0)
+        }
+    }
+
+    impl Sub for Int {
+    	type Output = Self;
+
+    	fn sub(self, other: Self) -> Self::Output {
+           Int(0)
+        }
+    }
+
+    impl Mul for Int {
+    	type Output = Self;
+
+    	fn mul(self, other: Self) -> Self::Output {
+           Int(0)
+        }
+    }
+
+    impl Div for Int {
+    	type Output = Self;
+
+    	fn div(self, other: Self) -> Self::Output {
+           Int(0)
+        }
+    }
 
     impl Int {
         pub fn pow2(self) -> Self {
@@ -100,6 +129,13 @@ pub mod int {
         }
     }
 
+    impl Abstraction for i32 {
+        type AbstractType = Int;
+        fn lift(self) -> Self::AbstractType {
+            Int(0)
+        }
+    }
+
     impl Concretization<u32> for Int {
         fn concretize(self) -> u32 {
             0

From 1acd747cf0fa01e2c4999bc645003f678bd21881 Mon Sep 17 00:00:00 2001
From: Karthikeyan Bhargavan <karthik.bhargavan@gmail.com>
Date: Mon, 3 Feb 2025 10:22:09 +0100
Subject: [PATCH 3/3] fmt

---
 hax-lib/src/dummy.rs | 24 ++++++++++++------------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/hax-lib/src/dummy.rs b/hax-lib/src/dummy.rs
index 1ebef1715..891187753 100644
--- a/hax-lib/src/dummy.rs
+++ b/hax-lib/src/dummy.rs
@@ -73,34 +73,34 @@ pub mod int {
     }
 
     impl Add for Int {
-    	type Output = Self;
+        type Output = Self;
 
-    	fn add(self, other: Self) -> Self::Output {
-           Int(0)
+        fn add(self, other: Self) -> Self::Output {
+            Int(0)
         }
     }
 
     impl Sub for Int {
-    	type Output = Self;
+        type Output = Self;
 
-    	fn sub(self, other: Self) -> Self::Output {
-           Int(0)
+        fn sub(self, other: Self) -> Self::Output {
+            Int(0)
         }
     }
 
     impl Mul for Int {
-    	type Output = Self;
+        type Output = Self;
 
-    	fn mul(self, other: Self) -> Self::Output {
-           Int(0)
+        fn mul(self, other: Self) -> Self::Output {
+            Int(0)
         }
     }
 
     impl Div for Int {
-    	type Output = Self;
+        type Output = Self;
 
-    	fn div(self, other: Self) -> Self::Output {
-           Int(0)
+        fn div(self, other: Self) -> Self::Output {
+            Int(0)
         }
     }