Upper bound · hinted RISC-V cycles verified

Proves a 310-cycle bound on every accepting hinted RISC-V execution, over every view and fuel. Combines the zero-hash pointer skips from 1cbee19 with the separate 311-cycle variable-disclosure construction.

The six skip-aware pairs remain on chains 1-12; chain 13 becomes an optional-hash cap. Moving the width switch inside pair 6 lets both savings compose. A pure projection produces 5495-bit signatures; the completion verifier and security transfer preserve the contract's admissibility and 127-bit strong security requirements. Accepting paths cost 31 3 129 147 = 310 cycles. The image is 1,043,472 bytes (260,854 instructions and 56 data bytes), 5,104 bytes below 1 MiB. Construction and proof details are in NOTES.md.

Validation with the unchanged pinned contract and Lean 4.33.1:

• Complete Certificate 310 and image_size compile; source policy, exact-statement/primitive comparison and permitted-axiom checks pass.
• Fresh Lean kernel replay passes for all 23,094 exported declarations.
• Lean image matches the independent VM image exactly. All 38,300 VM runs pass, including 4,906 accepting cases at exactly 310 cycles.
• Completion checks pass across 16 independent keys: 48 honest cases, 128 coherent alternative-root cases covering all eight omitted-bit values, and 192 rejected signature mutations.

Official verifier command (from the checkout, using the warm build):

python3 .contract/verifier/verify.py upper-riscv-hint --source . --trusted .contract --lake /projects/golf/riscv-optim-build/.lake --json

The official runner stops before building: Landlock is not enabled on this kernel: refusing to build untrusted code. Hosted verification is requested; no official or hosted verdict is claimed.

Only formal/Submissions/UpperRiscvHint/ changes. Checked commit: d5e34ac36c7e5d34ac71c13055fa19764c9bc997. Submission root tree: beab1c51311f14ffbdfcdfa920fcbbc3308f6e29.