Skip to content

fix(kernel): reject circular safe definitions and pin IxVM rejection - #637

Merged
arthurpaulino merged 1 commit into
mainfrom
ap/kernel
Sep 17, 2026
Merged

arthurpaulino merged 1 commit into
mainfrom
ap/kernel

Conversation

@arthurpaulino

Copy link
Copy Markdown
Member

The Rust kernel could accept a safe declaration whose value was a reference to itself: looking up the reference returned its declared type without establishing that its definition was well founded. For example, with only P : Prop as an axiom, theorem loop : P := loop was accepted. Raw Ixon can also encode an axiom-free circular definition of forall P : Prop, P, or put the same attack in a singleton or mutually dependent definition block. This is a soundness defect: invalid proofs were accepted.

Port the Rust admission guard from #630 (2f0b47c). Before typechecking a safe definition, traverse definition references in both its type and value, including binder domains, let initializers, shared syntax, and projection heads. Explicit worklists distinguish active declarations from completed ones and reject cycles, including cycles spanning internal blocks. Expression traversal deduplicates shared syntax without recursive host-stack calls. The host traversal fails closed at one million dependency tasks. Axioms, inductives, constructors, and recursors retain their own admission rules; partial and unsafe definitions retain their existing policy.

IxVM is already protected against this attack: ingress gives safe definitions neither a standalone self-reference slot nor mutual peer slots. Add hash-bound Ixon exploit fixtures to demonstrate that protection through the production verify_claim entrypoint, using both the bytecode interpreter and generated executor. Cover self-reference in definitions, theorems, and opaque declarations; mutual cycles; cycles hidden in types, let initializers, and sharing; and misleading theorem/opaque safety bytes. A closed identity proof must be accepted as a positive control. These tests require successful witness construction before checking rejection. No IxVM implementation, generated code, or FFT pin changes are needed.

The Rust unit regressions reproduced acceptance before the fix. They now reject the attacks and cover projection-head dependency collection and preservation of partial/unsafe behavior. The serialized fixtures also run through the Rust checker with hash verification enabled, requiring the cycle diagnostic for invalid targets. Positive Rust controls retain valid acyclic forward references and shared dependencies. Exported structural, well-founded, and mutual recursion fixtures check all 33, 1350, and 26 targets respectively, with no omitted requested definitions. The shared fixtures run in the focused kernel-dependencies runner and the IxVM suite.

Validation:

  • cargo test --locked --release -p ix-kernel: 846 passed, 8 ignored.
  • lake test --wfail -- --ignored kernel-dependencies: 44 checks passed.
  • cargo clippy --locked --release --workspace --all-targets --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi -- -D warnings: passed.
  • cargo fmt --all -- --check and git diff --check: passed.
  • ix codegen --check: all three generated targets are up to date.

The Rust kernel could accept a safe declaration whose value was a reference
to itself: looking up the reference returned its declared type without
establishing that its definition was well founded. For example, with only
P : Prop as an axiom, `theorem loop : P := loop` was accepted. Raw Ixon can
also encode an axiom-free circular definition of `forall P : Prop, P`, or
put the same attack in a singleton or mutually dependent definition block.
This is a soundness defect: invalid proofs were accepted.

Port the Rust admission guard from #630 (2f0b47c).
Before typechecking a safe definition, traverse definition references in
both its type and value, including binder domains, let initializers,
shared syntax, and projection heads. Explicit worklists distinguish
active declarations from completed ones and reject cycles, including
cycles spanning internal blocks. Expression traversal deduplicates shared
syntax without recursive host-stack calls. The host traversal fails closed
at one million dependency tasks. Axioms, inductives, constructors, and
recursors retain their own admission rules; partial and unsafe definitions
retain their existing policy.

