check_sequence_contract_alignment.py

#!/usr/bin/env python3
"""Reproduce the bounded statement-level sequence-contract comparison."""

import hashlib
import json
from pathlib import Path


ROOT = Path(__file__).resolve().parents[3]


def read(relative):
    return (ROOT / relative).read_text(encoding="utf-8")


def load(relative):
    return json.loads(read(relative))


def digest(relative):
    return hashlib.sha256((ROOT / relative).read_bytes()).hexdigest()


direct_path = "public/reading-editions/direct-palindrome-scaffolding.html"
causal_path = "public/reading-editions/persistent-scaffold-causal-algebra.html"
direct = read(direct_path)
causal = read(causal_path)

direct_markers = {
    "conditional_theorem": "For a persistent sequence implementation satisfying the contract of Section 11.1",
    "conditional_corollary": "Under the sequence contract in Theorem 12.2",
    "implementation_is_informal": "These are informal source-level arguments for the contract in Section 11.1",
    "provenance_not_complete": "does not yet establish complete old/fresh pointer provenance",
    "parts_are_distinct": "The implementation evidence and the generic conditional construction should therefore be read as distinct parts of the argument",
    "draft_5_history": "Draft 5, 21 September 2026",
}
causal_markers = {
    "application_wording": "an explicit strict source-record implementation, its resource certificate, and a whole-client symbolic-normalization theorem",
    "abstract_model_scope": "in that companion’s stated abstract model",
    "generic_compiler_separate": "This paper proves only that a bounded opaque source program",
    "stale_reference_label": "Draft 4 corrected reading edition, 10 September 2026",
}

for name, marker in direct_markers.items():
    assert marker in direct, f"direct marker absent: {name}"
for name, marker in causal_markers.items():
    assert marker in causal, f"causal marker absent: {name}"

typed = load("data/direct-palindrome-typed-ast-certificate.json")
frontier = load("data/direct-palindrome-cat-ir-frontier.json")
context = load("data/direct-palindrome-context-specialization-contract-output.json")

assert any("not derived" in item for item in typed["checked_boundary"])
assert frontier["cat_frontier"]["ready_for_old_fresh_interpretation"] is False
assert frontier["cat_frontier"]["slot_admission"]["context_sensitive_slots_resolved"] == 0
assert context["semantic_instance_contract"]["instance_count_known"] is False
assert "no old/fresh interpretation executed" in context["claim_boundary"]
assert "no numerical radius derived" in context["claim_boundary"]

result = {
    "status": "pass",
    "scope": "statement-level alignment; not a proof of the sequence implementation or palindrome theorem",
    "paper_sha256": {
        "direct_html": digest(direct_path),
        "causal_html": digest(causal_path),
    },
    "direct_statement": {
        "theorem_is_conditional_on_sequence_contract": True,
        "source_evidence_is_explicitly_informal": True,
        "complete_old_fresh_provenance_automated": False,
        "direct_current_edition": "Draft 5, 21 September 2026",
    },
    "causal_statement": {
        "generic_compiler_is_separate": True,
        "palindrome_application_is_scoped_to_companion_abstract_model": True,
        "description_uses_stronger_implementation_language": True,
        "bibliography_still_names_direct_draft_4": True,
    },
    "source_evidence": {
        "typed_units": 3,
        "typed_expressions": 3912,
        "typed_direct_calls": 454,
        "cat_reachable_bindings": frontier["cat_frontier"]["resolved_binding_count"],
        "cat_slots": frontier["cat_frontier"]["slot_admission"]["syntactic_slots"],
        "context_sensitive_source_sites": frontier["cat_frontier"]["slot_admission"]["classifications"]["requires-contextual-type-specialization"],
        "context_sensitive_sites_resolved": frontier["cat_frontier"]["slot_admission"]["context_sensitive_slots_resolved"],
        "old_fresh_interpretation_executed": False,
        "numerical_radius_derived": False,
    },
}

print(json.dumps(result, indent=2, ensure_ascii=False))