Skip to content

pad the ppt program columns to allow lengths that arent powers of 2#1711

Draft
ohad-nir-starkware wants to merge 1 commit intoohadn/remove_program_segment_from_prooffrom
ohadn/padded-verify_program
Draft

pad the ppt program columns to allow lengths that arent powers of 2#1711
ohad-nir-starkware wants to merge 1 commit intoohadn/remove_program_segment_from_prooffrom
ohadn/padded-verify_program

Conversation

@ohad-nir-starkware
Copy link
Copy Markdown
Collaborator

@ohad-nir-starkware ohad-nir-starkware commented Mar 24, 2026

Note

Medium Risk
Changes the verify_program builtin AIR and witness generation to add a conditional/padded program column and to gate memory lookups, which can affect proof soundness/compatibility if any of the new padding/cond wiring is wrong. Scope is contained to program preprocessing and verify_program paths but touches core proving/verification constraints.

Overview
Supports non-power-of-two program lengths in the preprocessed trace by padding the program table to a fixed 1 << PROGRAM_LOG_LEN_BOUND and adding an extra program column (curr_program_28) that acts as an is-active/cond flag.

Updates the verify_program builtin to use a new MemVerifyCond subroutine so memory address/id and id/value relations are enforced only when cond=1, and adjusts witness generation to (a) compute cond in fast deduction, (b) avoid out-of-bounds memory reads on padding rows via a safe address, and (c) only feed memory subcomponent inputs for active lanes. Also updates adapter segment bounds, registry metadata, and the slow test to use the non-padded opcode program.

Written by Cursor Bugbot for commit 60c49df. This will update automatically on new commits. Configure here.


This change is Reviewable

@ohad-nir-starkware ohad-nir-starkware self-assigned this Mar 24, 2026
@ohad-nir-starkware ohad-nir-starkware force-pushed the ohadn/padded-verify_program branch 3 times, most recently from e4f8847 to 4ba74b1 Compare March 24, 2026 16:20

builtin_segments.verify_program = Some(MemorySegmentAddresses {
begin_addr: initial_pc as usize,
stop_ptr: initial_pc as usize + program_length,
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Missing assertion that program fits within bound

High Severity

The verify_program segment size is hardcoded to 1 << PROGRAM_LOG_LEN_BOUND (4096), but there is no assertion that the actual program length (initial_ap - 2 - initial_pc) fits within this bound. If a program exceeds 4096 entries, the segment silently covers only 4096 addresses, entries beyond that are never memory-verified, and ProgramColumn::new truncates the preprocessed data. This is a potential soundness issue where program instructions go unverified.

Additional Locations (1)
Fix in Cursor Fix in Web

@ohad-nir-starkware ohad-nir-starkware force-pushed the ohadn/padded-verify_program branch from 4ba74b1 to 60c49df Compare March 24, 2026 16:40
Copy link
Copy Markdown

@cursor cursor bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Cursor Bugbot has reviewed your changes and found 1 potential issue.

There are 2 total unresolved issues (including 1 from previous review).

Fix All in Cursor

Bugbot Autofix is OFF. To automatically fix reported issues with cloud agents, have a team admin enable autofix in the Cursor dashboard.

[M31(0); FELT252_N_WORDS];
1 << DEFAULT_PROGRAM_LOG_LEN
])
});
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Missing assertion that program fits within bound

Medium Severity

set_program_table accepts programs of any length, but ProgramColumn::new truncates to 1 << PROGRAM_LOG_LEN_BOUND (4096) entries. Previously, padded_len was data.len().next_power_of_two(), which accommodated any program size. Now, if program.len() > 4096, the preprocessed columns silently omit entries beyond the bound, and the cond column incorrectly marks all 4096 rows as active (since i < data.len() is always true). This produces an incorrect proof without any error.

Additional Locations (1)
Fix in Cursor Fix in Web

@ohad-nir-starkware ohad-nir-starkware marked this pull request as draft March 24, 2026 18:27
@ohad-nir-starkware ohad-nir-starkware force-pushed the ohadn/padded-verify_program branch 2 times, most recently from 7f199fe to 7fa3564 Compare March 25, 2026 14:22
@ohad-nir-starkware ohad-nir-starkware force-pushed the ohadn/padded-verify_program branch from 7fa3564 to d7a3580 Compare March 25, 2026 18:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant