Skip to content

AFFIRMATION.adoc

Latest commit

 

History

History
49 lines (39 loc) · 2.57 KB

AFFIRMATION.adoc

File metadata and controls

49 lines (39 loc) · 2.57 KB
Raw

AFFIRMATION — Haec

A dated, ground-truthed honesty snapshot. This is the brief’s "STATUS" for Haec: what exists, what is verified, what is deferred — stated plainly, no overclaim.

As of 2026-06-22

What exists (design pass): the surface grammar (design/grammar.ebnf), the elaboration table with a per-construct lowering-correctness (O2) obligation (design/elaboration.adoc), and examples/ pairing small programs with their lowered Trope IR.

Ground truth: every examples/*.ir.json is schema-valid against the IR contract and round-trips through the sibling trope-checker to the verdict the example states (faithful record → p-sufficient; survey collapse → p-insufficient, witness = the collapse edge; labelled aggregate fuse → p-sufficient). just check validates this standalone against the vendored schema.

What does NOT exist yet (deferred, named): the compiler (parser, type-checker, elaborator, codegen — compiler/STATUS.adoc), the LSP (lsp/STATUS.adoc), and a runtime. The O2 lowering-correctness proofs are stated as obligations, not yet discharged (HC-5: stated, not asserted-as-done).

Honest scope: Haec is one front-end among many; it defines neither the checker nor the vocabulary. Its sole present claim is that its elaboration targets the IR and its examples lower to IR the checker accepts.

— Authored by the build agent under owner direction; signed in git history.

As of 2026-10-27

Ground truth (run here, UTC 07:49, haec e9bee39): TROPECHECK_REQUIRED=1 TROPECHECK_BIN=/path/to/tropecheck-rs bash tests/check-examples.sh (the path is a placeholder for the built fast core) → the three examples (faithful-record, survey-collapse, station-average) lower to well-formed Trope IR; the vendored design/trope-ir.schema.json matches the canonical checker schema; all three round-trip through the checker to the verdict each states — faithful-record p-sufficient, survey-collapse p-insufficient with witness e_collapse/fate.quality, station-average p-sufficient. "examples: all lower to valid Trope IR." The checker was the Rust fast core built from trope-checker 44020f9 (main 216f23b plus the two Phase 0 spec/CI patches, which do not touch src/rust).

Still true, stated once: no compiler, no LSP, no runtime; the O2 lowering obligations in design/elaboration.adoc are stated, not discharged; no proofs of our own.