Porting feature #1108 and #905 from mlkem-native to mldsa-native #413
Conversation
There was a problem hiding this comment.
I see that the format script has diverged from mlkem-native.
Can we consolidate that by either fixing it in this PR, or opening an issue.
I see there is already #158 for the magic constant, but there are 3 more difference:
- check-constracts
- shell linting
- copyright checking
There was a problem hiding this comment.
Hello, Matthias,
Thank you for your reviewing, open issue:
There was a problem hiding this comment.
I do see a diff in run_cbmc_single_step compared to mlkem-native that looks unintentional to me. Can you consolidate that please?
There was a problem hiding this comment.
While at it - can you fix this line:
log.error(
"Could not find function {self.args.start_with}. Running all proofs"
)
log is not defined.
There was a problem hiding this comment.
Hello, Matthis, thank you for your reviewing!
Both issues you mentioned been fixed as follow:
-
For the first part, I aligned the error handling in mldsa with the approach used in mlkem, which involves three main updates:
- aligned the way
capture_outputis handled. - aligned the handling of
subprocess.TimeoutExpired. - Added an additional checking before decoding
p.stderr.
- aligned the way
-
For the second part, I created a corresponding log instance for the
run_cbmc,to solve the not defined error, -
And I throught that the same issue exists in the mlkem and need to be fixed. If my fix at here is acceptable, I will create a separate issue and apply the same fix in the mlkem-native repository.
willieyz
force-pushed
the
test-color-cbmc
branch
2 times, most recently
from
d2a700f to
daf8962
Compare
- This commit is ported from: - mlkem-native, commit: 1f40536 - `autogen` prints high-level status updates in addition to the low-level per-file status updates - `autogen` uses color coding like `format` does - `lint` omits GH summary content if GITHUB_STEP_SUMMARY is not set. - format uses color-coded error messages - The color definitions across the scripts have been harmonized Note: We did not port the functional changes from commit 1f40536 due to the divergence between the two project repositories. However, if `synchronize_backends`, `gen_citations_for` or other functions are introduced in the future, we will consider incorporating those changes into mldsa-native. Signed-off-by: willieyz <[email protected]>
- This commit is ported from: - mlkem, commit: 615d972 - This commit adds support for the use of wildcard pattern `*` in invocations of `tests cbmc`. Example: ``` tests cbmc -p "*poly*" ``` This will run all tests for functions containing "poly". - As before, multiple patterns can be provided, e.g. ``` tests cbmc -p "*keccak*" "*once*" ``` Signed-off-by: willieyz <[email protected]>
willieyz
force-pushed
the
test-color-cbmc
branch
from
daf8962 to
04ff52a
Compare
This PR port the following two PR from mlkem-native to here (mldsa-native):