Skip to content

Conversation

@OlivierBBB
Copy link
Collaborator

@OlivierBBB OlivierBBB commented Oct 24, 2025

Note

Introduce explicit in-bounds signals and gate OOB/EXP/MMU and pricing logic on them, while adjusting leading-word and log computations for MODEXP.

  • hub/osaka/constraints/.../modexp/common.lisp:
    • Bounds signals:
      • Add bbs-within-bounds/bbs-out-of-bounds, ebs-within-bounds/ebs-out-of-bounds, mbs-within-bounds/mbs-out-of-bounds, and aggregate all-byte-sizes-are-in-bounds.
    • bbs/ebs/mbs analysis:
      • In mbs OOB instruction, replace constant 1 with bbs-within-bounds for max selection gate.
    • Leading-word analysis:
      • Replace flag sum constraint with explicit gates: EXP and MMU flags tied to load-lead; OOB flag tied to all-byte-sizes-are-in-bounds; ensure MXP_FLAG and STP_FLAG are zero.
      • Gate setting of OOB/EXP/MMU instructions on their respective call flags.
      • Derive load-lead, cds-cutoff, ebs-cutoff, sub-ebs-32 from call-OOB-module-for-modexp-lead; compute raw-lead-* under call-MMU-module-for-modexp-lead.
      • Compute lead-log under call-EXP-module-for-modexp-lead; update modexp-full-log factor from 8 to 16.
    • Pricing analysis:
      • Gate OOB misc flag weight by all-byte-sizes-are-in-bounds.

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

@OlivierBBB OlivierBBB self-assigned this Oct 24, 2025
cursor[bot]

This comment was marked as outdated.

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