IxVM is already protected against this attack: ingress gives safe
definitions neither a standalone self-reference slot nor mutual peer
slots. Add hash-bound Ixon exploit fixtures to demonstrate that protection
through the production verify_claim entrypoint, using both the bytecode
interpreter and generated executor. Cover self-reference in definitions,
theorems, and opaque declarations; mutual cycles; cycles hidden in types,
let initializers, and sharing; and misleading theorem/opaque safety bytes.
A closed identity proof must be accepted as a positive control. These
tests require successful witness construction before checking rejection.
No IxVM implementation, generated code, or FFT pin changes are needed.

The Rust unit regressions reproduced acceptance before the fix. They now
reject the attacks and cover projection-head dependency collection and
preservation of partial/unsafe behavior. The serialized fixtures also run
through the Rust checker with hash verification enabled, requiring the
cycle diagnostic for invalid targets. Positive Rust controls retain valid
acyclic forward references and shared dependencies. Exported structural,
well-founded, and mutual recursion fixtures check all 33, 1350, and 26
targets respectively, with no omitted requested definitions. The shared
fixtures run in the focused kernel-dependencies runner and the IxVM suite.

Validation:
- cargo test --locked --release -p ix-kernel: 846 passed, 8 ignored.
- lake test --wfail -- --ignored kernel-dependencies: 44 checks passed.
- cargo clippy --locked --release --workspace --all-targets
  --features ix-ffi/parallel,ix-ffi/net,ix-ffi/test-ffi -- -D warnings: passed.
- cargo fmt --all -- --check and git diff --check: passed.
- ix codegen --check: all three generated targets are up to date.

Co-authored-by: John C. Burnham <john@agathic.com>
@arthurpaulino
arthurpaulino added this pull request to the merge queue Sep 17, 2026
Merged via the queue into main with commit 0ec538e Sep 17, 2026
14 checks passed
@arthurpaulino
arthurpaulino deleted the ap/kernel branch September 17, 2026 17:01
samuelburnham added a commit that referenced this pull request Sep 23, 2026
…ecking

The definition-dependency guard from #637 walked every safe definition's
reachable dependency graph on each check. #639 exempted the anonymous
IxonChecker, whose declarations all arrive through Ixon ingress with local
cycles rejected at block admission, but the Meta-mode lazy Ixon checker
kept the traversal. Combined with the per-constant cache clear in the
whole-env FFI check, each of the 222k constants re-ingressed and re-walked
its dependency graph, taking kernel-check-env from a few minutes to 21-44
minutes and the misc merge-test partition past the merge queue timeout.

Meta ingress did not validate local Rec cycles at all, so the flag alone
would have dropped the check. Gather and validate local definition edges in
ingress_standalone and ingress_muts_block exactly as the anon ingress
functions do, then mark the lazy Ixon checker as Ixon-ingress-backed.

