Skip to content

CBMC: State + prove spec for poly_sub #308

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
hanno-becker opened this issue Nov 2, 2024 · 1 comment · Fixed by #345
Closed

CBMC: State + prove spec for poly_sub #308

hanno-becker opened this issue Nov 2, 2024 · 1 comment · Fixed by #345
Assignees
@mkannwischer
Labels
CBMC enhancement New feature or request
Milestone
alpha-release

Comments

@hanno-becker
Copy link
Contributor

hanno-becker commented Nov 2, 2024 •
edited
Loading

Not quite the same as poly_add because of different aliasing: poly_sub is used as poly_sub(x,y,x). Otherwise, it should be the same as for poly_add, which is done in #306
@hanno-becker hanno-becker added enhancement New feature or request CBMC labels Nov 2, 2024
@hanno-becker hanno-becker added this to the cbmc-alpha milestone Nov 3, 2024
@hanno-becker
Copy link
Contributor Author

From the experience with poly_add(), we should first modify poly_sub() to a non-aliased version.

@mkannwischer mkannwischer self-assigned this Nov 5, 2024
mkannwischer added a commit that referenced this issue Nov 5, 2024
@mkannwischer
Add spec + proof for poly_sub
846ad4b 
Resolves #308

Signed-off-by: Matthias J. Kannwischer <[email protected]>
@mkannwischer mkannwischer mentioned this issue Nov 5, 2024
Merged
mkannwischer added a commit that referenced this issue Nov 5, 2024
@mkannwischer
Add spec + proof for poly_sub and change poly_sub to to argument form
d9644cd 
This first changes poly_sub from the 3 argument form poly_sub(r, a, b)
to a two argument form poly_sub(r, b) assuming that r=a.
This makes the proof possible as we do not have to reason about aliasing.
Unfortunately, currently we have poly_sub(x, a, x) rather than
poly_sub(x, x, a) in the single call site in indcpa_dec.
However, it is easy to change it there.

Resolves #308

Signed-off-by: Matthias J. Kannwischer <[email protected]>
mkannwischer added a commit that referenced this issue Nov 5, 2024
@mkannwischer
Add spec + proof for poly_sub and change poly_sub to to argument form
94e3a41 
This first changes poly_sub from the 3 argument form poly_sub(r, a, b)
to a two argument form poly_sub(r, b) assuming that r=a.
This makes the proof possible as we do not have to reason about aliasing.
Unfortunately, currently we have poly_sub(x, a, x) rather than
poly_sub(x, x, a) in the single call site in indcpa_dec.
However, it is easy to change it there.

Resolves #308

Signed-off-by: Matthias J. Kannwischer <[email protected]>
potsrevennil pushed a commit that referenced this issue Nov 6, 2024
@mkannwischer @potsrevennil
Add spec + proof for poly_sub and change poly_sub to to argument form
43f9ce3 
This first changes poly_sub from the 3 argument form poly_sub(r, a, b)
to a two argument form poly_sub(r, b) assuming that r=a.
This makes the proof possible as we do not have to reason about aliasing.
Unfortunately, currently we have poly_sub(x, a, x) rather than
poly_sub(x, x, a) in the single call site in indcpa_dec.
However, it is easy to change it there.

Resolves #308

Signed-off-by: Matthias J. Kannwischer <[email protected]>
@mkannwischer mkannwischer modified the milestones: cbmc-alpha, alpha-release Nov 13, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@mkannwischer mkannwischer

Labels
CBMC enhancement New feature or request
Projects
None yet
Milestone
alpha-release
Development

Successfully merging a pull request may close this issue.

CBMC: Add spec + proof for poly_sub pq-code-package/mlkem-native
2 participants
@mkannwischer @hanno-becker