Add equivalence lemma for `montgomery_multuiply` #975

W95Psp · 2025-05-19T10:01:50Z

This PR:

backport some improvements to the flattening tactic
adds a lemma proving pointwise equivalence for montgomery_multiply.

Related to #908.

This commit backports the following commits from `cryspen/core-models`: commit 76a33e9e7aa7328226ebc790d30f3d29e0e062fa Author: Lucas Franceschino <[email protected]> Date: Mon May 19 07:00:52 2025 +0000 Tactics.Circuit: intro `unapply` tactic commit 8973fcee991752427eef2f00b68ecf7c93451587 Author: Lucas Franceschino <[email protected]> Date: Mon May 19 07:00:18 2025 +0000 Tactics.Circuit: derive pointwise lemmas (e.g. from `f == g`, derive `forall x. f x == g x`) commit 52ed360e5ce8fb961530ef01f3d6d196d61f87f2 Author: Lucas Franceschino <[email protected]> Date: Mon May 19 09:06:25 2025 +0200 F*: tweak: isolate `i32_extended64_mul` in its own function commit 2d787098d8c87ccf1f1408505c29a4c056d6e69b Author: Lucas Franceschino <[email protected]> Date: Mon May 19 09:06:06 2025 +0200 tweak lemmas with SMTPats commit 5ec1fc5b4d7d2d9b9e81e8f2fa6761d2e5d388f3 Author: Lucas Franceschino <[email protected]> Date: Mon May 19 09:05:44 2025 +0200 funarray: use newtype instead of type synonym commit f18783b60dfdbcb1fed92e2734616c608ae02306 Author: Lucas Franceschino <[email protected]> Date: Mon May 19 06:54:51 2025 +0000 Tactics.Circuits: unfold local crate as well commit ead0c5c8175e699fd7bf8a782f2d21e584a3c431 Author: Lucas Franceschino <[email protected]> Date: Mon May 19 06:54:22 2025 +0000 inversion lemmas: add smtpat commit f6a51c36bc2025100e93c392bea438a9b97999ff Merge: 17098d3 8043c02 Author: Aniket Mishra <[email protected]> Date: Mon May 19 10:49:02 2025 +0530 Merge pull request #13 from cryspen-ext/lf-misc Miscellaneous changes, toward NTT verification in libcrux commit 8043c023973591e02389600e10c236573e82940e Author: Lucas Franceschino <[email protected]> Date: Thu May 15 09:35:50 2025 +0000 fix F* typo commit 4883b7c7e570d9226c70a5efea6f7fccb1f3e982 Author: Lucas Franceschino <[email protected]> Date: Thu May 15 09:34:09 2025 +0000 no need for preconditions commit b4fa7d4f9b8d87343dbdce93c35ffaf98108ae34 Author: Lucas Franceschino <[email protected]> Date: Thu May 15 07:09:08 2025 +0000 always apply the tactic commit d3f6d35bbfed8a2aacf6fd443bc9dd6ffa7ca669 Author: Lucas Franceschino <[email protected]> Date: Thu May 15 06:54:43 2025 +0000 cargo lock commit a2741fc1be036d73af6ea2bf428c7eeffff1f8ae Author: Lucas Franceschino <[email protected]> Date: Thu May 15 06:54:28 2025 +0000 _mm256_set_epi32: give a interpretation only pointwise commit 5ba1a644a78a463c84a3d28b764268f2999d64cd Author: Lucas Franceschino <[email protected]> Date: Thu May 15 06:53:11 2025 +0000 add lemma for conv simplification using into_i32x8 commit 2fb2a03fe594df872dd387777d72b1a310c2b1e5 Author: Lucas Franceschino <[email protected]> Date: Thu May 15 06:52:21 2025 +0000 add direct conversion tests commit 21c8668488dbd329e34a7664e6a5f8b69b9aef04 Author: Lucas Franceschino <[email protected]> Date: Thu May 15 06:52:02 2025 +0000 add convertion `into_i64x4` commit ae378b2ecd65dbcc39f4240c59b1585c87d15916 Author: Lucas Franceschino <[email protected]> Date: Thu May 15 06:48:58 2025 +0000 intro `helpers.rs`, move `HasRandom` commit ebdb0b68e3002dca6df891b858fccc3bbea6c05d Author: Lucas Franceschino <[email protected]> Date: Thu May 15 06:40:39 2025 +0000 use inherent method instead of `From` instances This is very helpful for F*: - it kills many uses of typeclasses, making normalization much much faster (about 10 times!) - names are explicit, so it's easier to debug commit 7e77a031e6fc4d5cc94d29f6c3b1163c55ad2db2 Author: Lucas Franceschino <[email protected]> Date: Wed May 14 12:52:44 2025 +0000 add _mm256_set_epi32 commit aaef66a86aa9b6dd38bcdee7f3b007963c62c781 Author: Lucas Franceschino <[email protected]> Date: Wed May 14 12:52:14 2025 +0000 add simplification lemma for trivial from commit 17098d3273b6efb2052f340deebc76d8f795bf07 Merge: 6ad06c4 25d8747 Author: Aniket Mishra <[email protected]> Date: Wed May 14 14:16:06 2025 +0530 Merge pull request #11 from cryspen-ext/add-raw-ptr-intrinsics Add missing raw pointer based intrinsics commit 25d874765c7d00ce313612dbc58a3deaa5651449 Author: Lucas Franceschino <[email protected]> Date: Wed May 14 08:22:08 2025 +0000 add missing raw pointer based intrinsics commit 6ad06c4cc0b25904252c93a20b0fa83cfac9526a Merge: cdfb1d9 58cbdcf Author: Aniket Mishra <[email protected]> Date: Wed May 14 12:54:58 2025 +0530 Merge pull request #10 from cryspen-ext/lemma-fixes fix misc small mistakes in lemmas commit 58cbdcffe5299152650ac6de2f2fd62d24b795d2 Author: Lucas Franceschino <[email protected]> Date: Wed May 14 07:11:58 2025 +0000 fix misc small mistakes in lemmas commit cdfb1d9b963380f257ec66fb87cc27a405ae146f Author: Lucas Franceschino <[email protected]> Date: Wed May 14 06:56:32 2025 +0000 rustfmt commit c7a38f78a22df80d9e29dc633be5b385e7d938c4 Merge: af5b21e 12c700d Author: Aniket Mishra <[email protected]> Date: Tue May 13 21:59:26 2025 +0530 Merge pull request #9 from cryspen-ext/lemma-quick-fix Added a missing lift lemma commit 12c700dab09cc64502207c3e62c25b61fe020caa Author: satiscugcat <[email protected]> Date: Tue May 13 21:51:02 2025 +0530 Added a missing lift lemma commit af5b21efa11dd6528ed9d70213cbdb0d8a78a0e3 Merge: 1c135b8 f761579 Author: Aniket Mishra <[email protected]> Date: Tue May 13 21:41:15 2025 +0530 Merge pull request #6 from cryspen-ext/fstar-tc Make F* typecheck commit f761579d30e7b8e2ebd3bc30147599a0ad40d4a1 Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:51:53 2025 +0000 gitignore: ignore F* cache files commit a15fd702f743e82f07cabdece93e8559065b47cd Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:51:04 2025 +0000 add `Tactics.Circuits.fst` commit 618d6b25d53e52e1ff3d451efe71368780e13bde Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:50:34 2025 +0000 remnove the extraction of Opaque as well commit 85dd39685c158be98a836ada271d62cf79e51f0f Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:49:38 2025 +0000 `hax.sh`: add a default z3rlimit to 80 commit 824a6fa44d8f475c43a6b5d02dc7baeccfff009c Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:49:10 2025 +0000 fix: move makefile to the right place commit e9537cedbfea53f5c2f245e50964b84625974287 Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:45:04 2025 +0000 add missing import (it is missing only when extracting with hax) commit 94aac4d5fb58374fdf81b68b1f4c4f07de1dd4f3 Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:44:39 2025 +0000 fixme: mark two intrinsics as lax commit 71b76ccf6bc57576e6af69a119ee23aec8f15335 Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:43:57 2025 +0000 inline constants: this helps F* commit 7615d8b846701a7aa4fc1182fb92479120139e66 Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:41:34 2025 +0000 use rem_euclid, not `%` commit 1fb107539ca6cb45071f122a7477480ba813e4c2 Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:40:00 2025 +0000 fix a few intrinsics edge cases commit 2dd907cae9597b826162aea68cd8e3cd047b4c84 Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:39:19 2025 +0000 avoid comparing bitvecs: use a fold to detect zeros instead commit 7f3a921e3c09b313b1313448a4cf8afce1bd4f65 Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:37:33 2025 +0000 feat(bitvec): add `fold` commit d1135334efa32335bd9f56c406f31a1cef73d11b Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:37:06 2025 +0000 use unreachable, not panic commit fc93714e4154195a0a343be38bfcdba52f8aa5ac Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:36:23 2025 +0000 rename remaining Minicore into Core_Models commit 3f0a6afafaa59f66b72c5f282ce826d7176f1b6c Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:35:20 2025 +0000 fix bug of `from` impl for int vecs commit 8878944565b9d36b4ba9baf6ead2fca6fb58f19b Author: Lucas Franceschino <[email protected]> Date: Tue May 13 14:34:37 2025 +0000 remove unused `MIN` and `MAX` constants on `MachineInteger` trait commit 1c135b8c08d9cfbf0a03cd8b1c928ee850081cc1 Merge: d10567b 78785c4 Author: Lucas Franceschino <[email protected]> Date: Tue May 13 16:48:19 2025 +0200 Merge pull request #8 from cryspen-ext/add-lift-lemmas-aux Add lift lemmas aux commit 78785c470088a299c9fc03b78b78aa43044cb43d Author: satiscugcat <[email protected]> Date: Tue May 13 18:12:21 2025 +0530 Added lift lemmas for interpretations, definitions that are just done with BitVec still need their bodies copied into x86.rs commit 99893629259b78c8de54064baf9163c364d96a08 Author: satiscugcat <[email protected]> Date: Tue May 13 13:56:15 2025 +0530 Fixed formatting issue commit d10567b78809f04a94250900cbeeacb9ad8f1abc Merge: 9453fee ecc67e9 Author: Lucas Franceschino <[email protected]> Date: Mon May 12 14:05:42 2025 +0200 Merge pull request #3 from cryspen-ext/add-makefile Add F* makefile commit 9453feedc0d43054bbc8670987e184711915f254 Merge: d6dd609 829e9ad Author: Aniket Mishra <[email protected]> Date: Mon May 12 17:30:06 2025 +0530 Merge pull request #1 from cryspen-ext/libcrux-port Porting over minicore from cryspen/libcrux, all the functions that have been specified in its opaque.rs have interpretations. Yet to add extraction support, yet to look at libcrux-intrinsics commit 829e9ad8e00644372a667ea115642ad3a2362c90 Author: satiscugcat <[email protected]> Date: Mon May 12 16:10:23 2025 +0530 Formatting works now! Added #[rustfmt::skip] before the two functions that were causing issues commit 4215890400747c4ee54b1dc6ebb50c088854e6fa Author: satiscugcat <[email protected]> Date: Mon May 12 15:06:52 2025 +0530 Removed reference to opaque in x86 commit 7944d6bd81935e3701e438cc71af477b87734665 Author: satiscugcat <[email protected]> Date: Mon May 12 15:04:40 2025 +0530 Removed comments from shell script, deleted opaque.rs commit eb70da1b1cc5ec06609cc4ff8c55a67238a68249 Author: satiscugcat <[email protected]> Date: Mon May 12 14:43:03 2025 +0530 Moving functions from avx2 into appropriate modules commit f9e1f93770d4bf3492a7c2f47415d307348c51f7 Author: satiscugcat <[email protected]> Date: Mon May 12 13:36:17 2025 +0530 Quick fixes, fold and test comments commit 968ff662963191c3bfd573908a53685722561dc3 Author: satiscugcat <[email protected]> Date: Fri May 9 14:06:48 2025 +0530 Added some more missing documentation commit 718767dfe711dd2121f88ee38931f7871f9277c9 Author: satiscugcat <[email protected]> Date: Fri May 9 13:57:37 2025 +0530 Documentation added! commit 334155dcac3961fe5288754e6a23b80005c4004c Author: satiscugcat <[email protected]> Date: Fri May 9 13:22:40 2025 +0530 All functions implemented! Extraction support left, addition to avx2 module left commit 45f5465594b4c96b9ac976c6b4494b16ef818c5e Author: satiscugcat <[email protected]> Date: Thu May 8 16:46:38 2025 +0530 Some cleanup commit 786603b580c93758c4bf4d8a2d202e7ca84ee337 Author: karthikbhargavan <[email protected]> Date: Wed May 7 13:46:11 2025 +0000 tests commit 1765f1382ea8114ac8b5ded29424ef6eace4a681 Author: satiscugcat <[email protected]> Date: Wed May 7 17:35:55 2025 +0530 Weird bsrli behaviour commit 1152554a1aa0053fb9fb67c651e2a8a48cbb8e9e Author: karthikbhargavan <[email protected]> Date: Wed May 7 10:52:58 2025 +0000 progress commit b31774e615085aa2f24b771c1ea25df4130f367a Author: satiscugcat <[email protected]> Date: Wed May 7 14:44:06 2025 +0530 Committing code with tests that are expected to fail commit 3fdb878b83fe026cc34f72df5721c042c7b9a275 Author: satiscugcat <[email protected]> Date: Mon May 5 20:51:29 2025 +0530 Removing target from the github repo commit ce8a5d381175acefcd544f43c793b2ba308b4102 Author: satiscugcat <[email protected]> Date: Mon May 5 20:43:18 2025 +0530 Libcrux port in progress, have not added support for extraction yet, but should not be too difficult commit 587015d930f11749eac3e1aa5fddeabcba93ae55 Author: satiscugcat <[email protected]> Date: Fri May 2 15:50:09 2025 +0530 Porting over stuff from libcrux minicore, yet to add fstar shell scripts and such commit ecc67e96cbd1140f4d0c86d912952b3cd5bd7d3c Author: Lucas Franceschino <[email protected]> Date: Mon May 12 13:37:09 2025 +0200 Cargo.toml: do not pin a version for hax-lib We use a git dependency, adding a version here is not useful and will break on updates. commit 7873184b8b3e8c164278d6cd991e20021327c87f Author: Lucas Franceschino <[email protected]> Date: Mon May 12 13:35:55 2025 +0200 Add F* makefile This PR adds a F* makefile so that we can typecheck core-models easily. commit d6dd6094cd14d326a6e818510c32a78562c5948d Author: satiscugcat <[email protected]> Date: Fri May 2 15:50:09 2025 +0530 Porting over stuff from libcrux minicore, yet to add fstar shell scripts and such commit 5901cf0e225c00734b03617c25c34bdc3e05a7ef Author: karthikbhargavan <[email protected]> Date: Fri May 2 09:42:20 2025 +0200 Initial commit

