Sha3 lax check #1092

Parrot7483 · 2025-08-08T13:12:36Z

This PR adds lax checking for SHA3. It also includes some changes towards full type checking. The theta, pi and chi functions are admitted.

It is based on my develop branch which changes are requested in PR 1076

franziskuskiefer

Thanks!

I only looked at the Rust changes and not inside the hax/F* blobs.

fstar-helpers/core-models/src/abstractions/bitvec.rs

libcrux-intrinsics/src/avx2.rs

libcrux-sha3/src/traits.rs

libcrux-sha3/Cargo.toml

libcrux-sha3/src/lib.rs

libcrux-sha3/src/generic_keccak.rs

libcrux-sha3/src/simd/portable.rs

libcrux-sha3/src/generic_keccak/xof.rs

Parrot7483 · 2025-08-19T11:26:45Z

One problem is this issue. I always get the wrong explicit_panic in F*.

Parrot7483 · 2025-08-19T14:10:01Z

One problem is this issue. I always get the wrong explicit_panic in F*.

Fixed in HAX cryspen/hax@ad0e608

franziskuskiefer

It looks like you force pushed. That breaks the entire review process. Please don't force push during the review.

Also, please enable laxing to the CI so that we don't break it again.
Then I think this is good to go.

libcrux-sha3/src/generic_keccak.rs

libcrux-sha3/src/traits.rs

Parrot7483 · 2025-08-20T08:47:31Z

It looks like you force pushed. That breaks the entire review process. Please don't force push during the review.

Yes, sorry. I rebased because I wanted the Makefile changes to be merged separately.

Parrot7483 · 2025-08-21T08:33:55Z

The new CI does not work with the Makefile. Will investigate. My first time working with Github workflows.

Parrot7483 · 2025-09-02T08:33:49Z

CI still fails because hax-lib is pulled from

--include /home/runner/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/hax-lib-0.3.2/proof-libs/fstar/core 
--include /home/runner/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/hax-lib-0.3.2/proof-libs/fstar/rust_primitives 
--include /home/runner/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/hax-lib-0.3.2/proofs/fstar/extraction

W95Psp · 2025-09-02T12:39:22Z

As we discussed on Google Chat, the problem here probably has nothing to do with the hax installation action.
The Makefile of F* will ask cargo for the path in which it has to find hax-lib.
So here, I believe you should just pin hax-lib in Cargo.toml to the git commit you want to use.

Does that make sense?

Parrot7483 · 2025-09-02T13:43:32Z

The Makefile.base automatically finds hax-lib/proofs-lib/fstar/code twice. That's why I use the HAX_HOME variable in the SHA3 Makefile

--include /home/runner/.cargo/git/checkouts/hax-580ebeee043cdea1/6b34a68/hax-lib/proof-libs/fstar/core
--include /home/runner/.cargo/git/checkouts/hax-580ebeee043cdea1/6b34a68/hax-lib/proof-libs/fstar/rust_primitives
--include /home/runner/.cargo/git/checkouts/hax-580ebeee043cdea1/6b34a68/hax-lib/proofs/fstar/extraction
--include /home/runner/.cargo/registry/src/index.crates.io-1949cf8c6b5b557f/hax-lib-0.3.2/proof-libs/fstar/core

cargo tree --invert registry+https://github.com/rust-lang/crates.io-index#[email protected]
+ command cargo tree --invert registry+https://github.com/rust-lang/crates.io-index#[email protected]
hax-lib v0.3.2
├── libcrux-intrinsics v0.0.3 (/home/tristan/Repositories/libcrux/libcrux-intrinsics)
│   └── libcrux-sha3 v0.0.3 (/home/tristan/Repositories/libcrux/libcrux-sha3)
└── libcrux-secrets v0.0.3 (/home/tristan/Repositories/libcrux/secrets)
    └── libcrux-traits v0.0.3 (/home/tristan/Repositories/libcrux/traits)
        └── libcrux-sha3 v0.0.3 (/home/tristan/Repositories/libcrux/libcrux-sha3)

