WIP: Jcb/ixvm consistency - #632

Open

johnchandlerburnham wants to merge 30 commits into

mainfrom

jcb/ixvm-consistency

Commits on Sep 13, 2026

Add Ix.Kernel certified checking and set-model consistency proofs
johnchandlerburnham
committed
489b66d
Prove relative consistency for an atomic checkEnvAnon fragment
johnchandlerburnham
committed
76dc310
Simplify kernel certification proofs and documentation
johnchandlerburnham
committed
8172135
Make verification documentation self-contained
johnchandlerburnham
committed
4abe7af
Add typed Ixon inputs to certified checking commands
johnchandlerburnham
committed
9615301
Refine polymorphic constant inference into the set model
johnchandlerburnham
committed
1bd7a44
Extend production environment consistency to polymorphic specializations
johnchandlerburnham
committed
ec40b6f
Extend production consistency to dependent function bodies
johnchandlerburnham
committed
2e45671
Refine applications and constant references in function bodies
johnchandlerburnham
committed
7ee64b4
Refine polymorphic constant calls inside function bodies
johnchandlerburnham
committed
4835e6e
Refine constant cache hits in function inference
johnchandlerburnham
committed
caa9826
Prove inference cache preservation for sorts and loaded constants
johnchandlerburnham
committed
6ff0cca
Carry cache preservation through recursive inference
johnchandlerburnham
committed
cc67fff
fix(aiur): reject forged results and cyclic call traces
johnchandlerburnham
committed
3cec1f8
perf(aiur): derive callee ranks and cache claim shapes
johnchandlerburnham
committed
fd9b62b
fix(aiur): reject Merkle caps that omit trace matrices
johnchandlerburnham
committed
9c390fd
perf(aiur): specialize IxVM call ranks by checked components
johnchandlerburnham
committed
9df0532
perf(aiur): tune lookup groups using compiled degree costs
johnchandlerburnham
committed
11fd8a5
perf(aiur): reduce host memory and correct shard estimates
johnchandlerburnham
committed
37daf7c
Check Aiur emission inputs and conservative folded degrees
johnchandlerburnham
committed
df3ceb0

Navigation Menu

WIP: Jcb/ixvm consistency - #632

WIP: Jcb/ixvm consistency#632
johnchandlerburnham wants to merge 30 commits into
mainfrom
jcb/ixvm-consistency

Commits on Sep 13, 2026

Add Ix.Kernel certified checking and set-model consistency proofs

Prove relative consistency for an atomic checkEnvAnon fragment

Simplify kernel certification proofs and documentation

Make verification documentation self-contained

Add typed Ixon inputs to certified checking commands

Refine polymorphic constant inference into the set model

Extend production environment consistency to polymorphic specializations

Extend production consistency to dependent function bodies

Refine applications and constant references in function bodies

Refine polymorphic constant calls inside function bodies

Refine constant cache hits in function inference

Prove inference cache preservation for sorts and loaded constants

Carry cache preservation through recursive inference

fix(aiur): reject forged results and cyclic call traces

perf(aiur): derive callee ranks and cache claim shapes

fix(aiur): reject Merkle caps that omit trace matrices

perf(aiur): specialize IxVM call ranks by checked components

perf(aiur): tune lookup groups using compiled degree costs

perf(aiur): reduce host memory and correct shard estimates

Check Aiur emission inputs and conservative folded degrees

Commits on Sep 14, 2026

Port and audit Aiur proofs on optimized layouts

Prove optimized AIR execution from physical traces

Extend consistency readings and maintained cache invariants

Reject circular safe definitions in host kernels

Preserve model readings through local values and binder opening

Derive production let traces and preserve substituted type readings

Preserve local scopes and state through general inference

Make anonymous ingress total and preserve checker state

Close local-state preservation through the recursive checker

Verify termination-checked recursion survives dependency guards