HOL Light proofs infrastructure for x86 and basemul proof #1323
Conversation
dkostic
force-pushed
the
hol-x86-poly-basemul
branch
5 times, most recently
from
8155685 to
52cc0bd
Compare
Signed-off-by: Dusan Kostic <[email protected]>
dkostic
force-pushed
the
hol-x86-poly-basemul
branch
from
52cc0bd to
d32e305
Compare
hanno-becker
left a comment
hanno-becker
left a comment
There was a problem hiding this comment.
Looking really good @dkostic, thank you.
Could you clean up x86/proofs/mlkem_specs.ml? This has at least mentions of Arm and mldsa in it.
the reason it has mentions of Arm and ML-DSA is because I copied the whole script from s2n-bignum (https://github.com/awslabs/s2n-bignum/blob/main/common/mlkem_mldsa.ml). There, we tried to minimize duplication and consolidate all definitions and theorems that are common to ML-KEM and ML-DSA for x86 and Arm into a single file. I think we should follow the same approach here. We should aim to have a single mlkem_specs.ml file that can be shared between Arm and x86. I'd be fine with removing the ML-DSA parts but I think ideally we'd keep the file identical to the one in s2n-bignum. |
Signed-off-by: Dusan Kostic <[email protected]>
No description provided.