CBMC: Pull and test weakening is_fresh in contract applications #834

hanno-becker · 2025-03-03T07:24:04Z

Resolves CBMC: Avoid splitting multi-dimensional arrays into multiple allocations #764

This PR updates CBMC to include the in-review patch diffblue/cbmc#8603 which weakens the interpretation of memory_no_alias (or __CPROVER_is_fresh) in function contract applications: Rather than asserting that every pointer featuring in a memory_no_alis/__CPROVER_is_fresh clause be in a separate object, pointers can now point to the same object, so long as the slices they represent are disjoint.

This allows us to undo some artificial splitting of 2D arrays into separate objects, which this PR also does.

oqs-bot

Intel Xeon 4th gen (c7i)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`9520` cycles	`9597` cycles	`0.99`
`ML-KEM-512 encaps`	`11066` cycles	`11236` cycles	`0.98`
`ML-KEM-512 decaps`	`15315` cycles	`15670` cycles	`0.98`
`ML-KEM-768 keypair`	`16328` cycles	`16353` cycles	`1.00`
`ML-KEM-768 encaps`	`17740` cycles	`17883` cycles	`0.99`
`ML-KEM-768 decaps`	`23381` cycles	`23614` cycles	`0.99`
`ML-KEM-1024 keypair`	`22009` cycles	`22200` cycles	`0.99`
`ML-KEM-1024 encaps`	`24052` cycles	`24055` cycles	`1.00`
`ML-KEM-1024 decaps`	`31707` cycles	`31879` cycles	`0.99`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 4th gen (c7i) (no-opt)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`30106` cycles	`29295` cycles	`1.03`
`ML-KEM-512 encaps`	`35560` cycles	`34666` cycles	`1.03`
`ML-KEM-512 decaps`	`44940` cycles	`45016` cycles	`1.00`
`ML-KEM-768 keypair`	`48520` cycles	`48626` cycles	`1.00`
`ML-KEM-768 encaps`	`55670` cycles	`55749` cycles	`1.00`
`ML-KEM-768 decaps`	`68995` cycles	`67492` cycles	`1.02`
`ML-KEM-1024 keypair`	`74883` cycles	`72614` cycles	`1.03`
`ML-KEM-1024 encaps`	`83240` cycles	`84526` cycles	`0.98`
`ML-KEM-1024 decaps`	`99734` cycles	`101720` cycles	`0.98`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

⚠️ Performance Alert ⚠️