…fstar/extraction`

`core-models` now models (or declare) most avx2 intrinsics used in libcrux-intrinscs

W95Psp · 2025-05-21T08:03:40Z

This PR will conflict with #988.
Let's wait for #988 to be merged before mergining that one.
It will be easier to fix in this direction.

franziskuskiefer · 2025-05-22T06:46:11Z

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

-                        fn from(bv: BitVec<$n>) -> Self {
-                            let vec: Vec<$ty> = bv.to_vec();
-                            Self::from_fn(|i| vec[i as usize])
+                pastey::paste! {


I don't think this is good and readable code.

It seems the only reason you need pastey here is because you want to concatenate names. But why do you need those names? And how much additional code would you have to write without?

franziskuskiefer · 2025-05-22T06:49:05Z

fstar-helpers/core-models/src/core_arch/x86/interpretations.rs

+            } else {
+                if b[i - 8] > (i8::MAX as i16) {


Why do you use nested blocks instead of else if?

franziskuskiefer · 2025-05-22T06:50:09Z

fstar-helpers/core-models/src/core_arch/x86/interpretations.rs

@@ -28,18 +36,509 @@ pub mod int_vec {
    }

    pub fn _mm256_blend_epi32<const CONTROL: i32>(x: i32x8, y: i32x8) -> i32x8 {


All of these functions need some comments on what they are doing, not only the code.

franziskuskiefer · 2025-05-22T06:50:44Z

fstar-helpers/core-models/src/core_arch/x86/interpretations.rs

    pub mod lemmas {
+        //! This module provides lemmas allowing to lift the intrinsics modeled in `super` from their version operating on AVX2 vectors to functions operating on machine integer vectors (e.g. on `i32x8`).
+        #[cfg(hax)]


Shouldn't this only be used with a hax config anyway?

franziskuskiefer · 2025-05-22T06:51:30Z

fstar-helpers/core-models/src/core_arch/x86/interpretations.rs

-        #[allow(unused)]
-        use crate::core_arch::x86::__m256i;
+        #[cfg(hax)]
+        use crate::core_arch::x86::{__m128i, __m256, __m256i};

        /// An F* attribute that marks an item as being an lifting lemma.
        #[allow(dead_code)]


Why allow dead code? That should never be necessary. Either it's public and could be used by a consumer, or it's not used, that it should go away.

franziskuskiefer · 2025-05-22T06:55:21Z

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

@@ -0,0 +1,55 @@
+#[cfg(test)]


Looks like this should be a #![cfg(test)] or that guard should go a level up?

franziskuskiefer · 2025-05-22T06:56:04Z

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

+    use rand::prelude::*;
+
+    /// Helper trait to generate random values
+    pub trait HasRandom {


HasRandom is a question. So I would expect this to tell me if a type has randomness. But this generates randomness.

franziskuskiefer · 2025-05-22T06:57:23Z

libcrux-ml-dsa/src/simd/avx2/arithmetic.rs

+// TODO: prove equivalence to our specification of `montgomery_multiply`.
+#[cfg(hax)]
+#[hax_lib::fstar::before("[@@ Tactics.Circuits.auto_unapply 2 ]")]
+pub fn montgomery_multiply_spec(x: i32, y: i32) -> i32 {


Let's move the proof code into a separate module from the start.

franziskuskiefer · 2025-05-22T06:57:41Z

libcrux-ml-dsa/src/simd/avx2/arithmetic.rs

+#[cfg(hax)]
+#[hax_lib::fstar::before("[@@ Tactics.Circuits.auto_unapply 2 ]")]
+pub fn montgomery_multiply_spec(x: i32, y: i32) -> i32 {
+    pub fn i32_extended64_mul(x: i32, y: i32) -> i64 {


Why does this need to be public?

franziskuskiefer · 2025-05-22T06:58:49Z

libcrux-ml-dsa/src/simd/avx2/arithmetic.rs

+    }
+    let x_mul_y = i32_extended64_mul(x, y);
+    let lhs = (x_mul_y >> 32i32) as i32;
+    let rhs = ((((i32_extended64_mul(x_mul_y as i32, INVERSE_OF_MODULUS_MOD_MONTGOMERY_R as i32)


Can you make this more readable by pulling out the different steps?

W95Psp · 2025-05-23T06:19:35Z

Turning into draft, not sure if we will merge this one.

W95Psp added 8 commits May 19, 2025 07:26

F*: core-models: use generic makefile

f5f0758

Tactics.Circuits.fst: was moved to `fstar-helpers/core-models/proofs/…