A Meta-mode unit test builds a two-member Muts block with Named metadata
and checks the cyclic variant is rejected before publication.
johnchandlerburnham added a commit that referenced this pull request Oct 1, 2026
Merge ix main at b413cd9 (Ixon v3, #636/#639 and seven later PRs) into the
certified kernel branch. The supported profile is unchanged; contracts are
layout data.

Conflicts: D01's 15 deletions of Ix/Compile/Verify and Ix/Tc/Verify stay
deleted; lean4lean is removed again from merge-tests.yml, BenchCmd, and the
IxTcVerify step main added to ci.yml. Ix/Resource/Audit moves to the
kernel's exact axiom guard.

v3 port: all 26 upstream Ix/Ixon.lean hunks are routed into Ix.Ixon.Types,
Ix.Ixon.Codec, and the host module; the contract types move to the pure
Ix.Ixon.Types.Contract (host IxonMode/IxonContract are shims that keep
Ix.Common). Six extracted codec proof modules take upstream's v3 revisions of
their sources, with updated provenance headers. The K4-authored proofs are
ported by hand for checkCount, canonical integer widths, strict Booleans,
flag validation, and contract bytes: Egress.Layout, ReaderBounds,
ConstantBounds, WorkTags, WorkExpr, WorkConstant.

Semantics: a let's v3 contract is erased by the reading, as at upstream
Ix.Tc's erased typing boundary, and retained by the egress layout; lambda and
forall contracts other than many/shared still decline (V2).

Audit re-records (frozen public statements unchanged):
- egress runtime closure 202 -> 206 functions, externs unchanged;
- codec closure 331 -> 355, externs 52 -> 55 (Nat.mul, UInt64.land,
  UInt8.add; Lean core);
- admission 1250 -> 1273 / 58 externs, now with an enforced no-new-extern
  check; projection 1381 -> 1404 / 72; block order 1509 -> 1532 / 79 (both
  adapter-specific extern sets unchanged).

Tests: the v3 decoder itself rejects nonminimal integers and non-Boolean
flags, while canonical decoding still rejects noncanonical universe
spellings; every contract spelling round-trips; parser-work costs are
re-pinned for v3; recursive block-order oracle cases use partial
definitions because ix #637 rejects cyclic safe blocks natively.

Validation (plans/review/v1-merge): lake run check-kernel --with-model
(189/212/645/975 jobs, 38 differential, 26/26 compiler cases with identical
verdicts and reasons on v3 inputs, 1117/1117 Rust order comparisons, model
audit); lake lint -- --wfail; lake test --wfail; ixon-v3-primitives and
ixon-v3-tests --primitives.
johnchandlerburnham added a commit that referenced this pull request Oct 1, 2026
Merge ix main at b413cd9 (Ixon v3, #636/#639 and seven later PRs) into the
certified kernel branch. The supported profile is unchanged; contracts are
layout data.

Conflicts: D01's 15 deletions of Ix/Compile/Verify and Ix/Tc/Verify stay
deleted; lean4lean is removed again from merge-tests.yml, BenchCmd, and the
IxTcVerify step main added to ci.yml. Ix/Resource/Audit moves to the
kernel's exact axiom guard.

v3 port: all 26 upstream Ix/Ixon.lean hunks are routed into Ix.Ixon.Types,
Ix.Ixon.Codec, and the host module; the contract types move to the pure
Ix.Ixon.Types.Contract (host IxonMode/IxonContract are shims that keep
Ix.Common). Six extracted codec proof modules take upstream's v3 revisions of
their sources, with updated provenance headers. The K4-authored proofs are
ported by hand for checkCount, canonical integer widths, strict Booleans,
flag validation, and contract bytes: Egress.Layout, ReaderBounds,
ConstantBounds, WorkTags, WorkExpr, WorkConstant.

Semantics: a let's v3 contract is erased by the reading, as at upstream
Ix.Tc's erased typing boundary, and retained by the egress layout; lambda and
forall contracts other than many/shared still decline (V2).

Audit re-records (frozen public statements unchanged):
- egress runtime closure 202 -> 206 functions, externs unchanged;
- codec closure 331 -> 355, externs 52 -> 55 (Nat.mul, UInt64.land,
  UInt8.add; Lean core);
- admission 1250 -> 1273 / 58 externs, now with an enforced no-new-extern
  check; projection 1381 -> 1404 / 72; block order 1509 -> 1532 / 79 (both
  adapter-specific extern sets unchanged).

Tests: the v3 decoder itself rejects nonminimal integers and non-Boolean
flags, while canonical decoding still rejects noncanonical universe
spellings; every contract spelling round-trips; parser-work costs are
re-pinned for v3; recursive block-order oracle cases use partial
definitions because ix #637 rejects cyclic safe blocks natively.

Validation (plans/review/v1-merge): lake run check-kernel --with-model
(189/212/645/975 jobs, 38 differential, 26/26 compiler cases with identical
verdicts and reasons on v3 inputs, 1117/1117 Rust order comparisons, model
audit); lake lint -- --wfail; lake test --wfail; ixon-v3-primitives and
ixon-v3-tests --primitives.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants