FEATURE/Add: Full Continuous Differential-Linear Model integration and CP evaluation#440
Draft
rony-ramos wants to merge 5 commits into
Draft
FEATURE/Add: Full Continuous Differential-Linear Model integration and CP evaluation#440rony-ramos wants to merge 5 commits into
rony-ramos wants to merge 5 commits into
Conversation
…ound test - Translated connection constraints from middle to bottom to use a canonical meaning per border bit, preventing mathematical errors from fan-out logic. - Adapted the integrated model to properly reflect standalone continuous boundary semantics. - Updated the differential linear model test to use float_search and explicitly minimize the correlation log2 approximation. - Improved solver output parsing to iterate over all solutions and accurately fetch the optimal correlation, avoiding premature factible states.
- Added get_fixed_variable_from_hex utility method to MznDifferentialLinearModel to standardize and simplify fixing component bits from hex strings. - Added optimization_objective parameter to build_xor_differential_linear_model to allow natively injecting custom solve statements (e.g., minimize correlation_log2_approximation) without manual constraint string manipulation. - Refactored mzn_differential_linear_model_test.py to use these new clean APIs, removing duplicated hex parsing helpers and hacky array replacements.
- Replace direct float equality checks with math.isclose() in continuous predicates - Extract complex loop logic into helper functions in mzn_differential_linear_model.py to reduce cognitive complexity (border constraints, output parsing) - Simplify intermediate output pinning iteration and remove unused 'pin_bit'
…nd clean up test cases
rony-ramos
force-pushed
the
feature/add-cp-continuous-model-tests
branch
from
0ede228 to
30f48b8
Compare
…linear wiring constraints Co-authored-by: Copilot <copilot@github.com>
|
juaninf
requested changes
Apr 27, 2026
Collaborator
juaninf
left a comment
juaninf
left a comment
There was a problem hiding this comment.
we should include more tests for many more ARX ciphers. LEA, ChaCha, Salsa, HIGHT...Every distinguisher must be checked experimentally using the checkers module
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Overview
This PR introduces the integration of the Continuous Differential-Linear Model into the CP solver pipeline. It enables the evaluation of differential-linear trails (e.g., Speck 9-rounds) by linking a differential top part, a continuous-correlation middle part, and a linear bottom part, based on the mathematical formulation from [BGGMP2023].
Current Implementation Approach:
_continuous_middle_to_bottom_connecting_constraints) is implemented per canonical border bit. This computes the differential-linear correlation across the boundary and maps fan-outs.optimization_objectiveinjection withinbuild_xor_differential_linear_model, allowing the solver to bypass default satisfying statements and minimize thecorrelation_log2_approximation.get_fixed_variable_from_hexutility to standardize variable fixing across test suites.test_differential_linear_trail_continuous_middle_9_rounds_speck_table4_full_model_float_search_scip) that builds the model and invokes the SCIP solver (float_search) to validate the total probability against the paper's expected values.How to test
Verify the standalone continuous models and the fully integrated split models: