Nix fixes

SSProve · Feb 3, 2025 · 3800608 · 3800608
1 parent 3f59a42
commit 3800608
Show file tree

Hide file tree

Showing 8 changed files with 65 additions and 23 deletions.
diff --git a/.github/workflows/nix-action-8.18.yml b/.github/workflows/nix-action-8.18.yml
@@ -36,12 +36,18 @@ jobs:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community, math-comp
         name: ssprove
+    - id: stepGetDerivation
+      name: Getting derivation for current job (coq)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"8.18\" --argstr job \"coq\" \\\n   --dry-run 2> err > out || (touch fail;
+        true)\n"
+    - name: Error reporting
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
+    - name: Failure check
+      run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
-      name: Checking presence of CI target coq
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr
-        bundle \"8.18\" --argstr job \"coq\" \\\n   --dry-run 2>&1 > /dev/null)\n
-        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
-        s/.*/built/\") >> $GITHUB_OUTPUT\n"
+      name: Checking presence of CI target for current job
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
@@ -84,12 +90,18 @@ jobs:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community, math-comp
         name: ssprove
+    - id: stepGetDerivation
+      name: Getting derivation for current job (mathcomp-analysis)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"8.18\" --argstr job \"mathcomp-analysis\" \\\n   --dry-run 2> err > out
+        || (touch fail; true)\n"
+    - name: Error reporting
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
+    - name: Failure check
+      run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
-      name: Checking presence of CI target mathcomp-analysis
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr
-        bundle \"8.18\" --argstr job \"mathcomp-analysis\" \\\n   --dry-run 2>&1 >
-        /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
-        \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
+      name: Checking presence of CI target for current job
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr
@@ -153,12 +165,18 @@ jobs:
         authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
         extraPullNames: coq, coq-community, math-comp
         name: ssprove
+    - id: stepGetDerivation
+      name: Getting derivation for current job (ssprove)
+      run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr bundle
+        \"8.18\" --argstr job \"ssprove\" \\\n   --dry-run 2> err > out || (touch
+        fail; true)\n"
+    - name: Error reporting
+      run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
+    - name: Failure check
+      run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
-      name: Checking presence of CI target ssprove
-      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr
-        bundle \"8.18\" --argstr job \"ssprove\" \\\n   --dry-run 2>&1 > /dev/null)\n
-        echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
-        s/.*/built/\") >> $GITHUB_OUTPUT\n"
+      name: Checking presence of CI target for current job
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.18" --argstr

diff --git a/.github/workflows/nix-action-8.19.yml b/.github/workflows/nix-action-8.19.yml
@@ -47,7 +47,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
@@ -101,7 +101,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr
@@ -176,7 +176,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.19" --argstr

diff --git a/.github/workflows/nix-action-8.20.yml b/.github/workflows/nix-action-8.20.yml
@@ -47,7 +47,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: Building/fetching current CI target
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -101,7 +101,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
@@ -176,7 +176,7 @@ jobs:
       run: if [ -e fail ]; then exit 1; else exit 0; fi;
     - id: stepCheck
       name: Checking presence of CI target for current job
-      run: (echo -n status=; cat out | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
+      run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
     - if: steps.stepCheck.outputs.status == 'built'
       name: 'Building/fetching previous CI target: coq'
       run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr

diff --git a/.github/workflows/opam-build.yml b/.github/workflows/opam-build.yml
@@ -51,4 +51,5 @@ jobs:
         run: |
           opam repo add coq-released https://coq.inria.fr/opam/released
           opam install coq.8.18.0 coq-equations.1.3+8.18 coq-mathcomp-ssreflect.2.1.0 coq-mathcomp-analysis.1.0.0 coq-extructures.0.4.0 coq-deriving.0.2.0 coq-mathcomp-word.3.0 coq-mathcomp-zify.1.5.0+2.0+8.16
+          opam pin jasmin.dev git+https://github.com/jasmin-lang/jasmin.git#main
           opam exec -- make -j4
diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix
@@ -1 +1 @@
-"78d95509824be9e3339c1c0ee19f9c085f32b23e"
+"ee1cc6946f9f33dd281f74cd5c5273786f0e0850"
diff --git a/.nix/coq-overlays/jasmin/default.nix b/.nix/coq-overlays/jasmin/default.nix
@@ -0,0 +1,11 @@
+{ lib, mkCoqDerivation, coq, mathcomp-word, version ? null }:
+
+mkCoqDerivation {
+  pname = "jasmin";
+  owner = "jasmin-lang";
+  inherit version;
+  defaultVersion = null;
+
+  makeFlags = [ "-C proofs" ];
+  propagatedBuildInputs = [ mathcomp-word ];
+}
diff --git a/.nix/coq-overlays/SSProve/default.nix → .nix/coq-overlays/ssprove/default.nix b/.nix/coq-overlays/SSProve/default.nix → .nix/coq-overlays/ssprove/default.nix
@@ -7,6 +7,7 @@
 , mathcomp-zify
 , extructures
 , deriving
+, jasmin
 }:
 
 (mkCoqDerivation {
@@ -42,7 +43,8 @@
                            mathcomp-word
                            mathcomp-zify
                            extructures
-                           deriving];
+                           deriving
+                           jasmin];
 
   meta = with lib; {
     description = "SSProve: A Foundational Framework for Modular Cryptographic Proofs in Coq";

diff --git a/theories/Jasmin/examples/add1.v b/theories/Jasmin/examples/add1.v
@@ -16,7 +16,17 @@ Import ListNotations.
 Local Open Scope string.
 
 
+Section Test.
+Context `{AsmOp : asmOp}.
 
+From Coq Require Import PrimInt63.
+
+Import FunName.
+Definition f : funname.
+Proof.
+    unfold funname.
+    Transparent t.
+    exact 1%uint63.
 
 Definition ssprove_jasmin_prog : uprog.
 Proof.
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		"78d95509824be9e3339c1c0ee19f9c085f32b23e"
		"ee1cc6946f9f33dd281f74cd5c5273786f0e0850"