Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 9 additions & 3 deletions LIMITS.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,15 @@
An honest list. Items marked (spec) are declared out of scope by START.md §8;
the rest are v0 implementation boundaries.

- **No `@async`** (spec). Parsed, rejected with "not in v0". There is no
effects executor; "intention facts" are collected by the host at tick
boundaries (see `examples/counter.rofl` and the `run` API's boundary hook).
- **No `@async`** (spec), and it is not reserved for later either — decided
2026-09-16. START.md §3.3 asked the parser to know the word and answer "not
in v0", which promises the word is being kept for something; the effects
executor is not going to be built, so it was being kept for nothing. The
temporal set is closed to `@init`, `@now` and `@next`, and `@async` is now
refused as the unknown marker it is — `examples/checks/async-refused.rofl` is
that refusal, pinned. Effects still leave by the door they always had:
"intention facts" are collected by the host at tick boundaries (see
`examples/counter.rofl` and the `run` API's boundary hook).
- **No incremental maintenance** (spec). No delta is ever propagated into a
derived relation: a relation is recomputed entirely or not at all, so there
is no DRed, no counting, and none of the 4–22× memory the field pays for
Expand Down
7 changes: 5 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -291,8 +291,11 @@ atom/rel := /[a-z][A-Za-z0-9_]*/
comment := "--" to end of line
```

`@async` parses and is rejected with *"not in v0"*. `@next` is not allowed in
bodies; `@init` is not allowed on rule heads.
The temporal set is exactly the three above. `@async` was reserved syntax
until 2026-09-16 and is not reserved now — the effects executor is not going
to be built, so the word was holding a place for nothing, and it is refused as
the unknown marker it is (LIMITS.md). `@next` is not allowed in bodies;
`@init` is not allowed on rule heads.

**A relation may take ZERO arguments, spelled `p()`** — added 2026-09-10, and
the grammar above says so (`terms` may be empty). A relation of arity *n* is a
Expand Down
20 changes: 20 additions & 0 deletions examples/checks/async-refused.rofl
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
-- examples/checks/async-refused.rofl — A PROGRAM THAT MUST BE REFUSED.
--
-- `@async` WAS RESERVED SYNTAX AND IS NOT RESERVED NOW. START.md §3.3 asked
-- the parser to know the word and answer `not in v0`, which is a promise that
-- the word is being kept for something; the effects executor is not going to
-- be built, so it is being kept for nothing. The temporal set is the grammar's
-- three -- `@init`, `@now`, `@next` -- and `@async` is an unknown marker like
-- any other, refused by the one branch that refuses all of them.
--
-- WHAT IS STILL OWED IS THE REFUSAL, which is what LIMITS.md's `No @async`
-- bullet means and what this world holds. Both spellings were probed and both
-- are refused -- the marker on a PREMISE and on a HEAD -- and the head form is
-- the one kept here, because it is the one a person reaching for async would
-- write.
--
-- The golden holds THAT the file is refused and not the wording (two engines
-- word a syntax error differently and always will), so a kernel that quietly
-- starts ACCEPTING this is a red.

p(X) @async :- q(X).
15 changes: 0 additions & 15 deletions examples/checks/async-reserved.rofl

This file was deleted.

14 changes: 9 additions & 5 deletions facts/checks.rofl
Original file line number Diff line number Diff line change
Expand Up @@ -127,11 +127,15 @@ check_file("spec_coverage", "rules/spec-coverage.rofl").
check_file("spec_coverage", "facts/spec.rofl").
check_file("spec_coverage", "facts/spec-census.rofl").

-- TWO PROHIBITIONS, WRITTEN DOWN SO THE LOADER CAN REFUSE THEM. A `prohibited`
-- duty has one mechanical form -- do the forbidden thing and require a no --
-- and eleven of them had no check at all until 2026-09-12.
check_world("async_reserved").
check_file("async_reserved", "examples/checks/async-reserved.rofl").
-- TWO THINGS WRITTEN DOWN SO THE LOADER CAN REFUSE THEM. A `prohibited` duty
-- has one mechanical form -- do the forbidden thing and require a no -- and
-- eleven of them had no check at all until 2026-09-12. `async_refused` is the
-- same form standing behind a LIMIT rather than a prohibition since
-- 2026-09-16: `@async` stopped being reserved syntax when the effects executor
-- stopped being planned, and the refusal is the whole of what LIMITS.md still
-- promises about it.
check_world("async_refused").
check_file("async_refused", "examples/checks/async-refused.rofl").

check_world("unstratifiable").
check_file("unstratifiable", "examples/checks/unstratifiable.rofl").
Expand Down
7 changes: 7 additions & 0 deletions facts/findings.rofl
Original file line number Diff line number Diff line change
Expand Up @@ -6483,3 +6483,10 @@ finding_note(f_the_model_could_not_say_a_prohibition_is_kept_by_construction, "T
addressed_by(f_the_model_could_not_say_a_prohibition_is_kept_by_construction, "rules/spec-coverage.rofl").
addressed_by(f_ci_is_red_on_nextver_and_green_on_main_so_the_merge_moves_it_backwards, "facts/spec-census.rofl").
finding_note(f_ci_is_red_on_nextver_and_green_on_main_so_the_merge_moves_it_backwards, "DECIDED 2026-09-12, AND THE QUESTION IT ASKED IS NOT THE ONE THAT GOT ANSWERED. It asked WHICH OF THESE MAY CROSS INTO MAIN AS RED AND UNDER WHAT RECORD, naming three: 32 unpriced cross products from `test/rule-shape.test.ts`, 22 stale or broken witnesses from `test/witness-check.test.ts`, and an unre-measured cost pin in `test/js-layer-cost.test.ts`. NOTHING CROSSES RED -- but only ONE of the three was repaired. The other two went with `test/` on 2026-09-11, so the reds are gone because the INSTRUMENTS are gone, and the questions they asked stopped being asked rather than being answered. That is the honest shape of this settlement and it is why the disposition cites the census rather than a fix. WHAT REPLACED THEM IS A NUMBER INSTEAD OF A GUESS. `npm run speccheck` had crashed with ENOENT on the deleted directory for a day; `rules_spec-coverage` was a golden world holding ZERO duties, because the walker pairs `rules/X.rofl` with `facts/X.rofl` and the specification is `facts/spec.rofl`. Both are repaired and the answer is out: 132 duties in 7 ledgers, 146 checks in the census, COVERED 22, UNCOVERED 102, superseded 8, and ZERO prohibitions without a guard -- down from eleven in a day, six by citation, four by restatement, one by amendment, one by a signed acceptance that keeps its own row in the report. SO THE DEFAULT BRANCH TAKES A KNOWN COVERAGE RATIO RATHER THAN AN UNKNOWN ONE, which is a different and smaller claim than `the tree is guarded`. 102 duties hold because the prose says so; most are LIMITS -- sentences about what the kernel does not do -- and a limit is legitimately discharged by a document, which is what `discharged_by` is for and what only three of them use. AND ONE CHECK STILL LIES: 21 `golden_host` demo hashes are frozen, `npm run bless` carries them forward unless `--hosts` is passed, and `cram` reads red for that reason alone. It is not in CI and it is not blocking, and it is named here rather than left for whoever runs it next. CI on `nextver` is six consecutive greens, 417 through 426, against main's last verdict of 2026-08-29 -- which was green under a workflow that ran a suite the tree no longer has.").

finding(f_a_word_reserved_for_nothing_is_a_promise_the_tree_cannot_keep, decision).
recorded(f_a_word_reserved_for_nothing_is_a_promise_the_tree_cannot_keep, "2026-09-16").
finding_note(f_a_word_reserved_for_nothing_is_a_promise_the_tree_cannot_keep, "A WORD RESERVED FOR NOTHING IS A PROMISE THE TREE CANNOT KEEP, and the owner retired the promise rather than the refusal. `@async` had a branch of its own in `temporal()` answering `'@async' is reserved syntax, not in v0`, which START.md 3.3 asked for and which says one thing beyond the refusal: THE WORD IS BEING HELD. The effects executor is not going to be built, so it was being held for nothing, and the branch is gone -- `@async` is now refused by the single arm that refuses every unknown marker, and the temporal set is exactly the three the section 1.1 grammar always listed. THE PARSER NOW AGREES WITH THE GRAMMAR IT WAS WRITTEN FROM: the reservation was never in the production, only in the prose. START.md WAS NOT EDITED, and that is the tree's own idiom rather than a choice made here: section 8 was retired item by item by LIMITS.md through `amends[map]` and not by deletion, so the document still says what it said and the model says what is owed today. Two sentences went superseded -- `s_async_reserved_rejected` (3.3) and `s7_no_pretend_async` (7) -- both amended by `l_no_async`, which says the stronger thing: not reserved, not a marker, refused like any other unknown one. Measured: 132 duties, superseded 8 -> 10, live 124 -> 122, uncovered 102 -> 101, `guarded_by` unchanged at 17, and PROHIBITIONS WITH NO MECHANICAL CHECK STILL 0 -- the one number that could have been paid for by this and was not, because the world that guarded a prohibition now guards a limit and the two sentences it left behind are no longer live. THE CHECK SURVIVED THE FEATURE, and what let it is a decision made for a different reason: a golden over a refused world hashes `refused <basename>` and NOT the diagnostic (scripts/goldens.ts, `The MESSAGE is not hashed`), because two implementations word a syntax error differently and always will. So deleting the branch moved no hash at all -- the world was re-blessed only because the FILE WAS RENAMED, async-reserved.rofl to async-refused.rofl, and the basename is in the diag. THE SAME DECISION IS THE CHECK'S BLIND SPOT AND IT IS THE RIGHT ONE HERE: the golden cannot tell `refused as reserved syntax` from `refused as an unknown marker`, and `No @async` does not ask it to -- a limit needs the no, not the wording of the no. A CHECK THAT OUTLIVES ITS DUTY MUST BE RE-POINTED OR IT DANGLES: `c_w_async_reserved` guarded `s_async_reserved_rejected`, and a superseded duty keeps its guard link while dropping out of `live_duty`, so the citation would have gone on resolving while standing behind a sentence nobody owed -- a green row describing nothing, which is the failure mode this model was built to catch one level up (`dangling`). It is cited at `l_no_async` now, which is the sentence that is actually owed, and that took the LIMITS.md bullet from uncovered to covered. THE SECOND ENGINE NEVER HAD THE BRANCH. rust/rofl/src/rofl_parse.rs reads a tense only when the word is init, now or next, and on anything else it leaves the `@` unconsumed and the clause fails a token later -- so the two engines have refused this file for two different reasons for as long as it has existed, and the golden agreed with both because it hashes neither reason. Read, not run: the release binary is not built in this container, and the agreement is the standing evidence of CI rather than a measurement made today.").
addressed_by(f_a_word_reserved_for_nothing_is_a_promise_the_tree_cannot_keep, "src/parser.ts").
addressed_by(f_a_word_reserved_for_nothing_is_a_promise_the_tree_cannot_keep, "facts/spec.rofl").
addressed_by(f_a_word_reserved_for_nothing_is_a_promise_the_tree_cannot_keep, "examples/checks/async-refused.rofl").
Loading
Loading