Possible performance regression was detected for benchmark 'Intel Xeon 4th gen (c7i) (no-opt)'.
Benchmark result of this commit is worse than the previous benchmark result exceeding threshold 1.03.

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-1024 keypair`	`74883` cycles	`72614` cycles	`1.03`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`29465` cycles	`29537` cycles	`1.00`
`ML-KEM-512 encaps`	`34949` cycles	`35130` cycles	`0.99`
`ML-KEM-512 decaps`	`45615` cycles	`45748` cycles	`1.00`
`ML-KEM-768 keypair`	`50151` cycles	`50466` cycles	`0.99`
`ML-KEM-768 encaps`	`55771` cycles	`55827` cycles	`1.00`
`ML-KEM-768 decaps`	`70733` cycles	`70802` cycles	`1.00`
`ML-KEM-1024 keypair`	`73192` cycles	`73372` cycles	`1.00`
`ML-KEM-1024 encaps`	`82038` cycles	`82306` cycles	`1.00`
`ML-KEM-1024 decaps`	`102141` cycles	`102575` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 4th gen (c7a)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`11736` cycles	`11632` cycles	`1.01`
`ML-KEM-512 encaps`	`13526` cycles	`13296` cycles	`1.02`
`ML-KEM-512 decaps`	`18354` cycles	`18191` cycles	`1.01`
`ML-KEM-768 keypair`	`20234` cycles	`20164` cycles	`1.00`
`ML-KEM-768 encaps`	`21163` cycles	`21234` cycles	`1.00`
`ML-KEM-768 decaps`	`28357` cycles	`29358` cycles	`0.97`
`ML-KEM-1024 keypair`	`27127` cycles	`27028` cycles	`1.00`
`ML-KEM-1024 encaps`	`29168` cycles	`29043` cycles	`1.00`
`ML-KEM-1024 decaps`	`38603` cycles	`38607` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 3rd gen (c6a)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`17256` cycles	`17238` cycles	`1.00`
`ML-KEM-512 encaps`	`19062` cycles	`19140` cycles	`1.00`
`ML-KEM-512 decaps`	`24516` cycles	`24492` cycles	`1.00`
`ML-KEM-768 keypair`	`29646` cycles	`29382` cycles	`1.01`
`ML-KEM-768 encaps`	`30806` cycles	`30618` cycles	`1.01`
`ML-KEM-768 decaps`	`38687` cycles	`38563` cycles	`1.00`
`ML-KEM-1024 keypair`	`42932` cycles	`44018` cycles	`0.98`
`ML-KEM-1024 encaps`	`45288` cycles	`45094` cycles	`1.00`
`ML-KEM-1024 decaps`	`55899` cycles	`55657` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 3rd gen (c6i)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`16140` cycles	`16173` cycles	`1.00`
`ML-KEM-512 encaps`	`18234` cycles	`18398` cycles	`0.99`
`ML-KEM-512 decaps`	`24753` cycles	`24967` cycles	`0.99`
`ML-KEM-768 keypair`	`27810` cycles	`27829` cycles	`1.00`
`ML-KEM-768 encaps`	`29443` cycles	`29542` cycles	`1.00`
`ML-KEM-768 decaps`	`38819` cycles	`38963` cycles	`1.00`
`ML-KEM-1024 keypair`	`37592` cycles	`37742` cycles	`1.00`
`ML-KEM-1024 encaps`	`40584` cycles	`40742` cycles	`1.00`
`ML-KEM-1024 decaps`	`53161` cycles	`53348` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton4

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`17934` cycles	`17994` cycles	`1.00`
`ML-KEM-512 encaps`	`21302` cycles	`21366` cycles	`1.00`
`ML-KEM-512 decaps`	`28002` cycles	`28067` cycles	`1.00`
`ML-KEM-768 keypair`	`30885` cycles	`31012` cycles	`1.00`
`ML-KEM-768 encaps`	`33981` cycles	`34096` cycles	`1.00`
`ML-KEM-768 decaps`	`43569` cycles	`43719` cycles	`1.00`
`ML-KEM-1024 keypair`	`44617` cycles	`44782` cycles	`1.00`
`ML-KEM-1024 encaps`	`50097` cycles	`50201` cycles	`1.00`
`ML-KEM-1024 decaps`	`63123` cycles	`63158` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 4th gen (c7a) (no-opt)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`36343` cycles	`36710` cycles	`0.99`
`ML-KEM-512 encaps`	`42961` cycles	`43098` cycles	`1.00`
`ML-KEM-512 decaps`	`56020` cycles	`56147` cycles	`1.00`
`ML-KEM-768 keypair`	`59298` cycles	`59507` cycles	`1.00`
`ML-KEM-768 encaps`	`67760` cycles	`67978` cycles	`1.00`
`ML-KEM-768 decaps`	`85062` cycles	`85150` cycles	`1.00`
`ML-KEM-1024 keypair`	`87914` cycles	`88143` cycles	`1.00`
`ML-KEM-1024 encaps`	`98605` cycles	`98998` cycles	`1.00`
`ML-KEM-1024 decaps`	`120556` cycles	`120682` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

AMD EPYC 3rd gen (c6a) (no-opt)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`39024` cycles	`39039` cycles	`1.00`
`ML-KEM-512 encaps`	`47079` cycles	`47229` cycles	`1.00`
`ML-KEM-512 decaps`	`60666` cycles	`60809` cycles	`1.00`
`ML-KEM-768 keypair`	`63347` cycles	`63520` cycles	`1.00`
`ML-KEM-768 encaps`	`74090` cycles	`74213` cycles	`1.00`
`ML-KEM-768 decaps`	`91909` cycles	`92318` cycles	`1.00`
`ML-KEM-1024 keypair`	`94224` cycles	`94330` cycles	`1.00`
`ML-KEM-1024 encaps`	`107039` cycles	`107393` cycles	`1.00`
`ML-KEM-1024 decaps`	`129518` cycles	`129890` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Intel Xeon 3rd gen (c6i) (no-opt)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`47477` cycles	`47713` cycles	`1.00`
`ML-KEM-512 encaps`	`55387` cycles	`55651` cycles	`1.00`
`ML-KEM-512 decaps`	`71616` cycles	`71784` cycles	`1.00`
`ML-KEM-768 keypair`	`77387` cycles	`76887` cycles	`1.01`
`ML-KEM-768 encaps`	`87503` cycles	`87324` cycles	`1.00`
`ML-KEM-768 decaps`	`108047` cycles	`108222` cycles	`1.00`
`ML-KEM-1024 keypair`	`113239` cycles	`112850` cycles	`1.00`
`ML-KEM-1024 encaps`	`126256` cycles	`126323` cycles	`1.00`
`ML-KEM-1024 decaps`	`152801` cycles	`153030` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton4 (no-opt)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`35923` cycles	`35965` cycles	`1.00`
`ML-KEM-512 encaps`	`40865` cycles	`40873` cycles	`1.00`
`ML-KEM-512 decaps`	`52272` cycles	`52312` cycles	`1.00`
`ML-KEM-768 keypair`	`60052` cycles	`63500` cycles	`0.95`
`ML-KEM-768 encaps`	`66960` cycles	`67650` cycles	`0.99`
`ML-KEM-768 decaps`	`81400` cycles	`81528` cycles	`1.00`
`ML-KEM-1024 keypair`	`89038` cycles	`89212` cycles	`1.00`
`ML-KEM-1024 encaps`	`98845` cycles	`99055` cycles	`1.00`
`ML-KEM-1024 decaps`	`117690` cycles	`117884` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton2

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`29462` cycles	`29539` cycles	`1.00`
`ML-KEM-512 encaps`	`34952` cycles	`35131` cycles	`0.99`
`ML-KEM-512 decaps`	`45628` cycles	`45736` cycles	`1.00`
`ML-KEM-768 keypair`	`50150` cycles	`50471` cycles	`0.99`
`ML-KEM-768 encaps`	`55768` cycles	`55826` cycles	`1.00`
`ML-KEM-768 decaps`	`70721` cycles	`70815` cycles	`1.00`
`ML-KEM-1024 keypair`	`73200` cycles	`73374` cycles	`1.00`
`ML-KEM-1024 encaps`	`82067` cycles	`82311` cycles	`1.00`
`ML-KEM-1024 decaps`	`102179` cycles	`102590` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton3

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`18958` cycles	`18975` cycles	`1.00`
`ML-KEM-512 encaps`	`22640` cycles	`22762` cycles	`0.99`
`ML-KEM-512 decaps`	`29960` cycles	`30063` cycles	`1.00`
`ML-KEM-768 keypair`	`32423` cycles	`32543` cycles	`1.00`
`ML-KEM-768 encaps`	`36153` cycles	`36266` cycles	`1.00`
`ML-KEM-768 decaps`	`46542` cycles	`46688` cycles	`1.00`
`ML-KEM-1024 keypair`	`46753` cycles	`46845` cycles	`1.00`
`ML-KEM-1024 encaps`	`52766` cycles	`52862` cycles	`1.00`
`ML-KEM-1024 decaps`	`66687` cycles	`66821` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton3 (no-opt)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`38968` cycles	`39095` cycles	`1.00`
`ML-KEM-512 encaps`	`44953` cycles	`44985` cycles	`1.00`
`ML-KEM-512 decaps`	`56753` cycles	`56885` cycles	`1.00`
`ML-KEM-768 keypair`	`64228` cycles	`64570` cycles	`0.99`
`ML-KEM-768 encaps`	`72047` cycles	`72797` cycles	`0.99`
`ML-KEM-768 decaps`	`88087` cycles	`88132` cycles	`1.00`
`ML-KEM-1024 keypair`	`96219` cycles	`96237` cycles	`1.00`
`ML-KEM-1024 encaps`	`106315` cycles	`106344` cycles	`1.00`
`ML-KEM-1024 decaps`	`127125` cycles	`127370` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Graviton2 (no-opt)

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`59359` cycles	`59540` cycles	`1.00`
`ML-KEM-512 encaps`	`68050` cycles	`68084` cycles	`1.00`
`ML-KEM-512 decaps`	`86715` cycles	`86728` cycles	`1.00`
`ML-KEM-768 keypair`	`98780` cycles	`99163` cycles	`1.00`
`ML-KEM-768 encaps`	`110970` cycles	`110609` cycles	`1.00`
`ML-KEM-768 decaps`	`134577` cycles	`134806` cycles	`1.00`
`ML-KEM-1024 keypair`	`148620` cycles	`149114` cycles	`1.00`
`ML-KEM-1024 encaps`	`163630` cycles	`164424` cycles	`1.00`
`ML-KEM-1024 decaps`	`195286` cycles	`195664` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Arm Cortex-A55 (Snapdragon 888) benchmarks

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`59489` cycles	`59531` cycles	`1.00`
`ML-KEM-512 encaps`	`67083` cycles	`67230` cycles	`1.00`
`ML-KEM-512 decaps`	`86178` cycles	`86700` cycles	`0.99`
`ML-KEM-768 keypair`	`101238` cycles	`101287` cycles	`1.00`
`ML-KEM-768 encaps`	`112266` cycles	`112496` cycles	`1.00`
`ML-KEM-768 decaps`	`140251` cycles	`139906` cycles	`1.00`
`ML-KEM-1024 keypair`	`153648` cycles	`153294` cycles	`1.00`
`ML-KEM-1024 encaps`	`171761` cycles	`170882` cycles	`1.01`
`ML-KEM-1024 decaps`	`210440` cycles	`207942` cycles	`1.01`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

SpacemiT K1 8 (Banana Pi F3) benchmarks

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`225745` cycles	`225449` cycles	`1.00`
`ML-KEM-512 encaps`	`272050` cycles	`271291` cycles	`1.00`
`ML-KEM-512 decaps`	`346626` cycles	`345866` cycles	`1.00`
`ML-KEM-768 keypair`	`374521` cycles	`373256` cycles	`1.00`
`ML-KEM-768 encaps`	`434247` cycles	`433951` cycles	`1.00`
`ML-KEM-768 decaps`	`533232` cycles	`531800` cycles	`1.00`
`ML-KEM-1024 keypair`	`555034` cycles	`555190` cycles	`1.00`
`ML-KEM-1024 encaps`	`633407` cycles	`634492` cycles	`1.00`
`ML-KEM-1024 decaps`	`756302` cycles	`757111` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

oqs-bot

Arm Cortex-A72 (Raspberry Pi 4) benchmarks

Benchmark suite	Current: `5ad011f`	Previous: `0642fe7`	Ratio
`ML-KEM-512 keypair`	`53073` cycles	`53953` cycles	`0.98`
`ML-KEM-512 encaps`	`62494` cycles	`61889` cycles	`1.01`
`ML-KEM-512 decaps`	`77963` cycles	`78765` cycles	`0.99`
`ML-KEM-768 keypair`	`92167` cycles	`90454` cycles	`1.02`
`ML-KEM-768 encaps`	`100317` cycles	`98496` cycles	`1.02`
`ML-KEM-768 decaps`	`122968` cycles	`123646` cycles	`0.99`
`ML-KEM-1024 keypair`	`134741` cycles	`136037` cycles	`0.99`
`ML-KEM-1024 encaps`	`148602` cycles	`148431` cycles	`1.00`
`ML-KEM-1024 decaps`	`181683` cycles	`181692` cycles	`1.00`

This comment was automatically generated by workflow using github-action-benchmark.

Signed-off-by: Hanno Becker <[email protected]>

Previously, we had to split various 2D arrays into separate objects to accommodate the strict semantics of is_fresh/memory_no_alias in function contract preconditions. With the new relaxed semantics of is_fresh/memory_no_alias, this is no longer necessary. Signed-off-by: Hanno Becker <[email protected]>

The previous semantics of `is_fresh()` as requiring pointers to separate objects forced us to write separate contracts for mlk_poly_getnoise_eta1_4x depending on MLKEM_K. With the relaxed semantics of is_fresh/memory_no_alias, this is no longer necessary, and a simple and unified contract suffices. Signed-off-by: Hanno Becker <[email protected]>

mkannwischer force-pushed the cbmc_test branch from dbb0b7f to e6eae8a Compare March 3, 2025 07:30

hanno-becker force-pushed the cbmc_test branch 6 times, most recently from 563a49a to 5ad011f Compare March 4, 2025 09:31

hanno-becker changed the title ~~[TEST] CBMC: Test PR weakening is_fresh in contract applications~~ CBMC: Test PR weakening is_fresh in contract applications Mar 4, 2025

hanno-becker changed the title ~~CBMC: Test PR weakening is_fresh in contract applications~~ CBMC: Pull and test weakening is_fresh in contract applications Mar 4, 2025

hanno-becker added the benchmark this PR should be benchmarked in CI label Mar 4, 2025

hanno-becker mentioned this pull request Mar 4, 2025

CONTRACTS: is_fresh now tracks separation at the byte level instead of whole objects diffblue/cbmc#8603

Merged

oqs-bot reviewed Mar 4, 2025

View reviewed changes

hanno-becker force-pushed the cbmc_test branch from 5ad011f to fd31f50 Compare March 5, 2025 20:25

hanno-becker added 3 commits March 8, 2025 13:55

[TEST] CBMC: Test PR weakening is_fresh in contract applications

105a185

Signed-off-by: Hanno Becker <[email protected]>

hanno-becker force-pushed the cbmc_test branch from fd31f50 to 07528c6 Compare March 8, 2025 13:55

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

CBMC: Pull and test weakening is_fresh in contract applications #834

CBMC: Pull and test weakening is_fresh in contract applications #834

hanno-becker commented Mar 3, 2025 •

edited

Loading

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

oqs-bot left a comment

CBMC: Pull and test weakening is_fresh in contract applications #834

Are you sure you want to change the base?

CBMC: Pull and test weakening is_fresh in contract applications #834

Conversation

hanno-becker commented Mar 3, 2025 • edited Loading

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 4th gen (c7i)

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 4th gen (c7i) (no-opt)

oqs-bot left a comment

Choose a reason for hiding this comment

⚠️ Performance Alert ⚠️

oqs-bot left a comment

Choose a reason for hiding this comment

Arm Cortex-A76 (Raspberry Pi 5) benchmarks

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 4th gen (c7a)

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 3rd gen (c6a)

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 3rd gen (c6i)

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton4

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 4th gen (c7a) (no-opt)

oqs-bot left a comment

Choose a reason for hiding this comment

AMD EPYC 3rd gen (c6a) (no-opt)

oqs-bot left a comment

Choose a reason for hiding this comment

Intel Xeon 3rd gen (c6i) (no-opt)

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton4 (no-opt)

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton2

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton3

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton3 (no-opt)

oqs-bot left a comment

Choose a reason for hiding this comment

Graviton2 (no-opt)

oqs-bot left a comment

Choose a reason for hiding this comment

Arm Cortex-A55 (Snapdragon 888) benchmarks

oqs-bot left a comment

Choose a reason for hiding this comment

SpacemiT K1 8 (Banana Pi F3) benchmarks

oqs-bot left a comment

Choose a reason for hiding this comment

Arm Cortex-A72 (Raspberry Pi 4) benchmarks

hanno-becker commented Mar 3, 2025 •

edited

Loading