Skip to content

fix!: claude-generated pre-audit for bitwise in avm - soundness bug and edge-case tests#19247

Closed
dbanks12 wants to merge 2 commits into
merge-train/avmfrom
db/claude-audit-bitwise
Closed

fix!: claude-generated pre-audit for bitwise in avm - soundness bug and edge-case tests#19247
dbanks12 wants to merge 2 commits into
merge-train/avmfrom
db/claude-audit-bitwise

Conversation

@dbanks12

@dbanks12 dbanks12 commented Dec 24, 2025

Copy link
Copy Markdown
Contributor

found a soundness bug in bitwise PIL

dbanks12 commented Dec 24, 2025

Copy link
Copy Markdown
Contributor Author

This stack of pull requests is managed by Graphite. Learn more about stacking.

Add audit-generated tests for the bitwise component:
- NegativeStartSha256NonBoolean: Tests that start_sha256 must be boolean
- NegativeStartKeccakNonBoolean: Tests that start_keccak must be boolean
- XorIdenticalValuesYieldsZero: Edge case for x XOR x = 0
- OrWithMaxValue: Edge case for OR with 0xFFFFFFFF
- AndWithZero: Edge case for AND with 0

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
@dbanks12 dbanks12 changed the base branch from db/ecc-claude-audit to graphite-base/19247 December 24, 2025 17:14
@dbanks12 dbanks12 force-pushed the graphite-base/19247 branch from 71533aa to 67fcd87 Compare December 24, 2025 17:14
@dbanks12 dbanks12 force-pushed the db/claude-audit-bitwise branch from 80f2cd5 to 19c47e3 Compare December 24, 2025 17:14
@dbanks12 dbanks12 changed the base branch from graphite-base/19247 to merge-train/avm December 24, 2025 17:14
@dbanks12 dbanks12 force-pushed the db/claude-audit-bitwise branch from 19c47e3 to 0e2c862 Compare December 24, 2025 17:57
The start_sha256 column was declared but lacked a boolean constraint,
which is required since it's used as a destination selector for lookups
from SHA256 into the bitwise trace.

Added: start_sha256 * (1 - start_sha256) = 0;

This was found during a comprehensive audit of the bitwise component.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
@dbanks12 dbanks12 force-pushed the db/claude-audit-bitwise branch from 0e2c862 to 2ca82e2 Compare December 24, 2025 17:58
@dbanks12 dbanks12 marked this pull request as ready for review December 24, 2025 17:58
@dbanks12 dbanks12 changed the title test: claude-generated edge case tests for bitwise audit test: claude-generated pre-audit for bitwise in avm - soundness bug and edge-case tests Dec 24, 2025
@dbanks12 dbanks12 changed the title test: claude-generated pre-audit for bitwise in avm - soundness bug and edge-case tests fix!: claude-generated pre-audit for bitwise in avm - soundness bug and edge-case tests Dec 24, 2025
EXPECT_THROW_WITH_MESSAGE(check_relation<bitwise>(trace, 2UL), "");
}

// Edge case: XOR of identical values should yield 0

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

I do not think that the 3 following tests are really edge cases (we precompute) but we can keep them as "sanity test vectors".


// Tests that start_sha256 must be boolean (0 or 1).
// This test verifies that the constraint `start_sha256 * (1 - start_sha256) = 0` is enforced.
TEST(BitwiseConstrainingTest, NegativeStartSha256NonBoolean)

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

If we want to keep these two boolean checks then we should use an alias for the sub-relation instead of calling check_relation<bitwise>(trace, 3UL) with an integer literal.

@jeanmon jeanmon left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

Good catch! I added some comments on the unit tests.

@dbanks12

dbanks12 commented Jan 6, 2026

Copy link
Copy Markdown
Contributor Author

Replaced by #19256

@dbanks12 dbanks12 closed this Jan 6, 2026
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.

2 participants