Merge pull request #653 from hacspec/library-fix-bounded-integers

library fix for libcrux ci
hacspec · May 7, 2024 · ecbd9cb · ecbd9cb
2 parents 5bb39d3 + 9436063
commit ecbd9cb
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 44 deletions.
diff --git 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'  }}

diff --git 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() &&

diff --git 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