Skip to content

Actions: formosa-crypto/formosa-mlkem

Actions

Extract & Check proofs

Actions

Loading...
Loading

Show workflow options

Create status badge

Loading
extract-and-prove.yml
192 workflow runs
192 workflow runs

Filter by Event

Filter by Status

Filter by Branch

Filter by Actor

Removed spurious smt. Extract & Check proofs #42: Commit 5ae4142 pushed by mbbarbosa
May 17, 2024 16:14 1m 21s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
May 17, 2024 16:14 1m 21s
New file just for genmatrix Extract & Check proofs #41: Commit 071b898 pushed by mbbarbosa
May 16, 2024 16:54 3m 8s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
May 16, 2024 16:54 3m 8s
Execute ML-KEM implementations in the Jasmin interpreter (#37) Extract & Check proofs #40: Commit 3e8b6ba pushed by bgregoir
May 14, 2024 12:52 2h 18m 9s master
master
May 14, 2024 12:52 2h 18m 9s
Execute ML-KEM implementations in the Jasmin interpreter Extract & Check proofs #39: Pull request #37 opened by vbgl
May 6, 2024 11:53 2h 16m 45s vbgl:exec
vbgl:exec
May 6, 2024 11:53 2h 16m 45s
Proof working with microarch protections Extract & Check proofs #38: Commit 08b34df pushed by mbbarbosa
April 29, 2024 13:27 2m 52s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
April 29, 2024 13:27 2m 52s
Use latest Jasmin release (2023.06.3) Extract & Check proofs #37: Commit 1cc454f pushed by vbgl
April 19, 2024 11:50 2h 16m 28s master
master
April 19, 2024 11:50 2h 16m 28s
Use latest Jasmin release (2023.06.3) Extract & Check proofs #36: Pull request #36 synchronize by vbgl
April 18, 2024 15:53 2h 22m 41s vbgl:jasmin-2023.06.3
vbgl:jasmin-2023.06.3
April 18, 2024 15:53 2h 22m 41s
fix mlkem768 sct : using https://github.com/jasmin-lang/jasmin/pull/785 Extract & Check proofs #35: Commit b807810 pushed by tfaoliveira-sb
April 18, 2024 11:28 2m 52s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
April 18, 2024 11:28 2m 52s
Use latest Jasmin release (2023.06.3) Extract & Check proofs #34: Pull request #36 synchronize by vbgl
April 17, 2024 07:50 2h 21m 26s vbgl:jasmin-2023.06.3
vbgl:jasmin-2023.06.3
April 17, 2024 07:50 2h 21m 26s
Use latest Jasmin release (2023.06.3) Extract & Check proofs #33: Pull request #36 opened by vbgl
April 17, 2024 06:31 2h 18m 0s vbgl:jasmin-2023.06.3
vbgl:jasmin-2023.06.3
April 17, 2024 06:31 2h 18m 0s
Fix w.r.t. EasyCrypt c0e1455 Extract & Check proofs #32: Commit 7222f3f pushed by strub
April 13, 2024 15:07 2h 22m 19s master
master
April 13, 2024 15:07 2h 22m 19s
Fix w.r.t. EasyCrypt c0e1455 Extract & Check proofs #31: Pull request #35 opened by strub
April 13, 2024 12:46 2h 19m 57s strub:fix-ec-13-april-2024
strub:fix-ec-13-april-2024
April 13, 2024 12:46 2h 19m 57s
mlkem ref sct: remove temporary(wip) init_msf Extract & Check proofs #30: Commit 8a1fc0f pushed by tfaoliveira-sb
April 10, 2024 08:12 1m 32s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
April 10, 2024 08:12 1m 32s
mlkem768 ref sct: work in progress - recording the state to try a dif… Extract & Check proofs #29: Commit 97cc863 pushed by tfaoliveira-sb
April 9, 2024 17:42 1m 22s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
April 9, 2024 17:42 1m 22s
synch with crypto-specs Extract & Check proofs #28: Commit 5c14571 pushed by mbbarbosa
April 5, 2024 22:19 1m 31s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
April 5, 2024 22:19 1m 31s
Removed H-related axiom Extract & Check proofs #27: Commit 0fd1d9b pushed by mbbarbosa
April 5, 2024 21:40 1m 15s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
April 5, 2024 21:40 1m 15s
Fixed failing smt Extract & Check proofs #26: Commit 3b2e937 pushed by mbbarbosa
April 5, 2024 20:12 1m 33s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
April 5, 2024 20:12 1m 33s
Preparing for avx2 proof Extract & Check proofs #25: Commit 18351a2 pushed by mbbarbosa
April 4, 2024 21:43 2m 48s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
April 4, 2024 21:43 2m 48s
Preparing for avx2 proof Extract & Check proofs #24: Commit 583a438 pushed by mbbarbosa
April 4, 2024 21:42 2m 53s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
April 4, 2024 21:42 2m 53s
keypair: spare a few additions Extract & Check proofs #23: Commit 643103e pushed by vbgl
March 27, 2024 10:25 2h 19m 4s master
master
March 27, 2024 10:25 2h 19m 4s
keypair: spare a few additions Extract & Check proofs #22: Pull request #28 synchronize by vbgl
March 27, 2024 05:34 2h 20m 21s vbgl:2024-02-14
vbgl:2024-02-14
March 27, 2024 05:34 2h 20m 21s
mlkem768 avx2 - updated gen matrix + SCT Extract & Check proofs #21: Pull request #32 synchronize by mbbarbosa
March 25, 2024 10:27 1m 17s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
March 25, 2024 10:27 1m 17s
only matrix sampling to prove Extract & Check proofs #20: Commit 664fd37 pushed by mbbarbosa
March 25, 2024 10:27 2m 53s mlkem768_avx2_gen_matrix_sct
mlkem768_avx2_gen_matrix_sct
March 25, 2024 10:27 2m 53s
Added LICENSE information; required for consumption by libjade Extract & Check proofs #19: Commit 3bd9229 pushed by cryptojedi
March 24, 2024 18:51 2h 17m 49s master
master
March 24, 2024 18:51 2h 17m 49s
Use alt-ergo 2.5 Extract & Check proofs #18: Commit 335417e pushed by vbgl
March 20, 2024 06:11 2h 26m 16s master
master
March 20, 2024 06:11 2h 26m 16s