Configure CI

.github/workflows/ci.yml

@@ -0,0 +1,38 @@
+name: crypto-specs
+
+on:
+  workflow_dispatch:
+  push:
+    branches:
+      - main
+
+env:
+  OPAMROOT: /home/charlie/.opam
+  OPAMYES: true
+  OPAMJOBS: 2
+  ECRJOBS: 1
+
+jobs:
+  ec:
+    name: Check EasyCrypt Files
+    runs-on: ubuntu-20.04
+    container:
+      image: ghcr.io/easycrypt/ec-build-box
+    strategy:
+      fail-fast: false
+    steps:
+    - uses: actions/checkout@v4
+    - uses: actions/checkout@v4
+      with:
+        repository: jasmin-lang/jasmin
+        ref: refs/heads/main
+        path: jasmin
+    - name: Compile & Install EasyCrypt
+      run: |
+        opam pin --dev-repo add -n easycrypt https://github.com/EasyCrypt/easycrypt.git
+        opam install -v easycrypt
+    - name: Detect SMT provers
+      run: |
+        opam exec -- easycrypt why3config
+    - name: Compile Project
+      run: opam exec -- make check

Makefile

@@ -2,6 +2,7 @@
 
 # --------------------------------------------------------------------
 ECCONF := config/tests.config 
+JOBS   ?= 1
 CHECKS ?= specs
 
 # --------------------------------------------------------------------
@@ -10,7 +11,7 @@ CHECKS ?= specs
 default: check
 
 check:
-	easycrypt runtest $(ECCONF) $(CHECKS)
+	easycrypt runtest -jobs $(JOBS) $(ECCONF) $(CHECKS)
 
 clean_eco:
-	find kyber768 -name '*.eco' -exec rm '{}' ';'
+	find . -name '*.eco' -exec rm '{}' ';'

config/tests.config

@@ -1,6 +1,5 @@
 [default]
 bin  = easycrypt
-args = -timeout 30 -R ml-kem -I Jasmin:jasmin/eclib -I common -I mlkem
 
 [test-specs]
-okdirs  = common ml-kem/ ml-kem/properties fips202 fips202/properties
+okdirs = !common !fips202 !ml-kem

easycrypt.project

@@ -5,8 +5,7 @@ provers = [email protected]
 provers = [email protected]
 provers = [email protected]
 
+rdirs = Jasmin:jasmin/eclib
 rdirs = common
-idirs = fips202
-idirs = fips202/properties
-idirs = ml-kem
-idirs = ml-kem/properties
+rdirs = fips202
+rdirs = ml-kem

kyber768/properties/Correctness.ec

@@ -48,7 +48,7 @@ by smt(rg_asint).
 (* Compress-error bound *)
 op Bq d = round (q%r / (2^(d+1))%r).
 
-lemma nosmt Bq_le_half d:
+lemma Bq_le_half d:
  0 < d =>
  (q%r / (2^(d+1))%r) <= (q-1)%r/2%r.
 proof.
@@ -60,7 +60,7 @@ rewrite (RField.mulrC (2%r)) invrM;1,2:by smt(lt_pow expr_gt0).
 by rewrite RField.mulrC (RField.mulrA (q%r)) (RField.mulrC (q%r)) !RField.mulrA /#.
 qed.
 
-lemma nosmt dvdzN_q_2d (d: int):
+lemma dvdzN_q_2d (d: int):
  0 < d =>
  q %% 2^d <> 0.
 proof.
@@ -73,7 +73,7 @@ move: (IH HHd); apply contra.
 by rewrite -!dvdzE /#.
 qed.
 
-lemma nosmt Bq_noties d:
+lemma Bq_noties d:
  0 < d =>
  2^d < q =>
  frac (q%r / (2 ^ (d + 1))%r) <> inv 2%r.
@@ -88,24 +88,24 @@ rewrite !mulrA divrr //= frac_div_eq0.
 by apply dvdzN_q_2d.
 qed.
 
