Ixon v3: usage, ownership, and relative locality in the Ix frontend

[johnchandlerburnham]

Summary

The Ix frontend needs to preserve resource contracts through Lean elaboration,
compilation, content addressing, and downstream validation. This PR implements
Ixon v3 with independent usage, ownership, and relative-locality annotations,
transports them through the Lean and Rust compilers, and adds native resource
validation for the supported annotated fragment.

Ordinary Lean code keeps its existing typing and computational interpretation.
Its binders receive unrestricted usage, shared ownership, and unrestricted
locality. IxVM continues to prove ordinary Lean typing with contracts erased.
Explicit resource annotations are checked by the native admission layer; IxVM
resource proofs and backend ownership/locality optimizations remain future work.

The serialized format changes. V3 changes canonical bytes, content addresses,
primitive pins, and claim/proof envelopes. Existing artifacts require regeneration.

Ordinary Lean defaults and the IxVM boundary

Ordinary source construct	Ixon v3 contract
Lambda or forall input	many, shared ownership, unrestricted locality
Arrow result	Shared ownership, unrestricted locality
Let binding	Ordinary value let, many, shared ownership, unrestricted locality; preserves the dependency flag

Both compilers use these defaults for unannotated source, including implicit and
instance binders. Lean's native @& metadata retains its existing role and grants
no additional resource permissions. Ordinary components keep the existing
compilation path without new resource obligations.

IxVM preserves the contract fields when decoding, serializing, hashing, and
revealing Ixon. Conversion into its typing representation erases those fields;
a shared-borrow let has the ordinary let's erased interpretation. Its Check
and CheckEnv proofs therefore retain their ordinary-typing meaning.

Validation boundary	What success establishes
Ordinary Lean/Rust kernel checking	Erased Lean typing
Native resource admission	Resource rules plus erased typing of the same addressed environment
IxVM Check / CheckEnv	Erased Lean typing, validator erased-lean-v1
IxVM Reveal / Contains	The requested structural statement
IxVM Resource	Explicitly unsupported; the request rejects

Format and validator identities are committed in the envelopes. A native
resource claim additionally binds the complete constant-set root and the
canonical resource profile. Consumers that rely on ownership or locality must
require resource admission separately from an IxVM typing proof.

Annotation model and source syntax

The three axes are independent:

Axis	Syntax	Meaning
Usage	0, 1, &, unmarked	Erased, exactly once, at most once, unrestricted
Ownership	!, unmarked	Unique, shared
Locality	~, unmarked	Local to an implicit scope, unrestricted

~! combines local scope and unique ownership. For example:

import Ix.Compile.SourceContract.Elab

def plainIdentity (x : Nat) : Nat := x

def localIdentity (~1 x : Nat) : ~ Nat := x

The second definition consumes its local input once and returns it under a local
result contract. Input and result contracts belong to individual arrows, including
intermediate arrows in curried functions.

Annotations are supported in definition headers, lambda and forall binders,
dependent arrows, arrow results, and lets. An explicit let borrow creates a
shared view whose loan lasts for the let body. Its initializer identifies an
owner binding or supported projection path.

Locality is relative to the caller and lexical scopes. Contracts carry no named
lifetimes, region parameter lists, or region arguments. App, Ref, and Recur
keep their ordinary roles. See the
source syntax and API specification.

Source transport and native validation

• Source registration records exact elaborated declarations and binder
  occurrences. Imports preserve registrations, including opaque bodies.
  Stale snapshots, missing registrations, and conflicting annotations reject.
• Contracts are resolved before canonicalization and sharing. Both compilers
  distinguish otherwise equal terms with different contracts in semantic
  equality, ordering, caches, sharing, bytes, and addresses.
• Decompilation reconstructs committed contracts independently of optional
  presentation metadata.
• Both production compilers validate resources and erased types before emitting
  annotated output. Invalid or unsupported annotated inputs produce no artifact,
  including with partial compilation enabled.
• Admission follows referenced interfaces and mutual blocks, so an unannotated
  alias cannot discard an imported resource obligation.

The Lean and Rust resource checkers enforce quantitative use, unique moves,
permanent sharing, active shared loans, reborrowing, local escape, and closure
captures. They account for calls, partial applications, recursive interfaces,
and profile-admitted alternative-path behavior. Analysis is bounded and rejects
unsupported cases or exhausted limits.

Ix.Resource.validate and ix_kernel::resource::validate consume the canonical
addressed environment and a profile. Profiles bind external assumptions,
shareable representations, selection primitives, literal identities, and
analysis limits. Optional metadata or cached materializations confer no
permissions. Native makeClaim and checkClaim bind and validate the complete
subject and profile.

Supported fragment and deferred infrastructure

• Transport and admission support definitions, theorems, opaque bodies, and
  explicitly admitted external interfaces.
• Annotated inductive/constructor/recursor generation and nonidentity compiler
  transformations reject before emission.
• The initial projection fragment uses closed, transparent field types with
  unrestricted field usage; availability is tracked for the whole owner.
