From 16a77ca28952561628a6a74de4abd3b6e92f77d4 Mon Sep 17 00:00:00 2001
From: Karthikeyan Bhargavan <karthik.bhargavan@gmail.com>
Date: Mon, 6 May 2024 19:34:31 +0200
Subject: [PATCH 1/3] library fix for libcrux ci

---
 .../rust_primitives/Rust_primitives.Hax.fst   | 24 +++++++++----------
 1 file changed, 12 insertions(+), 12 deletions(-)

diff --git a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
index 54b447f80..2ae166f32 100644
--- a/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
+++ b/proof-libs/fstar/rust_primitives/Rust_primitives.Hax.fst
@@ -18,18 +18,6 @@ class update_at_tc self idx = {
 
 open Core.Slice
 
-instance impl__index t l n: t_Index (t_Array t l) (int_t n)
-  = { f_Output = t;
-      f_index_pre = (fun (s: t_Array t l) (i: int_t n) -> v i >= 0 && v i < v l);
-      f_index_post = (fun _ _ _ -> true);
-      f_index = (fun s i -> Seq.index s (v i));
-    }
-
-instance update_at_tc_array t l n: update_at_tc (t_Array t l) (int_t n) = {
-  super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Array t l) (int_t n);
-  update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
-}
-
 /// We have an instance for `int_t n`, but we often work with refined
 /// `int_t n`, and F* typeclass inference doesn't support subtyping
 /// well, hence the instance below.
@@ -47,6 +35,18 @@ instance update_at_tc_array_refined t l n r: update_at_tc (t_Array t l) (x: int_
   update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
 }
 
+instance impl__index t l n: t_Index (t_Array t l) (int_t n)
+  = { f_Output = t;
+      f_index_pre = (fun (s: t_Array t l) (i: int_t n) -> v i >= 0 && v i < v l);
+      f_index_post = (fun _ _ _ -> true);
+      f_index = (fun s i -> Seq.index s (v i));
+    }
+
+instance update_at_tc_array t l n: update_at_tc (t_Array t l) (int_t n) = {
+  super_index = FStar.Tactics.Typeclasses.solve <: t_Index (t_Array t l) (int_t n);
+  update_at = (fun arr i x -> FStar.Seq.upd arr (v i) x);
+}
+
 let (.[]<-) #self #idx {| update_at_tc self idx |} (s: self) (i: idx {f_index_pre s i})
   = update_at s i
 

From ce1a066a26286fc3b810bd8bdd486c0089f698bb Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 7 May 2024 08:36:54 +0200
Subject: [PATCH 2/3] fix(ci): remove `specs` tests

The https://github.com/hacspec/specs repository contains
specifications written in hacspec, mainly at the time of hacspec v1.

Since hacspec v1 is deprecated and archived, its library is deprecated
as well.

The hacspec lib (https://github.com/hacspec/hacspec/tree/master/lib)
doesn't typecheck any longer with `num-bigint` version `0.4.5`.

The hacspec lib dependents on `num-bigint` version `0.4`, not
specifying the minor version. The `specs` repository has no
`Cargo.lock`, and thus, from a clean `git clone`, `cargo build` pins
`num-bigint` to version `0.4.5`, breaking the hacspec library.

This broke https://github.com/hacspec/hax/pull/653 recently, and we
had the same kind of errors a couple times before in the past.

Two options were considered:
 - remove the tests related to the specs in the CI of hax;
 - commit a `Cargo.lock`.

The choose the first one: we need to update those specifications to
hax anyway: this will add motivation to
https://github.com/hacspec/specs/issues/13.
---
 .github/workflows/install_and_test.yml | 27 --------------------------
 1 file changed, 27 deletions(-)

diff --git a/.github/workflows/install_and_test.yml b/.github/workflows/install_and_test.yml
index 2a044548a..153175e83 100644
--- a/.github/workflows/install_and_test.yml
+++ b/.github/workflows/install_and_test.yml
@@ -41,33 +41,6 @@ jobs:
       with:
         repository: 'hacspec/specs'
         path: specs
-        
-    - name: Extract specifications
-      working-directory: specs
-      run: |
-        paths=$(tomlq -r '.workspace.members | .[]' Cargo.toml)
-        for cratePath in $paths; do
-          crate=$(tomlq -r '.package.name' "$cratePath/Cargo.toml")
-          for backend in fstar coq; do
-            for skip in $SKIPLIST; do
-              if [[ "$skip" == "$crate" || "$skip" == "$crate-$backend" ]]; then
-                echo "⛔ $crate [$backend] (skipping)"
-                continue 2
-              fi
-            done
-            echo "::group::$crate [$backend]"
-            cargo hax -C -p "$crate" \; into "$backend"
-            echo "::endgroup::"
-          done
-        done
-      env:
-        SKIPLIST: |
-          tls_cryptolib
-          hacspec-merlin
-          hacspec-halo2-coq
-          hacspec-halo2-fstar
-          hacspec-weierstrass-coq
-          hacspec-weierstrass-fstar
 
     - name: Push to Cachix
       if: ${{ github.event_name == 'workflow_dispatch'  || github.event_name == 'merge_group'  }}

From e8fdd4f8b9fea60c052ddf9381628bc3a78c18c8 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas@cryspen.com>
Date: Tue, 7 May 2024 09:14:24 +0200
Subject: [PATCH 3/3] fix(ci): test local `chacha20`, not `specs` one

---
 .github/workflows/test_installs.yml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/test_installs.yml b/.github/workflows/test_installs.yml
index 5ed2a6640..f0de760ea 100644
--- a/.github/workflows/test_installs.yml
+++ b/.github/workflows/test_installs.yml
@@ -40,12 +40,10 @@ jobs:
         ./setup.sh
     - run: cargo hax --version
     - name: Test an extraction
-      uses: actions/checkout@v3
-      with:
-        repository: 'hacspec/specs'
-    - run: |
+      run: |
+        cd examples/chacha20
         eval $(opam env)
-        cargo hax -C -p hacspec-chacha20 \; -i '**' into fstar
+        cargo hax into fstar
   setup_sh_status:
     if: |
       always() &&