Merge pull request #1281 from cryspen/ml-dsa-lib-additions

Library additions for ML-DSA verification

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

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)))
 
 

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