IxVM: cheaper shard checking via an addr-first kernel, plus soundness hardening - #529

Merged

johnchandlerburnham merged 19 commits into

mainfrom

Aug 3, 2026

Commits on Aug 1, 2026

IxVM: cheaper shard checking via an addr-first kernel, plus soundness hardening
arthurpaulino
committed
Lean witness scope mirrors Rust witness_scope; bench counts checked constants
arthurpaulino
committed
Kernel: walk refs by positive constant-use, not by blob exclusion
arthurpaulino
committed

Commits on Aug 2, 2026

Kernel: validate Str literals as UTF-8 at conversion
arthurpaulino
committed
Witness: seed constant and blob channels independently
arthurpaulino
committed
Shard claim: frontier edges follow positive constant-use
arthurpaulino
committed
Kernel: decompose projection indices with a constrained byte hint
arthurpaulino
committed
Kernel: bar safe definitions from self-reference, and from partial ones
arthurpaulino
committed
Kernel: substitute parameter args in nested positivity
arthurpaulino
committed
Kernel: keep computed Nat literals canonical
arthurpaulino
committed
Kernel: require def-eq types before struct-eta
arthurpaulino
committed
Ixon: bound Tag0/Tag2 payload width to 8 bytes
arthurpaulino
committed
Tests: make the guards that should have caught these actually fail
arthurpaulino
committed
Keep debug entrypoints out of the production verifying key
arthurpaulino
committed
Kernel: compare recursor rules without the prover's own context
arthurpaulino
committed
Kernel: pin recursor rule labels against the constructor they name
arthurpaulino
committed
Kernel: iota requires the major's constructor to belong to the recursor
arthurpaulino
committed
Shards: fail coverage when a constant's bytes do not parse
arthurpaulino
committed

Commits on Aug 3, 2026

Compile: key the universe cache by its parameter context
arthurpaulino
committed