Skip to content
Merged
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
2 changes: 1 addition & 1 deletion .pmat/baseline.json
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
{
"version": "3.41.1",
"created_at": "2026-09-20T17:31:37.910110581Z",
"created_at": "2026-09-20T20:19:32.784452565Z",
"git_context": null,
"files": {
"./build.rs": {
Expand Down
84 changes: 84 additions & 0 deletions docs/audits/quorum-RHL-14.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,84 @@
{
"ticket": "RHL-14",
"pr": 230,
"base": "main",
"head": "9f40a2111d49d1aae8ff9c9e4de34adf43d23f41",
"diff_sha256": "e2a9a40cb058b903ef1e38d2db9c81cb22a18fabb64b6f35eb49b0a12b9c3ee4",
"agreed": true,
"verdict": "implement-as-written (2/2), plus one header line added after review",
"author": {
"session": "ruchy-9d",
"model": "claude-opus-5[1m]"
},
"families_required": [
"gemini",
"claude"
],
"families_run": [
"gemini"
],
"families_note": "Docs-only spec amendment. Both review lanes gemini (3.1-pro-high, 3.8-flash-high), both measured (command+output on 6/7 and 5/7 findings), tree witness verified, 0 BLIND. The DECISION itself was a separate 3-lane gemini quorum (dabbe241, 51ff083b, 679e5b1c) recorded in the spec's O1 block; the author is claude-family and took the minimal reading of a 2:1 split, which is recorded there as a residual, not hidden.",
"decision_quorum": {
"width": 3,
"lanes": [
{
"lane": 1,
"model_measured": "gemini-3.1-pro-high",
"conversation": "dabbe241-e44f-4516-bc87-aa7d275d8aeb",
"verdict": "split: <App> to <App> production for `to`; reword per/are"
},
{
"lane": 2,
"model_measured": "gemini-3.8-flash-high",
"conversation": "51ff083b-4470-4ef7-8ac5-4e366b5b7af9",
"verdict": "O1-R for all three; refutes O1-A's `of` claim"
},
{
"lane": 3,
"model_measured": "gemini-3.7-flash-high",
"conversation": "679e5b1c-5d2a-40ac-8f43-b7ddab8b2c00",
"verdict": "split, same as lane 1"
}
],
"consensus": "3/3 refuse O1-A as written; 3/3 measured zero vocabulary terms and zero docs/rhl/ programs use per/are or the three shapes; 2/1 on adding <App> to <App>; author took the minimal ruling (no grammar change) and recorded the split as a residual."
},
"review_quorum": {
"judged": "81e1ea0dc1800025fba91a92c6f5e54a74c8c7a3",
"width": 2,
"lanes": [
{
"lane": 1,
"model_measured": "gemini-3.1-pro-high",
"conversation": "92532bd8-8e69-491b-b7fb-97de581a5859",
"verdict": "implement-as-written",
"kept_clone": "wrote diff.txt/log.txt/old_spec.md/output_log.txt into its writes=false clone; shared checkout byte-identical; clone removed by the author"
},
{
"lane": 2,
"model_measured": "gemini-3.8-flash-high",
"conversation": "fde2b85e-cec5-45e5-bd4e-8efddb2a316d",
"verdict": "implement-as-written"
}
],
"measured": [
"spec sha256 matches the new manifest line; all 301 manifest hashes match the tree",
"per/are only in comment lines of both vocabularies (fleet 12,27; tickets 10,23)",
"rg 'no change to|per run|are filed' docs/rhl/ \u2192 nothing",
"match block: of=False in=True to=True",
"roadmap.yaml parses; RHL-1 notes 'NOT READY' gone"
],
"gaps_closed_by_author": [
"rg -n O1 sweep for stale 'awaiting operator' text: only grammar/fixtures/o1-a-candidate.lalrpop:4 (candidate evidence, manifest-hashed, left as both lanes allowed) and the RHL-0 receipt (historical)",
"the O1 header now says RULED so a reader landing there does not stop \u2014 one line, ed39f21e, manifest regenerated, 37 gates green"
],
"not_measured": [
"`expect host is unchanged` and `then ticket count is 0` have no corpus twin; their parse is a grammar read by both lanes, not a generated-parser run. RHL-1 builds the parser that measures it."
]
},
"rebind_note": "Reviewed at 81e1ea0d; head moved by one docs commit (the O1 header line + its manifest hash) after the review. Recorded rather than re-reviewed: one sentence, no claim in it the lanes did not already check.",
"residuals": [
"grammar/fixtures/o1-a-candidate.lalrpop:4 still reads 'Awaiting an operator ruling'",
"the 2:1 on <App> \"to\" <App> stays open for a corpus task that needs it"
],
"rebind_note_2": "Rebased onto main after #229 merged (both PRs appended roadmap rows; the conflict was two append hunks, resolved by keeping both sides \u2014 204 rows, ids unique, checked with a real YAML parser). The judged diff's content is unchanged except the roadmap hunk's position; head is the bind commit's parent 9f40a211 (the artifact commit adds only itself), the rhl_pre_registration gates re-run green after the rebase."
}
2 changes: 1 addition & 1 deletion docs/rhl/PREREGISTRATION.sha256
Original file line number Diff line number Diff line change
Expand Up @@ -304,7 +304,7 @@ f8b3f91447b4b64a09d69c71d87a7bdcecf5a37d1f9e08e1c6cc4314b61350bd docs/rhl/corpu
1772856a1c12f1a0a5b1fb3c7abf664bd7edafd2fe0318a737d0bda0fff7dfe9 docs/rhl/corpus/40-disk-cleanup-unstated-unit/tests.rs
6d0fd9fb92ad60ede614398d2051d31ca89c12d9d846f45384979e9bd3097a8e docs/rhl/corpus/HARNESS.md
a270e5ec4706ac2f66bdb0e3d5632f4cfc31056bcf6afc8571d3d7709fefc0f8 docs/rhl/phase0-bindings.md
64b5e95e5aa6f54dbd7102c7ca243c73ff4c332bea97115435b057cc36761038 docs/specifications/ruchy-high-level-language-interface.md
a45f5b4a37b4b7eaab39a17c1770ebb4b36ca4989cdfbdfd34591fddb38bcc35 docs/specifications/ruchy-high-level-language-interface.md
0447678137b6c7efc06628f010e42f2e2ff6e22cde38e7d573a570bc7939dd77 grammar/fixtures/ambiguous.lalrpop
3eac9148c0f4c28ff8d42259e23726d6f04dc1b7e95146fbe86468e6a5c8385c grammar/fixtures/o1-a-candidate.lalrpop
45f9dd4d63d64bbb6135b0113d8854545439ae7b2d3d54eaa893838f5a636088 grammar/fixtures/o1-b-candidate.lalrpop
Expand Down
15 changes: 14 additions & 1 deletion docs/roadmaps/roadmap.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -2916,7 +2916,7 @@ roadmap:
- kind:code
- rhl
- depends:RHL-0
notes: 'ADMITTED by RHL-0''s merge (commit 1c2caf5d, PR #225) — the spec''s readiness gate ''no implementation rows are admitted until RHL-0 is merged'' has opened. BUT NOT READY TO START: spec open question O1 is unruled. Three lines of section 3.2 do not parse (expect no change to host / expect at most 1 ticket per run / then 0 tickets are filed), and RHL-1 is the row that builds the parser those lines have to pass through. Both candidate repairs are measured and committed as grammar/fixtures/o1-{a,b}-candidate.lalrpop: O1-A is conflict-free, parses all three lines and keeps the corpus at 72/72, and costs two keywords; O1-B adds no keyword and is NOT conflict-free. Get the one-line ruling before starting. K-hat basis is 118 [C] from RHL-0 (see HARNESS-1 on the unit question). RHL-1 also inherits F1''s unmeasured second half: ''every corpus program has exactly one parse'' needs the parser this row builds.'
notes: 'ADMITTED by RHL-0''s merge (commit 1c2caf5d, PR #225) — the spec''s readiness gate ''no implementation rows are admitted until RHL-0 is merged'' has opened. O1 RULED 2026-09-20 by quorum (RHL-14, ruling O1-R): the three section-3.2 lines were reworded to the shapes the corpus already used, no keyword reserved, no grammar change; the 2:1 residual on an App-to-App production is recorded in the spec''s O1 block. READY TO START once RHL-14 merges. K-hat basis is 118 [C] from RHL-0 (see HARNESS-1 on the unit question). RHL-1 also inherits F1''s unmeasured second half: ''every corpus program has exactly one parse'' needs the parser this row builds.'
- id: RHL-2
github_issue: null
item_type: task
Expand Down Expand Up @@ -3388,6 +3388,18 @@ roadmap:
spec: null
acceptance_criteria:
- 'Five-class audit pass, 2026-09-20. CLASS 3 (gate-that-cannot-fail). src/quality/mod.rs:860, in test_satd_count_collection: ''let count = QualityGates::count_satd_comments().unwrap_or(0);'' followed by ''assert_eq!(count, 0, "SATD comments should be eliminated")''. count_satd_comments returns Result and shells out to ''find src -name *.rs -exec grep -c ...''. If that invocation fails for ANY reason — find missing, src/ absent, a packaged crate without src/, a sandbox without exec — the error becomes 0 and the assertion PASSES. The test cannot distinguish ''there is no SATD'' from ''the counter did not run'', and 0 is the most permissive of the two answers. GROUNDED BY INSPECTION, not executed: making the counter fail under test needs an environment change. NOTE the production gate is NOT affected — line 300 uses ''?'' and propagates. This is the test only. FALSIFIER: replace unwrap_or(0) with expect(), or assert on Ok(0) rather than on the unwrapped value, then rename the binary/PATH so find is unavailable; the test must go RED where today it goes green.'
- id: RHL-14
github_issue: null
item_type: task
title: 'RHL-14: O1 ruled by quorum — reword the three §3.2 lines, reserve no keyword'
status: planned
priority: medium
assigned_to: null
created: 2026-09-20T18:55:16Z
updated: 2026-09-20T18:55:16Z
spec: null
acceptance_criteria:
- Open question O1 (spec RHL-001, under §3.3) ruled by a 3-lane decision quorum on 2026-09-20, per the operator's standing instruction that decisions go to a quorum. 3/3 refuse O1-A as written (reserving per and are forecloses rate and descriptive terms — errors per hour, hosts that are pinned — and all 12 valid corpus programs already use the reworded shapes, so R costs 0 corpus diffs). 2/3 would additionally add App to App under Cmp for the to line; 1/3 calls that an ad-hoc preposition with no vocabulary term behind it. The minimal ruling is taken — reword all three, change no grammar — and the 2:1 on the to production is recorded as a residual. Lane 2 also found a factual error in the O1 text — it says reserving per/are is the same trade already made for of, and of is NOT reserved (grammar/rhl.lalrpop clause 2). Spec is manifest-hashed; PREREGISTRATION.sha256 regenerated in the same commit.
phases: []
subtasks: []
estimated_effort: null
Expand Down Expand Up @@ -3433,4 +3445,5 @@ roadmap:
labels:
- kind:code
- class:gate-cannot-fail
- kind:docs
notes: null
42 changes: 36 additions & 6 deletions docs/specifications/ruchy-high-level-language-interface.md
Original file line number Diff line number Diff line change
Expand Up @@ -110,17 +110,17 @@ job "gx10 disk watch"
end
end

expect no change to host
expect at most 1 ticket per run
expect host is unchanged
expect ticket count is at most 1

example "low disk files one ticket"
given disk free of "/" is 90 GB
then 1 ticket is filed
then ticket count is 1
end

example "healthy disk files nothing"
given disk free of "/" is 400 GB
then 0 tickets are filed
then ticket count is 0
end
end
```
Expand Down Expand Up @@ -161,7 +161,7 @@ Everything else in a program is a **vocabulary term**, a **literal**, or a **nam
> because an action's attributes reading as siblings of the statements around
> them loses the nesting §3.2 uses to say which attributes belong to which
> action. But "the only one" was not measured and was not true.
> **Open question O1 — three lines of §3.2 do not parse (RHL-0, 2026-09-20) `[V]`.**
> **Open question O1 — three lines of §3.2 do not parse (RHL-0, 2026-09-20) `[V]`. RULED: see O1-R at the end of this block (RHL-14).**
> A parser was generated from `grammar/rhl.lalrpop` and fed §3.2 verbatim. After
> Amendment A1 these three lines still fail:
>
Expand Down Expand Up @@ -192,7 +192,10 @@ Everything else in a program is a **vocabulary term**, a **literal**, or a **nam
> | the 72 non-`missing-end` corpus programs | **72/72, 0 failures** |
>
> Cost: §3.3 grows by two keywords, and `per` and `are` become unusable inside any
> vocabulary term — the same trade §3.3 already makes for `of`, `in` and `to`. It
> vocabulary term — the same trade §3.3 already makes for `in` and `to`. (This
> line first said "for `of`, `in` and `to`". `of` is NOT reserved: grammar clause 2
> keeps it free precisely so `disk free of` stays spellable. Found by the O1
> quorum, lane 2.) It
> costs §3.1 principle 8 (block-closed, count the `end`s) **nothing**: no
> production here touches block structure.
>
Expand All @@ -212,6 +215,33 @@ Everything else in a program is a **vocabulary term**, a **literal**, or a **nam
> **The ruling wanted, in one line:** adopt O1-A and add `per` and `are` to §3.3,
> or reword these three lines of §3.2 so the language does not need them. O1-B is
> not available — it is not conflict-free.
>>
> **Ruling O1-R (RHL-14, 2026-09-20) `[V]` — reword; reserve nothing; change no
> grammar.** Ruled by a three-lane decision quorum (gemini 3.1-pro / 3.7-flash /
> 3.8-flash, conversations `dabbe241…`, `51ff083b…`, `679e5b1c…`), under the
> operator's standing instruction that design decisions go to a quorum. The three
> lines of §3.2 now read `expect host is unchanged`, `expect ticket count is at
> most 1`, `then ticket count is 1` / `is 0` — the shapes the 12 valid corpus
> programs (`docs/rhl/breaks/valid/`) already used, so the corpus diff is zero and
> the grammar is untouched. Each parses under the pre-registered grammar as
> `"expect"|"then" <Cond>` → `Cmp` → `<App> <CompOp> <App>`.
>
> Measured by all three lanes: no term in `vocab/fleet-v1.yaml` or
> `vocab/tickets-v1.yaml` contains `per` or `are` (the words occur only in
> comments), and no program under `docs/rhl/` uses `no change to`, `per run` or
> `are filed`. Why 3/3 refused O1-A: reserving `per` and `are` forecloses every
> future rate or descriptive term — `errors per hour`, `hosts that are pinned` —
> for three lines of an example, and the A1 precedent cuts the other way: A1 added
> a keyword to keep a *structure* (the nested block); nothing structural is at
> stake here. Principle 9 wins over "reads like English" when the English costs
> the vocabulary a word.
>
> *Residual, 2:1.* Lanes 1 and 3 would also have admitted `<App> "to" <App>` under
> `Cmp` (one production, zero keywords, `to` is already reserved) so that `expect
> no change to host` parses. Lane 2 called that an ad-hoc preposition with no
> vocabulary term behind it — there is no term `no change` — and the minimal
> ruling was taken. A corpus task that needs `X to Y` as a comparison re-opens it;
> `grammar/fixtures/o1-a-candidate.lalrpop` keeps the measured production.
>
> The unmarked form is kept verbatim as `grammar/fixtures/ambiguous.lalrpop`,
> where it serves as F1's positive control. Evidence:
Expand Down
Loading