Upper bound · hinted RISC-V cycles verified

Ports Nicolas Consigny’s 349-cycle deterministic record (#40) to the hinted RISC-V track with identity views. The scheme, bytecode and score are unchanged. Original checked source: 162d80e00c6f9263389c9d87bbdbfc799d60a582.

Compression is id; honest expansion returns the signature unchanged. The adapter proves that the larger hinted loader cannot introduce an accepting oversized input: every view longer than 5,504 bits takes the existing rejecting length-check branch. The general identity transfer theorem comes from scaraven’s hinted-track work in leanEthereum/ots.golf-dev#2. The transfer proof establishes soundness, faithfulness and the 349-cycle accepting-execution bound for every view and fuel budget.

Image: 15,701 instructions and 88 embedded-data bytes (62,892 bytes total).

Only formal/Submissions/UpperRiscvHint/ changes. NOTES.md explains the adapter and retains the original construction notes and attribution.

Validation: The official verifier returned verified, claim 349, in 411 seconds on macOS. Statement comparison, permitted-axiom checks and Lean kernel replay passed; the trusted size driver measured 15,701 instructions and 88 data bytes. macOS is a development check; hosted verification supplies the production isolation/resource checks.

Command: python3 .contract/verifier/verify.py upper-riscv-hint --source . (local invocation used the same deployed core via --trusted and a prebuilt --lake).

Deployed contract: ca67ddc3fc9d; contract ID: 2e8ba38cb5cfb50d5446e9a5f200ca35ef459317e6ca7b7eb75f3ec1d663411e.