Add self-contained kernel verification and relative consistency for environment checking - #630

Closed

johnchandlerburnham wants to merge 63 commits into

mainfrom

jcb/ix-kernel-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
Preserve cached witnesses through standalone lazy loading
johnchandlerburnham
committed
179d25c
Preserve cached witnesses through mutual-block loading
johnchandlerburnham
committed
acfc296
Preserve intern coherence through lazy loading
johnchandlerburnham
committed
b53bd32

Commits on Sep 14, 2026

Commits on Sep 15, 2026