b76af57

…fstar/extraction`

F*: Makefile: remove ref to Hacl*, see #961

365c6f6

libcrux-intrinsics: hax_lib::opaque not useful any longer

1c8da44

`core-models` now models (or declare) most avx2 intrinsics used in libcrux-intrinscs

F*: generic makefile: add a check/*.fst target

cc3209f

backport from core-models: Tactics.Circuits: unapply lemmas

713532c

ml-dsa: F*: equiv lemma for montgomery_lemma

18a96c1

W95Psp requested a review from a team as a code owner May 19, 2025 10:01

W95Psp requested a review from karthikbhargavan May 19, 2025 11:58

W95Psp self-assigned this May 19, 2025

karthikbhargavan approved these changes May 21, 2025

View reviewed changes

karthikbhargavan added the do-not-merge Don't merge this PR label May 21, 2025

franziskuskiefer requested changes May 22, 2025

View reviewed changes

W95Psp marked this pull request as draft May 23, 2025 06:19

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Add equivalence lemma for `montgomery_multuiply` #975

Add equivalence lemma for `montgomery_multuiply` #975

Uh oh!

W95Psp commented May 19, 2025

Uh oh!

W95Psp commented May 21, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

franziskuskiefer May 22, 2025

Uh oh!

W95Psp commented May 23, 2025

Uh oh!

Uh oh!

		@@ -28,18 +36,509 @@ pub mod int_vec {
		}

		pub fn _mm256_blend_epi32<const CONTROL: i32>(x: i32x8, y: i32x8) -> i32x8 {

Add equivalence lemma for montgomery_multuiply #975

Are you sure you want to change the base?

Add equivalence lemma for montgomery_multuiply #975

Uh oh!

Conversation

W95Psp commented May 19, 2025

Uh oh!

W95Psp commented May 21, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

W95Psp commented May 23, 2025

Uh oh!

Uh oh!

Add equivalence lemma for `montgomery_multuiply` #975

Add equivalence lemma for `montgomery_multuiply` #975