cargo tree --invert git+https://github.com/cryspen/hax.git?rev=6b34a68a0b38cd2aff09a4ad05569d712620af27#[email protected]
+ command cargo tree --invert 'git+https://github.com/cryspen/hax.git?rev=6b34a68a0b38cd2aff09a4ad05569d712620af27#[email protected]'
hax-lib v0.3.2 (https://github.com/cryspen/hax.git?rev=6b34a68a0b38cd2aff09a4ad05569d712620af27#6b34a68a)
└── libcrux-sha3 v0.0.3 (/home/tristan/Repositories/libcrux/libcrux-sha3)

W95Psp · 2025-09-02T14:01:08Z

Oh, I see, I recall your PR introducing HAX_HOME in the README.
I think this is not so great: now, you can have a Rust hax-lib inconsistant with the F* hax-lib.

Looking at the commit change, I don't see where HAX_HOME is supposed to be defined, in CI.
The libcrux jobs CI are not using the flake.nix from this repo.

Parrot7483 · 2025-09-02T14:46:19Z

I changed the version of hax-lib in root Cargo.toml to use the latest commit. Only using latest version of hax-lib in libcrux-sha3/Cargo.toml causes the Makefile.generic to find different versions of hax-lib and then verification fails.

What do you think @franziskuskiefer

franziskuskiefer · 2025-09-03T06:25:28Z

I changed the version of hax-lib in root Cargo.toml to use the latest commit. Only using latest version of hax-lib in libcrux-sha3/Cargo.toml causes the Makefile.generic to find different versions of hax-lib and then verification fails.

What do you think @franziskuskiefer

That's ok to get this in. But please file a follow-up issue to get this fixed.

Also, we need to get the hax action fixed to avoid this hack. I filed hacspec/hax-actions#5 for that.

W95Psp · 2025-09-03T06:38:35Z

Thanks for filing the issue, Franziskus, I replied there. I believe this isn’t something the action can address, as it works as intended in this case.
What F* library picked is decided by the Makefile that lives in this repo, the action has no power over it.

IMO, the way to improve things here is to allocate time on the workbench to kill makefiles altogether.

franziskuskiefer · 2025-09-03T06:40:43Z

Ok, then we'll have to get this fixed in here properly before we can merge it.

W95Psp · 2025-09-03T15:09:51Z

You can now update hax-lib to 0.3.4, hax was released.

Parrot7483 · 2025-09-03T15:33:38Z

I created a separate bump #1127.

I will clean up the last couple commits and rebase.

- add a `--portable` flag for extract in the python build script - add a `clean` option to the python build script - remove F* interface generation - add a Makefile for verification - remove non default interative prove config - change .gitignore

franziskuskiefer

Thanks, almost there. Just a few nits, then we can get this in.

libcrux-sha3/Cargo.toml

libcrux-sha3/src/traits.rs

.github/workflows/sha3-hax.yml

- typo - yml formatting - add workflow path - remove libcrux-traits feature - remove sha3-extract-portable-hax-status

franziskuskiefer

One last thing (that would fail ci)

libcrux-sha3/src/lib.rs

franziskuskiefer

Thanks! Let's get this in.

Parrot7483 · 2025-09-10T19:14:09Z

I don't see an error in the log that failed. What is the problem here?

franziskuskiefer · 2025-09-11T06:28:36Z

Looks like the branch is pretty out of date. Updating may fix it. If not, C extraction must be updated.

Parrot7483 requested review from a team as code owners August 8, 2025 13:12

Parrot7483 requested review from jschneider-bensch, franziskuskiefer and karthikbhargavan and removed request for jschneider-bensch August 8, 2025 13:12

franziskuskiefer mentioned this pull request Aug 11, 2025

Verify libcrux-sha3 #395

Open

franziskuskiefer requested changes Aug 11, 2025

View reviewed changes

franziskuskiefer assigned Parrot7483 Aug 18, 2025

Parrot7483 requested a review from franziskuskiefer August 19, 2025 11:20

Parrot7483 force-pushed the sha3-lax-check branch from 087bfc8 to 4f45356 Compare August 19, 2025 11:23

Parrot7483 mentioned this pull request Aug 19, 2025

Makefile improvement #1101

Merged

Parrot7483 force-pushed the sha3-lax-check branch from 4f45356 to 25962c8 Compare August 20, 2025 08:26

franziskuskiefer requested changes Aug 20, 2025

View reviewed changes

libcrux-sha3/src/generic_keccak.rs Show resolved Hide resolved

libcrux-sha3/src/traits.rs Show resolved Hide resolved

Parrot7483 mentioned this pull request Sep 3, 2025

Makefile.generic discovers multiple versions of hax-lib #1125

Open

Add HAX_HOME env variable & jq dependency to nix flake

a17b38f

Parrot7483 added 7 commits September 5, 2025 12:01

Update flake HAX input

4573748

Init Lax Check SHA3

e21c9c0

- add a `--portable` flag for extract in the python build script - add a `clean` option to the python build script - remove F* interface generation - add a Makefile for verification - remove non default interative prove config - change .gitignore

Fix type errors

2da85bf

Fix build warnings. Removes extra parentheses. Allow unused unsafe.

3784772

Split rho and theta function

4368928

Apply feedback

b14c179

Add feature for Digest Trait in SHA3

d750ab1

Parrot7483 force-pushed the sha3-lax-check branch from d1b7358 to d750ab1 Compare September 5, 2025 10:06

Parrot7483 requested a review from franziskuskiefer September 5, 2025 12:01

franziskuskiefer requested changes Sep 8, 2025

View reviewed changes

Apply feedback from Franziskus

96e02cb

- typo - yml formatting - add workflow path - remove libcrux-traits feature - remove sha3-extract-portable-hax-status

Parrot7483 requested review from franziskuskiefer and removed request for karthikbhargavan September 8, 2025 09:14

franziskuskiefer requested changes Sep 10, 2025

View reviewed changes

libcrux-sha3/src/lib.rs Outdated Show resolved Hide resolved

Exclude impl_digest_trait when either hax or eurydice is enabled

91fbd22

franziskuskiefer approved these changes Sep 10, 2025

View reviewed changes

Parrot7483 added this pull request to the merge queue Sep 10, 2025

github-merge-queue bot removed this pull request from the merge queue due to failed status checks Sep 10, 2025

Merge branch 'main' into sha3-lax-check

ae00be9

franziskuskiefer enabled auto-merge September 11, 2025 06:28

franziskuskiefer added this pull request to the merge queue Sep 11, 2025

github-merge-queue bot removed this pull request from the merge queue due to failed status checks Sep 11, 2025

c: update extraction

62f3a5f

franziskuskiefer enabled auto-merge September 11, 2025 07:32

franziskuskiefer added this pull request to the merge queue Sep 11, 2025

Merged via the queue into cryspen:main with commit 4f028e0 Sep 11, 2025
102 checks passed

Parrot7483 deleted the sha3-lax-check branch September 11, 2025 08:27

Sha3 lax check #1092

Sha3 lax check #1092

Uh oh!

Conversation

Parrot7483 commented Aug 8, 2025

Uh oh!

franziskuskiefer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Parrot7483 commented Aug 19, 2025

Uh oh!

Parrot7483 commented Aug 19, 2025

Uh oh!

franziskuskiefer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Parrot7483 commented Aug 20, 2025

Uh oh!

Parrot7483 commented Aug 21, 2025

Uh oh!

Parrot7483 commented Sep 2, 2025

Uh oh!

W95Psp commented Sep 2, 2025

Uh oh!

Parrot7483 commented Sep 2, 2025

Uh oh!

W95Psp commented Sep 2, 2025

Uh oh!

Parrot7483 commented Sep 2, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

franziskuskiefer commented Sep 3, 2025

Uh oh!

W95Psp commented Sep 3, 2025

Uh oh!

franziskuskiefer commented Sep 3, 2025

Uh oh!

W95Psp commented Sep 3, 2025

Uh oh!

Parrot7483 commented Sep 3, 2025

Uh oh!

franziskuskiefer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

franziskuskiefer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

franziskuskiefer left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Parrot7483 commented Sep 10, 2025

Uh oh!

franziskuskiefer commented Sep 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Parrot7483 commented Sep 2, 2025 •

edited

Loading

franziskuskiefer commented Sep 11, 2025 •

edited

Loading