-
Notifications
You must be signed in to change notification settings - Fork 0
All issues
Issue creation is restricted in this repository
- #173 · codygunton opened
on Jun 28, 2026
Issues
is:issue state:open
is:issue state:open
Search results
Five vestigial _of_table compatibility binders pinned by frozen Equivalence/ signatures (owner decision)
infraTooling / housekeeping / legibility refactor; not proof content on either axisTooling / housekeeping / legibility refactor; not proof content on either axisStatus: Open.#282 In eth-act/zisk-fv;ArithTable standalone module: projection facts over-claim beyond ROM data (np = na XOR nb, W-mode sext = 0)
soundnessCircuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Circuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Status: Open.#281 In eth-act/zisk-fv;Main source-C copy constraint (main.pil:386) has no live or transition home — carried as JALR-bridge premises
soundnessCircuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Circuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Status: Open.#280 In eth-act/zisk-fv;Live ensemble validates an incomplete Arith provider circuit — model-coverage gap class
soundnessCircuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Circuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Status: Open.#279 In eth-act/zisk-fv;MemAlign-family read-soundness discharge (follow-on to #115, gated on MemAlignRom extraction)
mvpRequired for the two legible root theorems (non-vacuous + every premise derived or named trust)Required for the two legible root theorems (non-vacuous + every premise derived or named trust)soundnessCircuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Circuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Status: Open.#242 In eth-act/zisk-fv;Trace-acquisition tool: dump real ZisK witness row literals + Sail states for root_soundness instantiations (#74)
infraTooling / housekeeping / legibility refactor; not proof content on either axisTooling / housekeeping / legibility refactor; not proof content on either axisStatus: Open.root_soundness instantiation: load with a real multi-row memory prefix (non-degenerate memory, #74)
mvpRequired for the two legible root theorems (non-vacuous + every premise derived or named trust)Required for the two legible root theorems (non-vacuous + every premise derived or named trust)soundnessCircuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Circuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Status: Open.Proof-tower naming/structure refactor for human navigability (legibility of the two root theorems)
infraTooling / housekeeping / legibility refactor; not proof content on either axisTooling / housekeeping / legibility refactor; not proof content on either axismvpRequired for the two legible root theorems (non-vacuous + every premise derived or named trust)Required for the two legible root theorems (non-vacuous + every premise derived or named trust)Status: Open.#186 In eth-act/zisk-fv;Reader-facing premise audit of root_soundness: classify InputsAgree/SailTrace fields, document the irreducible-trust core
mvpRequired for the two legible root theorems (non-vacuous + every premise derived or named trust)Required for the two legible root theorems (non-vacuous + every premise derived or named trust)soundnessCircuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Circuit faithfully implements the Sail spec (equivalence, trust, defects, extraction fidelity)Status: Open.Completeness non-vacuity: concrete OutstandingZiskPredicates instance from a real trace (completeness sibling of #74)
completenessEvery valid RV64IM instruction is covered/processed (decode coverage, Aeneas harness)Every valid RV64IM instruction is covered/processed (decode coverage, Aeneas harness)mvpRequired for the two legible root theorems (non-vacuous + every premise derived or named trust)Required for the two legible root theorems (non-vacuous + every premise derived or named trust)Status: Open.#183 In eth-act/zisk-fv;Promote skeletal_root_completeness → root_completeness: wire the proven decoder (#164) + Aeneas lowering (#111/#159) into a concrete OutstandingZiskPredicates
completenessEvery valid RV64IM instruction is covered/processed (decode coverage, Aeneas harness)Every valid RV64IM instruction is covered/processed (decode coverage, Aeneas harness)mvpRequired for the two legible root theorems (non-vacuous + every premise derived or named trust)Required for the two legible root theorems (non-vacuous + every premise derived or named trust)Status: Open.#182 In eth-act/zisk-fv;De-native_decide the Sail-decode encode-equality bridge (make PR #164's Sail↔ZisK match kernel-sound)
beyond-mvpStrengthening/hardness beyond the legible-root-theorems bar (trust-base, re-checks, spec validation)Strengthening/hardness beyond the legible-root-theorems bar (trust-base, re-checks, spec validation)completenessEvery valid RV64IM instruction is covered/processed (decode coverage, Aeneas harness)Every valid RV64IM instruction is covered/processed (decode coverage, Aeneas harness)Status: Open.#174 In eth-act/zisk-fv;