• Resource checking requires visible arrow interfaces after bounded
  normalization. Unsupported higher-order or representation assumptions reject.
• A dedicated resource-checking CLI, richer diagnostics, annotation inference,
  and broader generated resource-program testing remain follow-up work.
• IxVM resource enforcement and proofs, whole-checker operational soundness,
  and backend allocation/reuse strategies remain follow-up work.
• Compilatrix changes are external to this PR. The
  consumer handoff
  supplies complete accepted/rejected environments, a profile, a resource claim,
  and exact identities for downstream integration.

The detailed admitted fragment is documented in
resource checking.

Format and consumer migration

• Environment format becomes 3; catalog-manifest format becomes 2.
• The twelve expression variants and existing declaration headers remain.
• Lambda input contracts occupy four bits. Forall input/result contracts occupy
  six bits. Lets carry a binder byte and dependency/shared-borrow flags.
• Lean, Rust, and IxVM codecs, text syntax, FFI layouts, equality, sharing hashes,
  claims, catalogs, and decompilation use the same v3 fields.
• Readers reject nonminimal encodings, reserved bits, invalid flags, malformed
  counts, noncanonical telescopes, truncation, and whole-object trailing bytes.
  IxVM uses strict incremental reads for counted sequences.
• Primitive addresses and independent byte/address fixtures are regenerated.
  The generated Rust kernel and recursive consumers match their current Aiur
  sources. The historical Mathlib proof fixture retains its pinned identity and
  rejects at the incompatible envelope header.

See the v3 specification
and wire format.

Verification

The compiler audit covers 143 roots. The ordinary typechecker audits cover
2,034 completed roots, one conditional root, and seven statement roots, with
existing assumptions recorded in their manifests. The resource audit covers
15 roots tied to executable quantitative, scope, ownership, loan-ending, and
join invariants. Local sorry-frontier audits pass; no new axioms or local
sorry placeholders were added.

The resource theorems establish the stated checks and transition invariants.
A theorem connecting the entire resource checker to machine operational
semantics remains future work.

Executed checks

Area	Result
Lean proof/module builds and lake lint -- --wfail	Passed
Primary suite and CLI suite	Passed; includes fresh-process imports, annotated emission, and rejection without output
Ordinary production corpus	6,656 source constants; Lean serial/parallel and Rust emit identical v3 bytes and metadata; all source constants decompile without mismatches
Compile determinism	Fixture corpus and Batteries produce identical files in separate processes
Dedicated v3 suite	1,844 golden/rejection checks, 475 FFI/sharing checks, 3,639 VM checks, 458 text checks, and resource/admission/transport suites passed
Primitive closure	3,634 constants and 3,540 addressed interfaces validated
IxVM regression suite	843 checks passed, including adversarial cases, generated/interpreter parity, 83 exact kernel FFT pins, and the shard pin
Code generation	ix codegen --check passes for all three generated consumers
Rust formatting, Clippy, and build checks	Passed for the affected workspace and CI features
Rust release tests / nextest	1,563 passed; 14 existing ignored/skipped tests

The new counted-decoding regressions cover all 11 affected paths with complete
single-element inputs and truncated inputs declaring two or UInt64.max
elements. Rejection is checked during decoding, before reserialization.

Specialized CUDA, SP1, and Zisk toolchain jobs were not run locally. Commands,
counts, trust boundaries, and migration evidence are recorded in the
verification record.

FFT cost

The final deterministic estimates increase by 0.008%–1.278% across the
83 existing kernel cases compared with the pre-v3 baseline. Exact equality
assertions are retained.

Case	Pre-v3	This PR	Change
Nat.add_comm	321,012,193	322,598,714	+0.494%
Shard fixture	6,999,296,124	7,072,190,269	+1.041%

These are estimates of FFT work. They are derived from the actual circuit
shapes and execution query counts.

Review map

Area	Main files
Contracts and canonical representation	Ix/IxonContract.lean, Ix/Ixon.lean, crates/ixon/src/contract.rs, codecs and sharing
Source registration, syntax, and transport	Ix/Compile/SourceContract/, Ix/SemanticContract.lean, crates/compile/src/semantic_contract.rs
Production integration	Ix/CompileDriver.lean, Ix/CompileM.lean, crates/compile/src/compile/, FFI adapters
Native resource checking and admission	Ix/Resource/, crates/ixon/src/resource/, crates/ixon/src/resource.rs, crates/kernel/src/resource.rs
IxVM representation and proof boundary	Ix/IxVM/Ixon*.lean, Ix/IxVM/Convert.lean, Ix/IxVM/Kernel/Claim.lean, claim/catalog/aggregate consumers
Formal verification	Ix/Compile/Verify/, affected Ix/Tc/Verify/ modules, Ix/Resource/Audit.lean
Regression evidence and handoff	Tests/Ix/, Tests/Fixtures/ixon-v3/, CLI tests, v3 test executables, docs/

Most of the line churn is regenerated Rust in crates/ixvm-codegen/src/.
Its consistency is checked by regeneration and execution/query-count parity.