Improve hax proofs

.github/workflows/hax.yml

@@ -14,7 +14,7 @@ jobs:
         uses: hacspec/hax-actions@main
         with:
           fstar: v2025.02.17
-          hax_reference: hax-lib-v0.3.5
+          hax_reference: tls-codec-panic-freedom
 
       - run: sudo apt-get install protobuf-compiler
 

Cargo.toml

@@ -10,7 +10,7 @@ rust-version = "1.83.0"
 [dependencies]
 curve25519-dalek = { version = "4.1.3", features = ["rand_core"] }
 displaydoc = "0.2"
-hax-lib = "0.3.5"
+hax-lib = {git = "https://github.com/cryspen/hax", branch = "tls-codec-panic-freedom"}
 hkdf = "0.12"
 libcrux-hkdf = "0.0.3"
 libcrux-hmac = "0.0.3"

proofs/fstar/models/Libcrux_ml_kem.Ind_cca.Incremental.Types.fsti

@@ -137,7 +137,8 @@ val impl_4__deserialize
 type t_Ciphertext1 (v_LEN: usize) = { f_value:t_Array u8 v_LEN }
 
 /// The size of the ciphertext.
-val impl_5__len: v_LEN: usize -> Prims.unit -> Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
+val impl_5__len: v_LEN: usize -> Prims.unit -> Prims.Pure usize Prims.l_True 
+  (ensures fun res -> let res:usize = res in res =. v_LEN)
 
 /// The partial ciphertext c2 - second part.
 type t_Ciphertext2 (v_LEN: usize) = { f_value:t_Array u8 v_LEN }

proofs/fstar/models/Libcrux_ml_kem.Mlkem768.Incremental.fsti

@@ -15,7 +15,7 @@ val pk1_len: Prims.unit -> Prims.Pure usize Prims.l_True
   (ensures fun res -> let res:usize = res in res =. mk_usize 64)
 
 /// Get the size of the second public key in bytes.
-val pk2_len: Prims.unit -> Prims.Pure usize Prims.l_True (fun _ -> Prims.l_True)
+val pk2_len: Prims.unit -> Prims.Pure usize Prims.l_True (ensures fun res -> res =. mk_usize 1152)
 
 /// The size of a compressed key pair in bytes.
 let v_COMPRESSED_KEYPAIR_LEN: usize = Libcrux_ml_kem.Mlkem768.v_SECRET_KEY_SIZE

src/chain.rs

@@ -217,6 +217,7 @@ impl ChainEpochDirection {
     }
 
     #[hax_lib::requires(next.len() > 0 && *ctr < u32::MAX)]
+    #[hax_lib::ensures(|_| *future(ctr) == ctr + 1)]
     fn next_key_internal(next: &mut [u8], ctr: &mut u32) -> (u32, [u8; 32]) {
         assert!(!next.is_empty());
         *ctr += 1;
@@ -258,18 +259,29 @@ impl ChainEpochDirection {
             // them all.
             self.prev.clear();
         }
-        hax_lib::fstar!("admit ()"); // potential overflows in condition and body of the loop
         while at > self.ctr + 1 {
+            hax_lib::loop_invariant!(self.ctr < u32::MAX);
+            hax_lib::loop_decreases!(u32::MAX - self.ctr);
+            hax_lib::assume!(self.next.len() > 0);
             let k = Self::next_key_internal(&mut self.next, &mut self.ctr);
+            hax_lib::assume!(
+                params.max_ooo_keys_or_default() < 390451572 && self.ctr <= u32::MAX - 390451572
+            );
             // Only add keys into our history if we're not going to immediately GC them.
             if self.ctr + params.max_ooo_keys_or_default() >= at {
+                hax_lib::assume!(
+                    params.trim_size() < 119304647
+                        && self.prev.data.len() <= KeyHistory::KEY_SIZE * params.trim_size()
+                );
                 self.prev.add(k, params);
             }
         }
         // After we've potentially added some new keys, see if there's any we
         // want to throw away.
         self.prev.gc(self.ctr, params);
 
+        hax_lib::assume!(self.next.len() > 0);
+
         Ok(Self::next_key_internal(&mut self.next, &mut self.ctr)
             .1
             .to_vec())

src/encoding/gf.rs

@@ -196,11 +196,15 @@ impl ops::Div<&GF16> for GF16 {
 }
 
 #[inline]
-#[hax_lib::fstar::verification_status(lax)] // proving absence of overflow in loop condition is tricky
+#[hax_lib::requires(into.len() <= usize::MAX - 2)]
+#[hax_lib::ensures(|_| future(into).len() == into.len())]
 pub fn parallel_mult(a: GF16, into: &mut [GF16]) {
-    let mut i = 0;
+    let mut i: usize = 0;
+    #[cfg(hax)]
+    let l = into.len();
     while i + 2 <= into.len() {
-        hax_lib::loop_decreases!(into.len() - i);
+        hax_lib::loop_decreases!(l - i);
+        hax_lib::loop_invariant!(into.len() == l && i <= l);
         (into[i].value, into[i + 1].value) = mul2_u16(a.value, into[i].value, into[i + 1].value);
         i += 2;
     }