Repository navigation
W0 hygiene: K9 gate fix, proof gate that can fail, repo deed, ABI/FFI seam aligned - #74
Conversation
…gfood Gate can pass
validate-k9.sh rejected .machine_readable/self-validating/methodology-guard.k9.ncl
for a missing `K9!` magic line and pedigree block; that is why the Dogfood
Gate workflow has been red on main. This ports rsr-template-repo's current
methodology-guard (which reads the ROADMAP journal and the repo deed's
bot-directives clause) with the identity placeholders filled in, and fills
the one author placeholder in template-kennel.k9.ncl.
Verified: `bash .github/hooks/validate-k9.sh` 10 files, 0 errors (was 2).
The two remaining `{{` in methodology-guard are the guard's own reject
patterns, deliberately split with a Nickel concat so repo-init cannot eat
them.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J4QvDfmD7HiQBt2GX3aYUv
…late's MANIFEST-driven check
build/just/proofs.just did `command -v idris2 || { echo SKIP; exit 0; }` for
every prover, so `just proof-check-all` reported green on any machine that
could not check a proof, and scanned raw lines for believe_me so it fired on
its own comments. Ported verbatim from rsr-template-repo:
- scripts/check-proofs.sh: a missing toolchain is FATAL; every module is
checked from its own source root per verification/proofs/<prover>/MANIFEST;
a proof file absent from the MANIFEST is an error; idris2 --check's exit 0
on a missing import is caught by grepping for `Error:`.
- scripts/scan-dangerous.sh: strips comments before matching.
- build/just/proofs.just: delegates to both.
- verification/proofs/lean4/lean-toolchain: the template's pin.
The four MANIFESTs list every module as `gated` and say in their header that
nothing was ground-truthed here (no prover on PATH): the first CI run with a
toolchain decides, and a FAIL there is the gate working.
Watched: scan-dangerous PASS clean, FAIL on a planted believe_me;
check-proofs idris2 exits 1 with the fatal no-toolchain message.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J4QvDfmD7HiQBt2GX3aYUv
… specs One deed per repo (standards#837, D312), written by hand from the frozen .machine_readable/ A2ML sources under 1-formats/deed/mappings/, one clause per mapped family; no converter (D313). Lints OK with deed_lint.js (deed.abnf v1.2.1). scripts/deed-field.sh is ported verbatim from rsr-template-repo so every gate reads the deed the same way; the deed is added to the root allowlist so the root-shape gate still passes (38 entries → 39). Values that are not verbatim translations are commented in place: - :repo-uuid is the derived #u5 name, not CLADE.a2ml's v4 hex (mapping P-1). - (lineage :born "2026-06-21") from the GitHub API; CLADE.a2ml's 2026-03-16 is the template's own born date carried over at mint. - (ecosystem …) is written from STATE/README/Intentfile because the A2ML ECOSYSTEM still describes rsr-template-repo itself. - (anchor …) drops (semantic-authority-files …): all four files it named are absent from the tree. - (clade :secondary (gv)) is verbatim and flagged: the template dropped its own inherited gv and noted it had propagated into minted repos. - (rsr-profile …) declares only capabilities with code in the tree and records why the rest are omitted. Not carried (no mapping spec; the worked model's versions are template canon): ply, ensaid, integrations, policies, egress. STATE's journal lives in docs/status/ROADMAP.adoc (state-v1-decision option B). The A2ML files stay in place, frozen; deleting them is a separate reviewable step. Verified: deed_lint OK; deed-field.sh reads canonical-name, status phase, maturity level, lineage born, agentic/integrity allow-silent-skip (false), bot-directives/coverage/metadata last-updated, and derives the uuid; validate-a2ml.sh scans the deed without error; check-root-shape.sh PASS. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDfmD7HiQBt2GX3aYUv
… FFI actually exports The template seam bound rsr_init/rsr_free/rsr_process/rsr_get_error in librsr, which nothing in this repository builds; src/interface/ffi exports recon_silly_ation_* from librecon_silly_ation. The Idris2 Result had four constructors (with Busy) against the Zig enum's five; the Idris2 `process` wrapper treated 0 as failure while the Zig side returns 0 for ok. Each side was internally consistent, so no per-side check could see it (ultraplan corpus row 3). - Abi/Types.idr: Result = Ok | Error | InvalidParam | OutOfMemory | NullPointer in the Zig enum's order; resultCode/fromCode carry the c_int table; fromCodeResultCode proves the table round-trips; DecEq's 25 clauses are generated, not typed. - Abi/Foreign.idr: six %foreign bindings to recon_silly_ation_* in librecon_silly_ation; `process` decodes the code and returns Either Result (); last_error takes no handle, as in Zig. - tests/aspect_tests.sh Aspect 3: a real ABI/FFI contract check — every symbol the ABI binds must be exported by the FFI, and the bound library must be what build.zig names. Watched to FAIL on the old seam (4 unbound symbols, librsr vs librecon_silly_ation), PASS after. NOT compiled: no idris2 on PATH in this session and none in CI. The symbol and library agreement is verified by the aspect test; the Idris2 itself awaits a toolchain (W3 E3). The ultraplan corpus gains row 12: CLADE.a2ml's born date is the template's own, found while authoring the deed. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDfmD7HiQBt2GX3aYUv
|
Caution Review failedThe pull request is closed. 📝 Summary
Merge Risk:
 |
|
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 01c802f91a
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| } else if (bo != "" && substr(line,i,length(bo)) == bo) { | ||
| inblk = 1; i += length(bo) | ||
| } else if (lc != "" && substr(line,i,length(lc)) == lc) { | ||
| break # rest of the line is a line-comment |
There was a problem hiding this comment.
In the new proof-scan gate, comment delimiters are recognized without tracking quoted strings, so a valid string containing -- (or {-/(*) causes the remainder of the line or file to be discarded. For example, a Lean/Idris/Agda line containing "--" before sorry or believe_me passes this scanner even though those proof escapes compile successfully; the analogous Perl stripping in tests/aspect_tests.sh has the same bypass. Make the stripping string-aware so these gates cannot report an unsound proof as clean.
Useful? React with 👍 / 👎.
| if [ "$status" = gated ]; then | ||
| echo "FAIL" | ||
| printf '%s\n' "${LAST_OUT//$'\n'/$'\n '}" | sed '1s/^/ /' | ||
| fails=$((fails + 1)) | ||
| else | ||
| echo "fail (quarantined, expected)" |
There was a problem hiding this comment.
When a MANIFEST status is misspelled, empty, or has trailing whitespace, every value other than the exact string gated is treated as quarantine. A failing proof with such an entry is therefore reported as an expected failure and can leave the overall gate green, silently defeating the checker’s central guarantee. Validate and normalize the status field, accepting only gated or quarantine and failing on anything else.
Useful? React with 👍 / 👎.
| ABI_SYMS=$(grep -ho '%foreign "C:[A-Za-z0-9_]*,' "$ABI_DIR"/*.idr 2>/dev/null | sed -e 's/.*C://' -e 's/,$//' | sort -u) | ||
| ABI_LIBS=$(grep -ho '%foreign "C:[A-Za-z0-9_]*,[A-Za-z0-9_]*"' "$ABI_DIR"/*.idr 2>/dev/null | sed -e 's/.*,//' -e 's/"$//' | sort -u) | ||
| # Every symbol the Zig FFI exports, and the library name build.zig gives it. | ||
| FFI_SYMS=$(grep -ho 'export fn [A-Za-z0-9_]*' "$FFI_SRC"/*.zig 2>/dev/null | awk '{print $3}' | sort -u) |
There was a problem hiding this comment.
The new contract test greps raw source text, so commented-out declarations still count as live exports and bindings. For example, changing a Zig definition to // export fn recon_silly_ation_process... leaves it in FFI_SYMS, allowing Aspect 3 to pass even though the library no longer exports the symbol and consumers will fail to link; a commented Idris %foreign line is handled the same way. Strip comments or inspect parsed/compiler-produced symbol information before comparing the two sides.
Useful? React with 👍 / 👎.
| ||| Raw FFI call for main processing. The Zig side returns `Result` as a | ||
| ||| c_int code (0 = ok), not a value: see Abi.Types.resultCode. | ||
| %foreign "C:recon_silly_ation_process,librecon_silly_ation" | ||
| prim__process : Bits64 -> Bits32 -> PrimIO Int |
There was a problem hiding this comment.
This change replaces the rsr_*/librsr bindings and expands the Idris Result to the same five cases as Zig, but docs/status/ROADMAP.adoc:28-29 still presents those exact mismatches as the current state and leaves the task unchecked. Because the new deed designates that roadmap as the state journal, landing the code as written immediately makes the repository’s authoritative status record false; update the M1 entry alongside the seam.
Useful? React with 👍 / 👎.
| else | ||
| pass "ABI/FFI not applicable (no $ABI_DIR or $FFI_SRC)" |
There was a problem hiding this comment.
Aspect 3 reports the contract as passing whenever either directory is absent, because the else branch treats a partially present seam as “not applicable.” If the Zig implementation is deleted or renamed while the Idris bindings remain (or vice versa), this gate goes green even though the surviving side still declares an ABI that cannot be satisfied. Treat the seam as inapplicable only when both sides are absent, and fail when exactly one exists.
Useful? React with 👍 / 👎.
| e = close_of(o) | ||
| if (!e) exit 2 | ||
| if (mode == "has") exit 0 | ||
| if (mode == "clause") { for (t = o; t <= e; t++) print tok[t]; exit 0 } |
There was a problem hiding this comment.
The reader decodes \n escapes inside strings and then --clause prints each raw token on its own line, so distinct clauses can produce identical byte streams for hashing. For example, the token output for :x "a\nA:y\nSb" collides with the output for :x "a" :y "b"; any integrity check using the advertised hashing mode therefore cannot distinguish those deeds. Escape embedded control characters or length-prefix each token before emitting the canonical stream.
Useful? React with 👍 / 👎.
…art; add session handover (#75) ## Summary Seven workflows were red on `main` (`95f8b33`), all from before the 2026-10-27 session. Five never started: GitHub rejected them with zero jobs because this repository runs the actions lockfile and they called `hyperpolymath/standards` reusable workflows the lock cannot cover. This re-adopts rsr-template-repo's current inline, SHA-pinned versions, fixes the Well-Known check that looked in the wrong directory, rebuilds `actions.lock`, and adds the session handover so nothing from the session lives only in chat. ## Changes - **governance, hypatia-scan, mirror, secret-scanner, static-analysis-gate, scorecard, release** — verbatim from rsr-template-repo, which replaced every cross-repo reusable call with inline jobs. `release.yml` now uses `actions/attest-build-provenance` in place of the SLSA generator's reusable workflow (same startup-failure class; it only runs on tags). - **`wellknown-enforcement.yml` → `dot-wellknown-enforcement.yml`** — the old one checked `.well-known/security.txt` at the root after #56 moved it to `www/.well-known/`. The template's replacement checks `www/.well-known/` first; `scripts/migrate-wellknown-to-www.sh`, which it names, is included. - **`.github/workflows/actions.lock`** — rebuilt, both the `workflows:` and `dependencies:` sections: entries for the replaced files from the template's generated lock (byte-identical files), the rest kept; dependency records for exactly the refs now used plus their transitive `uses`. Two lines of Dependabot drift corrected (`smtp-notify-action` v0.3.0→v0.5.0, `upload-artifact` v7.0.1→v7.0.2). - **`www/.well-known/security.txt`** — `Policy:` pointed at `SECURITY.md`, which does not exist; now `SECURITY.adoc`. - **`docs/status/HANDOVER-2026-10-27.adoc`** — what landed in #73/#74/this PR, the owner's D-1..D-4 decisions, what is and is not true (no proof compiled, no reconciliation code), open items, where to start. Linked from `ROADMAP.adoc`. ## RSR Quality Checklist ### Required - [x] Tests pass — aspect 5/5, root shape, K9 0 errors, `validate_workflows_test.sh` PASS - [x] Code is formatted — workflows and lock parse with `yq` - [x] Linter is clean — see lock verification below - [x] No banned language patterns - [x] No `unsafe` blocks - [x] No banned functions - [x] SPDX headers present on all new/modified files - [x] No secrets — no workflow added or changed reads a secret ### As Applicable - [ ] `STATE.a2ml` — frozen; state lives in the deed and `ROADMAP.adoc` - [x] Documentation updated (handover, roadmap link) - [ ] CHANGELOG — not updated (no release) - [ ] ABI/FFI — not touched ## Testing ``` # every uses: in every workflow is locked under that workflow, and every lock line is used exact match both ways # every SHA-keyed dependency record's commit equals its key ok (9 of 9) yq '.' on all workflows and actions.lock # all parse grep for cross-repo reusable workflow calls # none bash tests/aspect_tests.sh # PASS=5 FAIL=0 WARN=1 bash .github/hooks/validate-k9.sh # 0 errors bash tests/workflows/validate_workflows_test.sh # PASSED security.txt: 65 days to expiry; security.txt, ai.txt, humans.txt all in www/.well-known/ ``` Not verified locally: `gh actions-lock --verify-local` (gh is not authenticated in this session). The Workflow Security Linter runs it on this PR and is the authority on the lock. --- _Generated by [Claude Code](https://claude.ai/code/session_01J4QvDfmD7HiQBt2GX3aYUv)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com> Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com>
Summary
Wave 0 of
docs/proposals/ULTRAPLAN-2026-10-27.adoc(merged in #73), as the owner chose via the selector on 2026-10-27: hand-authored repo deed, the proof gate that can fail, the K9 fix that unblocks the Dogfood Gate, and the ABI/FFI seam aligned under a real contract check. #73 merged before these four commits were pushed, so they are rebased ontomainhere as a fresh PR.Four commits, each independently reviewable and each with the gate it touches watched failing first. No reconciliation code.
Changes
.machine_readable/self-validating/methodology-guard.k9.ncl— ported from the template with identity filled; had noK9!line or pedigree, which is why the "Validate K9 contracts" check was red on W0: ADR 0002 (D152), ultraplan, repo deed, and four gates that could not fail #73 and onmain.validate-k9.sh: 2 errors → 0.scripts/check-proofs.sh,scripts/scan-dangerous.sh,build/just/proofs.just, fourMANIFESTs,lean-toolchain— verbatim template ports. A missing toolchain is fatal, not a skip. MANIFESTs list every modulegatedand say in their header that nothing was ground-truthed here.recon-silly-ation_chora.deed— hand-authored from the mapping specs (no converter, D313), lints OK withdeed_lint.js. Non-verbatim values commented in place: derived uuid;:born "2026-06-21"from the GitHub API (CLADE.a2ml carries the template's date); ecosystem written fresh (the A2ML one still describes the template); anchor drops four dangling file references;:secondary (gv)verbatim and flagged; rsr-profile declares only capabilities with code in tree.scripts/deed-field.shported; deed added toroot-allow.txt. A2ML files left in place, frozen.src/interface/Abi/{Types,Foreign}.idr— bound torecon_silly_ation_*inlibrecon_silly_ation(wasrsr_*inlibrsr, which nothing builds);Resultnow five cases in the Zig enum's order with a round-trip lemma;processno longer treats 0 as failure. Aspect 3 intests/aspect_tests.shis now a real ABI/FFI contract check: FAIL on the old seam (4 unbound symbols, wrong lib), PASS after. The ultraplan gains corpus row 12 (CLADE born date).RSR Quality Checklist
Required
just test(zig build test) not run: no Zig here; no Zig file changed.bash -nclean; deed linted)unsafescan-dangerous.shand Aspect 2 both watched catching a plantedbelieve_me/AdmittedAs Applicable
STATE.a2ml— frozen (never add a fact to A2ML); state now lives in the deed andROADMAP.adoc01c802f) can be dropped on its own; the contract check in it would then fail onmain, which is the honest state.Testing
Not verified: Idris2, Zig, Agda, Lean, Rocq (none installed). CI has no prover either; wiring one is W3 E3.
Generated by Claude Code