Remove whole-struct assignment in `polyvec` functions #102

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

Open

mkannwischer opened this issue Apr 9, 2025 · 0 comments

Contributor

mkannwischer commented Apr 9, 2025 •

edited

Loading

For the CBMC proof of polyveck_decompose added in #92, some workarounds were needed due to limitations in CBMC:

This issue is to track diffblue/cbmc#8617.
Further functions were identified in #151.

Once that is resolved and CBMC is updated, we should be able to remove the workarounds in all affected functions

polyveck_decompose
polyvecl_add
polyveck_add
polyveck_sub
polyveck_use_hint
polyveck_reduce
polyvecl_reduce
polyvecl_ntt
polyveck_ntt
polyveck_addq
polyveck_power2round
polyvecl_invntt_tomont
polyveck_invntt_tomont

The text was updated successfully, but these errors were encountered:

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyvecl_add

f0c4087

Resolves #117

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer changed the title ~~Remove whole-struct assignment in polyveck_decompose~~ Remove whole-struct assignment in polyveck_decompose, and polyvecl_add

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyvecl_add

1fe877b

Resolves #117

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer mentioned this issue

CBMC: Add contracts and proofs for various polyvec functions #151

Merged

mkannwischer changed the title ~~Remove whole-struct assignment in polyveck_decompose, and polyvecl_add~~ Remove whole-struct assignment in polyveck_decompose, polyvecl_add, and polyveck_add

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_sub

fb2a396

Resolves #127

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

This also moves the correctness post-condition in poly_sub into a assert at
the end of the function. This vastly improves performance.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer changed the title ~~Remove whole-struct assignment in polyveck_decompose, polyvecl_add, and polyveck_add~~ Remove whole-struct assignment in polyvec functions

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_sub

b9efccf

Resolves #127

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

This also moves the correctness post-condition in poly_sub into a assert at
the end of the function. This vastly improves performance.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_use_hint

29b7232

Resolves #135

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyvecl_add

a630caf

Resolves #117

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_sub

0ea1b7d

Resolves #127

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

This also moves the correctness post-condition in poly_sub into a assert at
the end of the function. This vastly improves performance.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_use_hint

5c4cfad

Resolves #135

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyvecl_add

d0d1b62

Resolves #117

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_sub

ab65b05

Resolves #127

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

This also moves the correctness post-condition in poly_sub into a assert at
the end of the function. This vastly improves performance.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_use_hint

d60ef12

Resolves #135

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_sub

d3f61c4

Resolves #127

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

This also moves the correctness post-condition in poly_sub into a assert at
the end of the function. This vastly improves performance.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_use_hint

0049ad3

Resolves #135

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyvecl_add

64e372d

Resolves #117

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_sub

961efbd

Resolves #127

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

This also moves the correctness post-condition in poly_sub into a assert at
the end of the function. This vastly improves performance.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_use_hint

cdec6c2

Resolves #135

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyvecl_add

638751a

Resolves #117

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_sub

dcf9a39

Resolves #127

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

This also moves the correctness post-condition in poly_sub into a assert at
the end of the function. This vastly improves performance.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_use_hint

6050f70

Resolves #135

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyvecl_add

597a0df

Resolves #117

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_sub

75f7b1f

Resolves #127

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

This also moves the correctness post-condition in poly_sub into a assert at
the end of the function. This vastly improves performance.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer added a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_use_hint

5a25f42

Resolves #135

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

hanno-becker pushed a commit that referenced this issue


          CBMC: Add contract and proof for polyvecl_add

c345114

Resolves #117

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

hanno-becker pushed a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_sub

ece623f

Resolves #127

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

This also moves the correctness post-condition in poly_sub into a assert at
the end of the function. This vastly improves performance.

Signed-off-by: Matthias J. Kannwischer <[email protected]>

hanno-becker pushed a commit that referenced this issue


          CBMC: Add contract and proof for polyveck_use_hint

61a2040

Resolves #135

Unrolling resulted in too poor performance. The direct proof works, but it
requires to workaround the CBMC limitation described in:
#102
diffblue/cbmc#8617

Signed-off-by: Matthias J. Kannwischer <[email protected]>

mkannwischer mentioned this issue

CBMC: Add contracts and proofs for more polyvec functions #169

Merged

This was referenced Apr 30, 2025

CBMC: Add contract and proof for polyvecl_invntt_tomont #186

Merged

CBMC: Add proof and contract for polyveck_invntt_tomont #188

Merged

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment