Skip to content

Labels

Labels

16 labels

  • bug

    bug
    Something isn't working

  • build-performance

    build-performance
    Elaboration / rebuild cost: module splits, import hygiene, CI wall-clock. Not proof content.

  • completeness

    completeness
    Every valid RV64IM instruction is covered/processed (decode coverage, Aeneas harness)

  • documentation

    documentation
    Improvements or additions to documentation

  • duplicate

    duplicate
    This issue or pull request already exists

  • enhancement

    enhancement
    New feature or request

  • good first issue

    good first issue
    Good for newcomers

  • help wanted

    help wanted
    Extra attention is needed

  • infra

    infra
    Tooling / housekeeping / legibility refactor; not proof content on either axis

  • invalid

    invalid
    This doesn't seem right

  • mvp

    mvp
    Required for the two legible root theorems (non-vacuous + every premise derived or named trust)

  • question

    question
    Further information is requested

  • run-ci

    run-ci
    Trigger proofs CI on this PR

  • soundness

    soundness
    Circuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)

  • testing

    testing

  • wontfix

    wontfix
    This will not be worked on