-lemma nosmt Bq1E: Bq 1 = 832
+lemma Bq1E: Bq 1 = 832
 by rewrite /Bq /= round_divz 1:// qE.
 
-lemma nosmt Bq4E: Bq 4 = 104
+lemma Bq4E: Bq 4 = 104
 by rewrite /Bq /= round_divz 1:// qE.
 
 (* Compression and decompression are used as operations between 
    polynomials over coeff, but we first define the basic operations 
    over coefficients. *)
 
-lemma nosmt comp_bound d x:
+lemma comp_bound d x:
  0 < d =>
  2^d < q =>
  x * (2 ^ d)%r / q%r - inv 2%r
  < (comp d x)%r <= x * (2 ^ d)%r / q%r + inv 2%r.
 proof. smt(round_bound). qed.
 
-lemma nosmt comp_asint_bound d x:
+lemma comp_asint_bound d x:
  0 < d =>
  2^d < q =>
  (asint x)%r * (2 ^ d)%r - q%r / 2%r < q%r * (comp d (asint x)%r)%r
@@ -126,7 +126,7 @@ apply (RealOrder.ler_lt_trans ((asint x)%r*(2^d)%r/q%r+ inv 2%r)); first smt(com
 by rewrite RealOrder.ltr_add2r RealOrder.ltr_pmul2r 1:/# RealOrder.ltr_pmul2r; smt(expr_gt0 rg_asint).
 qed.
 
-lemma nosmt comp_over d x:
+lemma comp_over d x:
  0 < d =>
  2^d < q =>
  comp d (asint x)%r = 2^d
@@ -141,7 +141,7 @@ rewrite RealOrder.ler_subl_addl -RealOrder.ler_subl_addr ler_pdivl_mulr.
 by rewrite exprD_nneg 1..2:/# /= fromintM /#.
 qed.
 
-lemma nosmt compress0L d x:
+lemma compress0L d x:
  0 < d =>
  2^d < q =>
  q%r - q%r / (2^(d+1))%r <= (asint x)%r =>
@@ -153,7 +153,7 @@ have ->: comp d (asint x)%r = 2^d.
 by rewrite modzz.
 qed.
 
-lemma nosmt compress_small d x:
+lemma compress_small d x:
  0 < d =>
  2^d < q =>
  (asint x)%r < q%r - q%r / (2^(d+1))%r =>
@@ -167,7 +167,7 @@ have ?: comp d (asint x)%r <> 2^d by rewrite comp_over // /#.
 smt(comp_asint_range).
 qed.
 
-lemma nosmt compress1_is0 x:
+lemma compress1_is0 x:
  compress 1 x = 0 <=> absZq x <= Bq 1.
 proof.
 have L: forall y m, 0 <= y <= m => y %% m = 0 <=> y=0 \/ y=m.

kyber768/properties/KyberLib.ec

@@ -16,11 +16,11 @@ rewrite (floorE (x+floor y)) //.
 smt(floor_bound).
 qed.
 
-lemma nosmt le_floorE n x:
+lemma le_floorE n x:
  (n <= floor x) = (n%r <= x)
 by smt(floor_bound).
 
-lemma nosmt floor_ltE x n:
+lemma floor_ltE x n:
  (floor x < n) = (x < n%r)
 by smt(floor_bound).
 
@@ -137,16 +137,16 @@ lemma round_bound x:
  x - inv(2%r) < (round x)%r <= x + inv(2%r)
 by smt(floor_bound).
 
-lemma nosmt le_roundE n x:
+lemma le_roundE n x:
  (n <= round x) = (n%r <= x + inv 2%r)
 by smt(le_floorE).
 
-lemma nosmt round_ltE x n:
+lemma round_ltE x n:
  (round x < n) = (x + inv 2%r < n%r)
 by smt(floor_ltE).
 
 
-lemma nosmt roundN x:
+lemma roundN x:
  frac x <> inv 2%r => round (-x) = -round x.
 proof.
 move => H.