Pre release v1.2.6#515
Merged
Merged
Conversation
…iren into shankara/syscall-bugs
…ating the extractor to support phase extraction in a more principled way than before
* fix trace generator bug for division that handles dividing by INT_MIN * refactoring mipstests to support both executor and prover tests * handling syscall * adding global exploit poc * adding syscall bugs * adding syscall bugs * removing large file * adding another bug * 9th bug * 10th bug * 12th bug * adding picus annotations * 13th bug * adding brk issue * 15th bug, bad fix attempt * adding 16th issue that relates to issue 6 * updated issues * 19th * removing 19 * updating extractor to support summaries for ops including iszero. Updating the extractor to support phase extraction in a more principled way than before * adding readable names to picus vars * removing syscall bugs from this branch. It isn't needed to be in the main repository * deleting global lookup poc * removing global poc test from global chip * fixing extraction for single row only chips * adding back top level mod
* fix trace generator bug for division that handles dividing by INT_MIN * refactoring mipstests to support both executor and prover tests * handling syscall * adding global exploit poc * adding syscall bugs * adding syscall bugs * removing large file * adding another bug * 9th bug * 10th bug * 12th bug * adding picus annotations * 13th bug * adding brk issue * 15th bug, bad fix attempt * adding 16th issue that relates to issue 6 * updated issues * 19th * removing 19 * updating extractor to support summaries for ops including iszero. Updating the extractor to support phase extraction in a more principled way than before * adding readable names to picus vars * removing syscall bugs from this branch. It isn't needed to be in the main repository * deleting global lookup poc * removing global poc test from global chip * fixing extraction for single row only chips * adding back top level mod * fixing assume_determinism cleanup in top module * update interaction handling for send_instruction and send_program
* fix trace generator bug for division that handles dividing by INT_MIN * refactoring mipstests to support both executor and prover tests * handling syscall * adding global exploit poc * adding syscall bugs * adding syscall bugs * removing large file * adding another bug * 9th bug * 10th bug * 12th bug * adding picus annotations * 13th bug * adding brk issue * 15th bug, bad fix attempt * adding 16th issue that relates to issue 6 * updated issues * 19th * removing 19 * updating extractor to support summaries for ops including iszero. Updating the extractor to support phase extraction in a more principled way than before * adding readable names to picus vars * removing syscall bugs from this branch. It isn't needed to be in the main repository * deleting global lookup poc * removing global poc test from global chip * fixing extraction for single row only chips * adding back top level mod * fixing assume_determinism cleanup in top module * update interaction handling for send_instruction and send_program * adding syscall result receive and adding constraints to byte_interaction_mod * enable optimization pass * adding optimization
Shankara/picus frontend updates
fixing poseidon2 blowup and overconstrainedness issue for Sha
handling keccak and poseidon hash with the picus extractor
* adding support for sha compress * fixing CI build failure * fixing build failure
* adding support for sha compress * fixing CI build failure * fixing build failure * exposing internal keccak state and adding transition annotations
* feat: check syscall chips by picus * fix: invalid postcondition * feat: check GlobalChip by picus * fix: invalid postcondition for top * fix(BooleanCircuitGarbleChip): constraint on gate_type * fix:(BooleanCircuitGarbleChip): transition is non-deterministic * fix(BooleanCircuitGarbleChip): split checks into fields and add transfer constraints on check [3] * fix(BooleanCircuitGarbleChip): transition contraints * fix(BooleanCircuitGarbleChip): transition contraints * fix(BooleanCircuitGarbleChip): contraints on checks_acc * fix(BooleanCircuitGarbleChip): transition contraints on checks_acc * fix(BooleanCircuitGarbleChip): constraints on not_last_gate * fix(BooleanCircuitGarbleChip): clear transition_output_ranges * feat(BooleanCircuitGarbleChip): expose gate-control state as explicit inputs * fix(boolean-circuit-garble): make transition constraints event-local and deterministic * fix(boolean-circuit-garble): constrain last-gate output prev_value to zero * chore(boolean-circuit-garble): reduce boolean_circuit_garble columns * fix(boolean-circuit-garble): expose transition-driving state to Picus * fix(boolean-circuit-garble): tighten single-row constraints * fix(memory): constrain first-row helper witnesses in global init * fix(memory): canonicalize padded rows in memory global finalize/init air * fix(memory): scope next-lt constraints and stabilize bit-lt eval builder * fix(memory): avoid first-row helper zeroing in boundary extraction * fix(memory): zero first-row helpers on non-first rows * fix(memory): use structural first-row selector for helper constraints * fix(memory): keep first-row helper semantics row-gated * fix(memory): expose memory transition inputs for global init * fix(memory): tighten prev_addr zero constraints for single-row extraction * fix(boolean-circuit-garble): remove unconstrained transition outputs * fix(memory): expose shard/timestamp as transition inputs for Picus * fix(sys-linux): add local_only * fix(memory): pin single-row finalize to x0 branch * fix(memory): pin single-row finalize shard/timestamp * fix(divrem): range-check b/c byte limbs in AIR * fix(picus): LTU byte-lookup operand indices * chore(global): expose kind as picus output * fix(global): constrain global receive/send selectors * fix(cpu): strengthen control-flag and sequential-pc constraints * chore(global): remove picus selector annotations from direction flags * fix(cpu): constrain padding control/pc fields for determinism * style: refactor memory global code and cargo fmt * fix(cpu): constrain transition next_pc for non-halt rows * fix: cargo build err * Revert "fix(cpu): constrain transition next_pc for non-halt rows" This reverts commit b62641c. * fix(divrem): align trace U8 checks with b/c limb constraints * fix(syscall-instrs): constrain SYSHINTLEN result through SyscallResult bridge * chore(keccak-sponge): add picus annotations * Revert "fix(syscall-instrs): constrain SYSHINTLEN result through SyscallResult bridge" This reverts commit 2591a76. * chore: add picus annotations * feat(cbindgen): add header file post-processing to fix U64_LIMBS definition * fix(poseidon2): enforce low-limb u8 checks and emit matching byte lookups * fix(picus): stop exporting unconstrained ShaCompress successor state * chore(syscall-core): annotate picus IO cols * fix(keccak-sponge): constrain read_block to first keccak round * fix(keccak-sponge): constrain input_address across non-final rounds * fix(keccak-sponge): zero unconstrained bytes when read_block is disabled * fix(keccak-sponge): use input_len_u32s for trace input_len * chore(picus): treat SyscallInstrs op_a as input in receive_instruction * fix(keccak-sponge): range-check original_state bytes in AIR and trace * fix(keccak-sponge): keep original_state stable across non-absorbed transitions * fix(keccak-sponge): range-check memory bytes used in packed limb constraints * fix(keccak-sponge): enforce first/final step flag exclusivity in outer AIR * fix(keccak-sponge): bind input_len to input_length memory word * fix(keccak-sponge): constrain input_length_mem bytes on real rows * chore(keccak_sponge): limit Picus transition outputs to stable inputs * Revert "chore(picus): treat SyscallInstrs op_a as input in receive_instruction" This reverts commit f121fdf. * style: cargo fmt & cargo clippy * fix: mips_costs.json * feat: gate picus annotations behind optional feature * style: gate chip picus_info behind picus feature
* Revert "fix(keccak_sponge): hold input_address stable across rounds (#510)" This reverts commit d2235ac. * feat(go-runtime): support non-byte slices * chore: gate PicusInfo behind the feature picus * chore: restore origin code * Revert "feat(go-runtime): support non-byte slices" This reverts commit f256821.
felicityin
approved these changes
Jun 5, 2026
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
3 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.
No description provided.