# This Source Code Form is subject to the terms of the Mozilla Public # License, v. 2.0. If a copy of the MPL was not distributed with this # file, You can obtain one at https://mozilla.org/MPL/2.0/. """Phase 14: Verification engine — all checks before artifact emission.""" from __future__ import annotations from dataclasses import dataclass, field from typing import Callable from .boolean_engine import BooleanNormalForm, normalize from .ir import Artifact, SemanticIR from .latin import LatinCanonicalForm, vocabulary from .rosetta import RosettaMapping from .subleq import SubleqProgram, SubleqVM from .token_engine import BooleanTokenStream, round_trip from .types import FSMState, VerificationError, VerificationState # ── Check result ────────────────────────────────────────────────────────────── @dataclass class CheckResult: name: str passed: bool message: str = "" def __repr__(self) -> str: status = "✓" if self.passed else "✗" return f"{status} {self.name}: {self.message}" @dataclass class VerificationReport: checks: list[CheckResult] = field(default_factory=list) state: VerificationState = VerificationState.UNVERIFIED @property def passed(self) -> bool: return all(c.passed for c in self.checks) def add(self, result: CheckResult) -> None: self.checks.append(result) def summary(self) -> str: lines = [repr(c) for c in self.checks] lines.append(f"\nResult: {'VERIFIED' if self.passed else 'REJECTED'}") return "\n".join(lines) # ── Individual checks ───────────────────────────────────────────────────────── def check_type_correctness(ir: SemanticIR) -> CheckResult: for node in ir.nodes: if node.operation and node.operation.arity != len(node.operands): if node.operation.arity > 0: return CheckResult( "type_correctness", False, f"Node {node.id}: arity {node.operation.arity} but {len(node.operands)} operands", ) return CheckResult("type_correctness", True, "all arities match") def check_geometry(ir: SemanticIR) -> CheckResult: for node in ir.nodes: if node.geometry and node.operation and node.operation.name == "multiply": if len(node.operands) >= 2: a = node.operands[0].geometry b = node.operands[1].geometry if a and b and a.col is not None and b.row is not None: if a.col != b.row: return CheckResult( "geometry", False, f"Matrix dim mismatch: A.col={a.col} ≠ B.row={b.row}", ) return CheckResult("geometry", True, "all dimensions compatible") def check_temporal_state(ir: SemanticIR) -> CheckResult: transitions = ir.temporal_lock.audit() for t in transitions: if not t.is_valid(): return CheckResult( "temporal_state", False, f"Invalid τ transition: {t.from_tau} → {t.to_tau}", ) return CheckResult("temporal_state", True, f"{len(transitions)} temporal transitions valid") def check_boolean_normalization(bnf: BooleanNormalForm) -> CheckResult: if not bnf.stable: bnf.verify_stability() if not bnf.stable: return CheckResult("boolean_normalization", False, "normalize(normalize(x)) ≠ normalize(x)") return CheckResult("boolean_normalization", True, "normalization idempotent") def check_token_round_trip(stream: BooleanTokenStream) -> CheckResult: try: from .token_engine import decode_binary, encode_binary binary = encode_binary(stream) decoded = decode_binary(binary) if len(decoded.tokens) != len(stream.tokens): return CheckResult("token_round_trip", False, f"Token count mismatch: {len(stream.tokens)} → {len(decoded.tokens)}") for orig, dec in zip(stream.tokens, decoded.tokens): if orig.token_type != dec.token_type or orig.payload != dec.payload: return CheckResult("token_round_trip", False, f"Token mismatch at pos {orig.position}") return CheckResult("token_round_trip", True, "encode/decode invariant holds") except Exception as e: return CheckResult("token_round_trip", False, str(e)) def check_latin_vocabulary(form: LatinCanonicalForm) -> CheckResult: vocab = vocabulary() for tok in form.tokens: if tok.lexeme not in vocab and tok.lexeme not in ("OPUS",): return CheckResult( "latin_vocabulary", False, f"Lexeme '{tok.lexeme}' not in controlled vocabulary", ) return CheckResult("latin_vocabulary", True, "all lexemes in vocabulary") def check_rosetta_mapping(mapping: RosettaMapping) -> CheckResult: if not mapping.complete: unmapped = [t.semantic_id for t in mapping.unmapped] return CheckResult("rosetta_mapping", False, f"Unmapped: {unmapped}") return CheckResult("rosetta_mapping", True, f"{len(mapping.entries)} entries mapped") def check_subleq_validity(prog: SubleqProgram) -> CheckResult: if not prog.instructions: return CheckResult("subleq_validity", False, "Empty SUBLEQ program") vm = SubleqVM(max_steps=10_000) halts = vm.verify_halts(prog) if not halts: return CheckResult("subleq_validity", False, "Program does not halt within limit") return CheckResult("subleq_validity", True, f"{len(prog.instructions)} instructions, halts") def check_artifact_provenance(artifact: Artifact, ir: SemanticIR) -> CheckResult: if artifact.semantic_root != ir.ir_id: return CheckResult( "artifact_provenance", False, f"Artifact root {artifact.semantic_root} ≠ IR id {ir.ir_id}", ) return CheckResult("artifact_provenance", True, "provenance chain intact") def check_template_bindings(artifact: Artifact) -> CheckResult: if not artifact.template: return CheckResult("template_bindings", False, "No template bound to artifact") if not artifact.content: return CheckResult("template_bindings", False, "Artifact content is empty") return CheckResult("template_bindings", True, "template bound and content non-empty") # ── Verification engine ─────────────────────────────────────────────────────── class Verifier: def verify_ir(self, ir: SemanticIR) -> VerificationReport: report = VerificationReport(state=VerificationState.VALIDATING) report.add(check_type_correctness(ir)) report.add(check_geometry(ir)) report.add(check_temporal_state(ir)) report.state = VerificationState.VERIFIED if report.passed else VerificationState.REJECTED return report def verify_boolean(self, bnf: BooleanNormalForm) -> VerificationReport: report = VerificationReport(state=VerificationState.VALIDATING) report.add(check_boolean_normalization(bnf)) report.state = VerificationState.VERIFIED if report.passed else VerificationState.REJECTED return report def verify_tokens(self, stream: BooleanTokenStream) -> VerificationReport: report = VerificationReport(state=VerificationState.VALIDATING) report.add(check_token_round_trip(stream)) report.state = VerificationState.VERIFIED if report.passed else VerificationState.REJECTED return report def verify_latin(self, form: LatinCanonicalForm) -> VerificationReport: report = VerificationReport(state=VerificationState.VALIDATING) report.add(check_latin_vocabulary(form)) report.state = VerificationState.VERIFIED if report.passed else VerificationState.REJECTED return report def verify_rosetta(self, mapping: RosettaMapping) -> VerificationReport: report = VerificationReport(state=VerificationState.VALIDATING) report.add(check_rosetta_mapping(mapping)) report.state = VerificationState.VERIFIED if report.passed else VerificationState.REJECTED return report def verify_subleq(self, prog: SubleqProgram) -> VerificationReport: report = VerificationReport(state=VerificationState.VALIDATING) report.add(check_subleq_validity(prog)) report.state = VerificationState.VERIFIED if report.passed else VerificationState.REJECTED return report def verify_artifact(self, artifact: Artifact, ir: SemanticIR) -> VerificationReport: report = VerificationReport(state=VerificationState.VALIDATING) report.add(check_artifact_provenance(artifact, ir)) report.add(check_template_bindings(artifact)) report.state = VerificationState.VERIFIED if report.passed else VerificationState.REJECTED return report def reject_if_failed(self, report: VerificationReport, stage: FSMState) -> None: if not report.passed: raise VerificationError(stage, "Verification failed:\n" + report.summary())