Independent parser
The proof kernel does not reuse the production compiler's parse result.
Evidence ceiling E3Proof boundary
SITE 60 · PROOF-CARRYING COMPILATION
Do not ask a third party to trust the compiler.
The v0.18 proof kernel independently parses the declared Structured/RCL subset, recomputes source semantics, recomputes IR semantics and rejects the proof bundle if the two projections differ. The current mechanism is executable proof-carrying verification, with a mechanized theorem prover as the explicit next assurance target.
Current proof boundary
REFERENCE PROOF VERIFIES
The verifier is deliberately smaller than the compiler and follows an independent parse/projection path.
- SOURCE SEMANTICS
- sha256:fba1b9d7f3d6dd1dd9afd00e6341eddfe20dec30dde7fcafae1eb18d1c380e57
- IR SEMANTICS
- sha256:fba1b9d7f3d6dd1dd9afd00e6341eddfe20dec30dde7fcafae1eb18d1c380e57
- PROOF HASH
- sha256:06b64381259b2e6dc7925a20dedb3ce93c06301f2ee739490cbfd4b7ea03e168
- RULES
- 8
- COMPCERT-CLASS THEOREM
- NOT CLAIMED
- MECHANIZED TARGET
- YES
Why this matters
Tests can pass while a compiler still changes meaning.
Site 60 separates a test suite from a portable proof object. A relying implementation can reject altered IR without trusting the Finality compiler process that created it.
Semantic equality
Source semantics and emitted IR semantics must hash identically.
Tamper detection
Changing a predicate, source, authority, contradiction or temporal rule invalidates the proof.
Fail closed
Unknown directives or unsupported source constructs cannot be silently inferred.
Portable proof
Proof rules and hashes travel with Reality IR.
Future theorem
Formal source/IR semantics can later be lifted into Rocq/Lean/Isabelle without changing the wire identity.