Skip to content

Register accesses now diverge from spec #569

Closed

Description

@jotabulacios

PR #493 changed how register accesses are proven (removed MEMW_R, added REGISTER_RELOAD, moved the access logic into the CPU chip). These changes were made directly in the prover and are not reflected in specs_vm/spec/.

Before this can be considered final we need to investigate:

  • Is the new model (register accesses on the CPU chip + REGISTER_RELOAD for gaps > 65534) the one we want to commit to long-term, or a temporary perf hack?
  • If it stays, the spec needs to be updated: drop MEMW_R, add REGISTER_RELOAD, and document the new CPU columns and Memory-bus interactions.
  • If not, decide what the spec-compliant version looks like and whether the perf gain (-31% prove time) justifies the divergence in the meantime

Activity

  1. added
    specUpdates and improvements to the spec document
    on Jun 2, 2026
  2. RobinJadoul commented on Jun 2, 2026

    @RobinJadoul
    Collaborator

    This may also enable eliminating e.g. read_register1 as write_register would still prevent writing anything else to x0

  3. erik-3milabs commented on Oct 14, 2026

    @erik-3milabs
    Collaborator

    @jotabulacios given that #493 was closed, is this issue still relevant?

  4. jotabulacios commented on Oct 14, 2026

    @jotabulacios
    CollaboratorAuthor

    Closing it
    Thanks for checking!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    specUpdates and improvements to the spec document

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions