Repository navigation
Follow-up to #107: review fixes and governance hardening - #108
Open
hyperpolymath wants to merge 58 commits into
Open
hyperpolymath wants to merge 58 commits into
hyperpolymath wants to merge 58 commits into
Conversation
… on the ratified carrier spec/calculus.adoc was a v0.1 document (revnumber 0.1, 2026-06-22) with the 2026-07-07 ratification spliced in as notes, a separate never-merged v0.2 addendum (spec/calculus-v0.2-draft.adoc, 2026-06-23), and two design notes carrying the operational model and the L4 analysis. It still said "seven effects" while the vocabulary, EffectAtoms.lean and the IR say nine. A reader — or an agent — following the spec alone got the pre-ratification world. This folds the four into one v0.2 spec. What changed, section by section: - §1: the object is stated as "property-instances as particulars", which every instance ontology supplies (tropes, modes, moments, qualities, SDCs), rather than as a commitment to one-category trope theory; §2 names the two constructs (attenuate, detach/FloatingQuality) that need instances to be particulars and would not survive a change of ontology. - §3: the fate chain, bond fibring (HC-4) and merge are stated on the ratified carrier with A1–A3 inline; new §3.5 gives the nine-effect / nine-atom-family table (EffectAtoms.lean) and the two structure theorems, so "seven" and "nine" are reconciled: nine families, six writable, three faults. - §4: L3 and L5 cover all three deceptive bottoms (two-sided zeros, A1); L4 is stated as holding in full with the Idris2/Lean/Agda lemma names; L6 (commutativity) is new; the addendum's R-2026-06-23-02..04 become the cancellation structure C1–C3 with the ratified lemma names; the tropical factorisation re-run is recorded as (B′) sighted, with the pre-ratification (B) result kept as history. - §5 T-Fuse: ⊔ is written ⊓ — the retention-order meet, "no better than its worse constituent" — matching the CO-1 note. Same meaning, one symbol. - §6: the prevent/detect decision now names all three deceptive duals. - §7: restated as greatest post-fixed point in the retention order with the decidable T-Fix-Decl rule, from the CO-1 note; the operational model is marked DESIGNED and its mechanisation OPEN. - §8: each soundness result carries its status (exact lowering and β/let PROVED; conservative lowering and fix OPEN); the third firewall now cites a defined O5. - §9.3: prover roles per the 2026-10-12 kernel ruling (Agda kernel, Idris2 executable reference, Lean provenance, Rust fast core) — see ADR 0005. - §10: O1 split into O1-carrier (PROVED) and O1-coord (OPEN, with the bond-transfer probe recorded as the live falsifier); O4 RESOLVED (ADR 0004); O5 DEFINED (adopted from the workbench proposal of 2026-07-17); O6 (ceiling verdict) newly opened; CO-1 listed with its DESIGNED/OPEN split. Every lemma name cited in the spec was checked against the source files on this branch (Idris2 Trope.*, Agda TB.*, Lean grade-boundary/* and grade-factorisation/*). No normative rule changes semantics; the IR stays 0.2. The README's repo map, firewall 3 and Status paragraph are brought into step; INTEGRATION-REPORT.adoc gets a header note marking it historical rather than being rewritten. CHANGELOG, ADR 0003 and PROOF-STATUS's dated history keep their references to the addendum as records of what was true when written.
…n source The `agda-theorem-b` job installed Agda from the runner's apt. ubuntu-latest is 24.04, whose agda-stdlib is 1.7.3, and Theorem B imports Data.Product.Base (stdlib >= 2.0): the job fails at scope checking (exit 42). Reproduced here 2026-10-13 with Agda 2.6.3 / stdlib 1.7.3, exactly the runner's pair. The workflow's own comment records a green run "under 2.6.4.3", which was a Debian machine, not the runner. Because the workflow is paths-filtered to verification/proofs/**, it has not run since the last proof change and the red was never seen. Fix: fetch the Agda 2.7.0.1 release binary and the agda-stdlib v2.0 archive, verify both SHA-256 sums, register the stdlib under the name theorem-b.agda-lib depends on (`standard-library`; the 2.0 archive calls itself `standard-library-2.0`), set Agda_datadir and a UTF-8 locale. Verified 2026-10-13 with exactly these artefacts and sums: All.agda and Smoke.agda typecheck under --safe --without-K, exit 0 (~100 s cold). The stdlib sum is of the GitHub-generated tag archive (no release asset exists); if GitHub ever regenerates it the checksum step fails loudly instead of testing something else. Also: `lean-source-honesty` and the mirroring `verify-all` recipe gated only the two v0.1 files (GradeBoundary, GradeFactorisation). The spec now cites GradeRatified, L4Monotonicity, TierTwoComplete, EffectAtoms and GradeFactorisationR, so both now iterate every tracked Lean source. All eight files pass the gate's regexes as they stand (run here). actionlint -shellcheck= on proofs.yml: clean. The job's real run is still needed: this sandbox has no Lean, so the lean-build matrix was not exercised.
What was wrong: PROOF-STATUS.adoc (revdate 2026-06-23) described the v0.1
carrier — a non-commutative ▷, a lax L4 that "fails on fate", CO-1 "gated by
O4", the OPEN-B/B′/C documentation gaps, "10/10" conformance — and listed as
open several results (O1 exhaustiveness, L4/L5 as lemmas) that are now proved.
A reader following it alone got the pre-ratification world.
What changed: one "Proved" table on the ratified carrier (Carrier & laws /
Cancellation / Factorisation / Metatheory / Soundness), citing only lemma names
that exist in the Idris2, Agda and Lean sources; one "Open" list matching
spec/calculus.adoc §10 (CO-1 mechanisation, O1-coord, O2, O3, O5 mechanisation,
O6) with where each is specified; the four modelling notes carried over; the
06-22 / 06-23 / 06-29 sections collapsed to one dated paragraph each under
"History", prefixed as superseded by R-2026-07-07 where they disagree.
What I ran: every cited identifier checked present by grep over
verification/proofs/{idris2/Trope,agda/theorem-b/TB,lean4} (38 + 43 + 44 names,
none missing); the acceptance grep for the stale phrases outside "== History"
returns nothing.
What I did not run: no prover in this commit (the AFFIRMATION commit carries
the runs).
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
What was wrong: ROADMAP listed v0.2 as "in progress" with the v0.1 vocabulary (CO-1 "gated by O4", the lax-L4 argument, OPEN-B/B′/C, a separate spec addendum) although the carrier was ratified on 2026-07-07 and the spec consolidated at v0.2. What changed: "Shipped (v0.2)" lists the ratified carrier (ADR 0004), the Agda carrier migration, L4 in full and L6, the atom factorisation (O1-carrier), TierTwoComplete, the sighted factorisation re-run and the spec consolidation; "Open problems" defers to spec/calculus.adoc §10 by reference and names CO-1 mechanisation as the next proof work; Deferred items kept. What I ran: grep for "gated by O4|lax|OPEN-B|OPEN-C" over the file — no hits. What I did not run: nothing else; documentation-only. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
What was wrong: the newest AFFIRMATION entry (2026-06-29) described the v0.1 carrier and cited 10/10 conformance cases and 8 schema-invalid fixtures; the corpus has been 13 + 9 for months and the carrier was ratified on 2026-07-07. What changed: a dated entry with an anchor (branch, commit, UTC time, exact toolchain), one bullet per command, a short proved/open paragraph naming only identifiers that exist, and two findings; :revdate: bumped. What I ran (all in this session, on this branch): idris2 --typecheck verification/proofs/idris2/trope.ipkg -> exit 0 just trope-build && bash tests/conformance/run.sh -> 13 + 9, all pass just trope-rust -> 13 + 9, all pass just build-agda -> PASS (All + Smoke) apt agda 2.6.3 + agda-stdlib 1.7.3 on All.agda -> exit 42 (finding 1) lean-source-honesty regexes over 8 .lean files -> clean What I did not run: just build-lean (no lake / Mathlib reachable here) — written as NOT RUN with the command named; the proofs.yml lean-build job is the attestation and is cited in the PR. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
…n CO-1 alone What was wrong: the NOT-REACHED footer of TB/Reduction.agda listed two obstructions to fix-subject-reduction, the second being "a LIMIT CARRIER … the open O4 fork (Conat-vs-tag)". ADR 0004 resolved O4 on 2026-07-07 (the finitary carrier suffices; transfinitely deep fix is inexpressible), and the operational model has since been designed. What changed (comment only, no code): the footer now states one obstruction — the operational model — DESIGNED in spec/notes/2026-07-07-co1-operational-model.adoc (λ-trope, tagged values, T-Fix-Decl) with its mechanisation plan (that note's §6, steps 1–5, extending this module), records O4 as RESOLVED by ADR 0004, and keeps "NOT-REACHED, NO postulate" and the tier-stability remark. What I ran: just build-agda (agda --safe --without-K All.agda + Smoke.agda) with this edit in the tree -> PASS, exit 0. What I did not run: nothing else applies. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
What was wrong: verification/proofs carried TypeSafety.v (Coq), StateMachine.tla (TLA+) and Properties.agda — mint templates whose own text says "Replace with your project's …", never instantiated — and the trees, usage lines and recipes advertised a fourth and fifth prover the roles ruling does not assign here. What changed: git rm of the three files; their lines dropped from the verification/proofs/README.adoc and docs/status/PROOF-NEEDS.adoc trees and the `just proof-check-coq` usage line; proof-check-coq removed from proof-check-all and the Coq/TLA+ lines from proof-status (proof-scan-dangerous keeps its harmless -name '*.v'); the awk's historical false-positive note no longer names the removed file by path. The INTEGRATION-REPORT mention stays as history. What I ran: git grep -n "TypeSafety\|StateMachine\|Properties.agda" -> only INTEGRATION-REPORT.adoc; just proof-status -> runs (Idris2 14, Lean4 8, Agda 9 files); just proof-check-all -> runs and is red for pre-existing reasons unrelated to this change (per-file idris2/agda checks from the repo root cannot resolve module names; the ABI/Types Idris2 mint templates do not typecheck) — recorded in AFFIRMATION and as an issue; just proof-scan-dangerous -> PASS. What I did not run: coqc / tlc (not installed, and no longer referenced). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
…er roles (Proposed) What was wrong: the spec consolidation of 2026-10-13 adopted O5, opened O6, wrote the prover roles into §9.3 and cited "ADR 0005" for all of it, but no ADR 0005 existed; the carrier-as-parameter question had no recorded home. What changed: docs/decisions/0005-…adoc in the 0004 layout — Status (Proposed, owner to accept), Context, Decisions D1–D6 (D1 v0.2 normative; D2 O5 adopted from the workbench proposal of 2026-07-17 unchanged in substance; D3 O6 opened; D4 prover roles per the 2026-10-12 kernel ruling; D5 three provers, templates removed; D6 recorded-not-decided: fidelity carrier as a parameter, Phase 1A), Consequences, Rejected alternatives. What I ran: nothing to run; the referenced files and identifiers were checked present (workbench note path, spec §9.3/§10, the removed templates). What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
What was wrong: CHANGELOG [Unreleased] stopped at the IR 0.2 normalisation and the 2026-06 developments; the spec consolidation, the proofs.yml pin, the status rewrites, ADR 0005 and the template removal were unrecorded. What changed: the v0.2 consolidation line from the foot of spec/calculus.adoc; one line each for the status-surface rewrites (T1–T4), the proofs.yml pin, ADR 0005 (Added) and the template removal (Removed). docs/status/READINESS.adoc was grepped for the same stale phrases as PROOF-STATUS and has none, so it is untouched (it remains the unfilled CRG template, which is not false). What I ran: grep -nE "non-commutative|lax L4|L4 fails|OPEN-B|OPEN-C|gated by O4|10/10|8 schema" docs/status/READINESS.adoc -> no hits. What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
…I Lean run What was wrong: spec §9.3, PROOF-STATUS and verification/proofs/README said the Lean developments' axiom audits show "propext/Quot.sound only". The proofs.yml lean-build run on this branch (40472568287) prints the audit: Trope.nine_families (EffectAtoms.lean), FateA.Q_add_left_cancel and FateA.atten_cancel_on_normalForms (GradeRatified.lean) also depend on Classical.choice. GradeBoundary.lean's own footer had listed Classical.choice all along; the surfaces overclaimed. What changed: the three surfaces now say "no sorryAx, no user axiom; propext, Quot.sound and, in three theorems, Classical.choice"; the AFFIRMATION entry's Lean bullet cites the CI run (lake build succeeded for both packages; the job is red only in lean-action's optional nanoda step, which cannot compile its lean4export under the v4.16.0 toolchain, as on main — issue #104) and records this as finding (3). What I ran: read the job logs of run 40472568287 (both Lean jobs): "Build completed successfully", one axiom line per theorem, then "nanoda check failed". What I did not run: lake build locally (unchanged: no lake here). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
… ratified carrier What was wrong (review findings on #102): the Reduction.agda footer said "the gfp's fidelity lands in the absorbing tops {total, unknown}" for every fix; that holds for a body that attenuates and recurses without bound, not for F(γ) = γ (gfp Present) or a body that ignores its binder (finite gfp). PROOF-NEEDS.adoc rows DOM-1/2/6/7/8 still described a non-commutative ▷, CO-1 "gated by O4", a "lax L4", and "propext/Quot.sound only". What changed: the footer restricts the absorbing-top argument to unbounded attenuation and names the other cases the fix proof must cover (comment only); DOM-1 marks non-commutativity historical and points at GradeRatified.lean, DOM-2 drops "non-commutative", DOM-6 records CO-1 as DESIGNED (O4 resolved) with mechanisation OPEN, DOM-7 drops the lax-L4 framing, DOM-8 records the (B′) re-run; "propext/Quot.sound only" becomes "no user axiom". What I ran: just build-agda after the footer edit -> PASS (All.agda + Smoke.agda); grep -n "non-commutative\|gated by O4\|lax L4\|Quot.sound" docs/status/PROOF-NEEDS.adoc -> none. What I did not run: n/a. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
… theorem is on Review round 2 (Codex, CodeRabbit) on PR #102: - proofs.yml lean-source-honesty and the `verify-all` recipe strip comments with tests/lib/strip-proof-comments.awk and match the bare `sorry`/`admit` tokens, so `:= by` followed by an indented `sorry` on the next line fails the gate (the old line-anchored regex passed it; ApiTypes.lean is not built by either Lake package, so the gate was its only check). Tested: all eight tracked .lean files still PASS; synthetic multiline sorry/admit now FAIL; "sorry-free" prose in comments still PASSes. actionlint clean. - README / ROADMAP: "carry no axioms" -> "no `sorryAx` and no user axiom", the wording the axiom audit supports (propext, Quot.sound, Classical.choice x3). - PROOF-STATUS, README, AFFIRMATION: the atom factorisation (`EffectAtoms.lean`) imports GradeBoundary and is a theorem about the v0.1 `Grade`; no GradeR restatement exists. Recorded as Open (O1-carrier on GradeR) and as AFFIRMATION finding (4); the spec's §6/§10 wording is left for the owner. - PROOF-NEEDS DOM-3: symmetric cut holds on the ratified carrier (`cut-grade-comm`); the v0.1 refutation is historical. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01J4QvDh3p24SCUjyM9HHT31
…roof audit comments
…firmation gate; make the workflow linter real
Three standards reusable pins (scorecard, governance, hypatia) referenced
commits that no longer exist in hyperpolymath/standards, so those
workflows failed at startup with zero jobs - invisible in 'gh pr checks'.
secret-scanner/mirror shared the same zero-job failure via wrapper shape.
All five are re-pinned to a verified-existing commit with the calling-job
permissions each reusable specifies, and workflow-linter now re-resolves
every external uses: ref so a phantom pin cannot rot invisibly again.
estate-audit failed its Affirmation gate: a depth-1 checkout made the
gate grade the PR test-merge commit, and the action's vendored GitHub
web-flow key is the pre-2024 expired one, so a good GitHub signature
classified as E ('cannot be checked') and failed as 'bad or revoked'.
Fetch full history, trust GitHub's current web-flow key (vendored with
provenance under .github/affirmation-trusted/), pin all 26 cicd-suite
composite actions that floated @main, add the SPDX header and top-level
permissions the file lacked, and run every gate even when one fails
instead of masking up to 18 unrun gates behind the first red.
workflow-linter's SPDX step demanded the tag on line 1, which
gh actions-lock's own banner makes impossible for every workflow
including itself; it now accepts the tag anywhere in the leading
comment block (REUSE convention) and thereby catches real misses.
Its enforcement core is now pinned actionlint + shellcheck and pinned
zizmor (hash-verified), alongside persist-credentials: false on every
checkout and env-passed values instead of template expansion in run:
scripts (template-injection class), with the three deliberate
exceptions justified inline for zizmor.
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…working Lean gate suite
Agda Theorem B now typechecks under --safe --without-K
--cubical-compatible --exact-split --warning=error - in CI, in
theorem-b.agda-lib flags, in every module OPTIONS pragma, and in the
just recipes - not merely --safe --without-K on one command line.
The Lean nanoda configuration could never pass: lean-action's
run_nanoda.sh greps lakefile.toml for a [package] table these
multi-lib lakefiles do not have, so module detection failed before
nanoda ran (every Formal-proofs Lean run ever, on both packages).
It also cloned a floating debug branch at gate time and set
unpermitted_axiom_hard_error: false, so its sorryAx rejection was
advisory. Replaced with pinned, hard-failing equivalents: lake build
--wfail, leanchecker re-checking the compiled environment, and an
axiom-audit allowlist of exactly {propext, Classical.choice,
Quot.sound} over every module (non-vacuity asserted), both packages.
The source-level tripwire now also bans unsafe/extern/implemented_by
and sorryAx/ofReduceBool by token, comment-aware as before.
Curl fetches enforce HTTPS and redirects (--proto =https
--proto-redir =https --tlsv1.2 --fail) - the SonarCloud 'C' security
rating on #102's new code was these two lines.
just proof-check-{idris2,lean4,agda} no longer run per-file checks
from the repo root (red on main, per #102) or report SKIP as pass:
they run the package builds CI runs, fail when the toolchain is
absent, and fail on orphan proof files no package builds.
proof-check-coq is gone with the Coq it never checked. build-lean's
axiom audit re-elaborates every source and checks each #print axioms
receipt against the allowlist instead of grepping a silent warm build.
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
- trope-check: the shipped JSON Schema is meta-validated (draft 2020-12, strict mode), every positive fixture validated against it and every schema-invalid fixture rejected BY it - not jq well-formedness alone. The formally-typed ABI seam (abi.ipkg) is typechecked for the first time; the banned-construct sweep is comment-aware, covers all Idris2 trees, and asserts the %default total / covering posture per module. Rust fast-core: cargo fmt --check, clippy -D warnings -D clippy::pedantic over all targets, cargo test (never run in CI before), all --locked. - quality: the list-and-pass steps become assertions (tracked .sh executable, none over 1MiB, missing core docs fail), TODO reporting is labelled advisory, and pinned ShellCheck runs at severity=style. Scripts it flagged are fixed, including two real bugs: missing line-continuations in maint-assault.sh and unexported variables consumed inside a bash -c child in the template e2e test. - CodeQL: security-and-quality query suite for the actions extractor instead of the default set. - release: git-cliff pinned + checksummed (was releases/latest with an asset name upstream does not publish - a guaranteed 404). - static-analysis: panic-attack and hypatia tool sources pinned instead of latest/floating HEAD; hypatia pinned to the same commit the estate governance reusable builds. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…nt the status docs
verification/proofs/lean4/ApiTypes.lean, verification/proofs/idris2/
Types.idr and verification/proofs/idris2/ABI/* were uninstantiated
RSR template mint files ('Template - replace with your project's
...'): members of no lake/ipkg package, never compiled by anything,
and recorded in PR #102 as not typechecking. The orphan guards added
to the just proof checks flag exactly this class, so the files go the
way of T5's three templates. PROOF-NEEDS repoints at the real ABI
seam (src/interface/Abi + abi.ipkg, now CI-typechecked) or marks the
need honestly homeless; the proofs README tree/commands describe what
exists; proof-debt gains a dated addendum for its now-historical rows.
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
… scoped Agda strictness, strict-clean schema, hypatia findings, Lean linter warnings
- actions.lock: an entry recording its own SHA as its ref is rejected
by the Actions backend at job setup (estate-audit died there);
cicd-suite ref is now the branch the commit came from ('main').
- proofs.yml Agda: CLI --exact-split -W error leaked into the stdlib's
compilation and failed on its Data.Maybe.Base.zipWith catch-all.
Exact-split/warnings-as-errors now live where they belong - the
theorem-b OPTIONS pragmas + theorem-b.agda-lib flags (registered as
a library in CI) - with a warning scan over theorem-b paths as belt.
- trope-ir schema: ajv strict mode found real gaps (contains without
type:array; untyped conditionals; strictRequired). All fixed as
semantics-preserving typings, proven verdict-identical to the old
schema over every positive and negative fixture.
- --wfail did its job on first contact: three linter.unnecessarySeqFocus
warnings in L4Monotonicity, fixed in the linter's suggested form.
- quality.yml: command-substitution while-loop returned the final
test's status under set -e; now if-form + true.
- Hypatia's real findings: build/setup.sh curl|bash replaced with a
pinned, checksum-verified just tarball (CWE-494); dependabot
auto-merge gets the contents: write it actually needs;
instant-sync skips cleanly when FARM_DISPATCH_TOKEN is absent.
- trope-check: failure-only clippy diagnostics step emitting every
lint as a check annotation for log-free diagnosis.
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…tyle-clean run blocks, wiki relocation, author-based dependabot gate - Agda: Q-inj proved by encode-decode transport instead of matching on refl, so --cubical-compatible is genuinely satisfied (the refl-match relied on constructor injectivity Cubical cannot compute through; warnings-as-errors caught it on first scoped run, as designed). - Lean: the (tac1; tac2) form must sit on one line; joined the two multiline comp_mono proofs. - actionlint runs ShellCheck at every severity: all 91 run: blocks are now style-clean. SC2295/SC2012/SC2035 fixed properly (quoted pattern expansion; find-based deed count). SC2129 carries a per-block recorded opt-out only where one-echo-per-summary-line is a readability choice. - estate formatting: wiki SOURCE pages move docs/wiki -> wiki/ (estate reserves docs/wiki* for published .md; this repo authors AsciiDoc). The generic docs/wikis template README goes with them. - dependabot: job gate is the PR author (unspoofable); the actor check is an in-job noise reducer gating later steps, not a boundary. - clippy diagnostics: full lint list to the step summary as well as the 10 annotations GitHub allows per step. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
… scope workflow secrets, and correct proof and conformance claims
…i pages to Markdown
…on check executable
…s, and proof helpers
…ffirmation key pinning, setup.sh portability, panic-attack from pinned source, Lean O1 on GradeR + axiom-audit compiler-decl filter Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…-repo resolver Canary findings from bfb8168, all root-caused: - patch-bridge.yml startup-failed and workflow-linter's lock-coverage step failed: the workflow was missing from actions.lock (a same-file edit collision dropped the entry), and GitHub's dependency locking refuses actions for workflows the lock does not name. Entry restored. - quality.yml's regression harness stubs gh as a silent logger, so the resolver's new canonical full_name query read empty stdout as a move to "". Resolver now treats empty as unresolved; the stub answers canonical/contents queries properly, and a third fixture case proves a moved repository (canonical name mismatch) is rejected — the exact 2026-10-28 outage class, now under test. - Confirmed by annotation: fork-governance/governance/secret-scanner now fail ONLY on the selected-actions allow-list (cross-owner reusables not yet admitted for metadatastician) — an owner Settings action, recorded in ADR 0006 prompt S1. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…low-list Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…lus knots Review-thread remediation for PRs #102/#107 (Codex + CodeRabbit): - proofs.yml axiom audit could hide a source axiom given a compiler-internal-looking name (private axiom forged_spec): the old filter excused any component containing _spec/_cstage/_unfold as a substring and dropped violations by declaration shape. Now: anchored compiler-minted component shapes only; any axiom DECLARED in the gated sources is never excused; a violation is dropped only when nothing non-allowlisted remains in it. The source tripwire is token-based (private/protected axiom now caught) and also rejects addDecl/axiomDecl. - workflow-linter resolver deduplicated by (repo, ref), so only the first reusable-workflow path per repo@SHA was existence-checked (eight of nine standards paths were unchecked). Dedup is now per coordinate; commit/tag resolution still happens once per (repo, ref). - ci/CI-CRITICALITY.toml: the retired static-analysis-gate entry is gone (its earlier removal was clobbered) and fork-governance is actually listed. - spec/calculus.adoc: 'deceptive' disambiguated into grade-deceptive (Falsified/Misbound/Conflated) vs fidelity-tier-deceptive (Unknown/top), at the Veridicality Derivation, L3 and C3, so Dropped absorbing Attenuated(top) no longer reads as laundering; C2 stated per carrier (unquotiented iff epsilon; A3-normalized finite core); O1-carrier now cites EffectAtomsRatified.GradeR.atom_factorization, the proof on the carrier in use; the detect profile is defined uniformly for all three deceptive duals (trope-ir aligned). - tests/workflows/review_regressions_test.sh: regression cases for the per-coordinate path check and for the axiom filter (extracted verbatim from proofs.yml; forged_spec declared/undeclared, internal-decl + sorryAx, genuine IR placeholders). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
… standards reusables Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
… debt ledger The fork-governance K9 lane executed for the first time on 2026-10-28 (run 40782505930) once the Actions allow-list admitted the canonical standards reusables. Verdict: 8 of 10 committed K9 files fail L0-L2 strict against contract v1.0.0 — rsr-template boilerplate and pre-contract drafts that predate the contract (TODO placeholders, missing pedigree.schema_version/component_type, a Hunt example with no signature block, two .k9 files that do not parse as Nickel). Standards grandfathered its own 25-file baseline the same way; fixing template semantics blind, or deleting the templates, would be worse. The ledger is shrink-only and renderer-enforced: conform-ing files must leave it, new debt cannot join it silently, and touching a listed file voids its exemption. Ratchet-exception: .machine_readable/k9-contract-debt.txt — first-ever K9 baseline for this repo; the 8 entries are the exact failing set of run 40782505930, cross-checked locally at L1 with canonical k9-validate.sh (standards@34cf03f9). Shrink work tracked against the lane, entry by entry. Also drop the curl|sh one-liner advertised in build/setup.sh (the 99-day Hypatia shell_download_then_run high): the script's own downloads are already sha256-verified pinned archives; remote-pipe bootstrap of the setup script itself was the indefensible part. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…ions Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…script usage path
…script usage path
…t Patch Bridge triage, axiom regression fixtures, and proof documentation
…a review round Witness selection (Codex on calculus §6.2): both checkers scanned the edges array in document order, so permuting the JSON changed the named witness and a violating non-ancestor edge could be blamed. Both cores now compute candidates as the output's ancestor DAG in topological order with edge-ID tie-breaking (Kahn, smallest ready ID). Conformance gains witness-permutation-a/-b: identical graphs, permuted edge arrays, both must name e_alpha. Rebased onto the CodeRabbit agent's f7f4139 (fork-governance workflow_run publisher, Patch Bridge http/v1/dedupe fixes, wiki/spec/ ci-cost corrections) — overlaps union-merged: their publisher replaces my same-repo verdict guard; my calculus/ci-cost wording kept. This commit adds the threads that were not CodeRabbit's: - proofs.just: mirror proofs.yml token-based axiom detection (private axiom, addDecl/axiomDecl) so verify-all is not weaker. - trope-check: push paths cover abi.ipkg + src/interface. - just e2e: depends on trope-build (no stale-binary conformance). - rust: stable map().unwrap_or_default() for unstable map_or_default. - instant-sync: harden-runner egress audit on the token-bearing dispatch job (Hypatia RE001), actions.lock updated. - workflow-linter diagnostics: capture-and-report exit code instead of || true (Hypatia RE005). - harness: undeclared-_spec_1 twin completing the declared/undeclared discrimination pair around source_declared_axiom. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…sure, lock order - str_list and its two call sites use a plain match: map_or_default is unstable on some stable toolchains (Codex), while map().unwrap_or_default() trips clippy::map_unwrap_or under -D warnings, which tries to turn it back. The match is accepted by every toolchain and lint set. - Extract the Kahn readiness predicate so its formatting is the rustfmt-canonical chain layout. - actions.lock: list instant-sync actions in file-appearance order (harden-runner is the first step), matching gh actions-lock output. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…y entry CI log ground truth: rustfmt wants the collect broken after '=' (the only diff hunk), and gh actions-lock --verify-local requires a dependencies: entry (ref/commit/owner_id/repo_id) for step-security/harden-runner@v2.22.3, not just the per-workflow list. SHA/IDs taken from the live repo (tag v2.22.3 -> commit 46b06ce). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…h name
Hypatia SARIF gate (run 40789972726): workflow_audit
actions_expression_injection (critical) on fork-governance-publish —
${{ github.event.workflow_run.head_branch }} in the concurrency group.
A concurrency key is not a shell context, but there is no reason to
key on an attacker-controlled string when the head SHA is available
and the publish step already re-validates the PR head against it.
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Before grade accumulation the calculus requires rejecting unknown node references, duplicate producers and cycles as validation faults that MUST NOT produce a verdict. Neither core enforced it: accumulation treats a missing producer as grade ε, so a schema-valid document with an undeclared use_model.output returned p-sufficient (Codex P1). Both decoders now validate (lib.rs::validate_graph, Decode.validateGraph): unique node IDs; edge inputs/outputs and use_model.output all declared; at most one producer per node; producer graph acyclic (Kahn). Faults ride the existing validation-fault/exit-2 channel in both CLIs. Conformance gains graph-invalid/ (7 schema-valid fixtures, one per fault class) driven by a new run.sh loop; the calculus paragraph that admitted the gap now records conformance. The pre-existing corpus was machine-checked clean under the new rules before enabling them. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
A fork PR controls the PR-side Fork governance workflow, so it could upload a fork-governance-result artifact with correct identifiers and arbitrary green lanes, and the trusted workflow_run publisher would post it as github-actions[bot]. The publisher now refuses unless: - the source run's referenced_workflows include every reusable the DEFAULT branch's fork-governance.yml names, at the same pins (a pin-bump PR simply gets no comment until merged — fail closed); - lane pass/fail is derived from GitHub's own job conclusions for the run, and the artifact's lane claims must agree with them. Rendering takes results from the API-derived lanes; only verdict shading/grids remain artifact-sourced (produced by the proven-called reusables). Concurrency is also keyed on fork identity + head SHA so two forks' same-named branches cannot cancel each other's publisher (Codex P2). jq lane derivation and the reusable-set comparison were verified against run 40789972726's real API data. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…/trope-checker into arena/99ad561a-trope-checker # Conflicts: # .github/workflows/trope-check.yml # docs/wiki/Home.adoc # src/rust/src/lib.rs Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
Important Review skippedToo many files! This PR contains 127 files, which is 27 over the limit of 100. To get a review, reduce the PR to 100 files or fewer by splitting it into smaller PRs or changing its base branch. Upgrade to a paid plan to raise the limit. This review couldn't start because sufficient usage credits or metered capacity aren't available. Add credits or update usage-based reviews in the billing tab, then retry.
 |
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
hyperpolymath
marked this pull request as ready for review
October 29, 2026 11:53
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. |
hyperpolymath
enabled auto-merge (squash)
October 29, 2026 15:40
|
Add Carrot credits or activate Agent usage billing to use Autofix |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Scope
This draft includes the current head of #107 and is intended to supersede it after the remaining blockers are resolved. It preserves #102 through #107. No other PR or branch has been merged or closed.
Known blockers / limitations
workflow_rununtil its workflow is present on the default branch. Its output is not an independent attestation of scanner execution or a security certification. K9 has eight ledgered debt entries; advisory fleet reports remain incomplete.Validation
f64f360, GitHub conformance (Rust and Idris), Lean, Agda, quality, workflow lint and SonarCloud passed. The pinned standards allowlist preflight failed, and the Hypatia scan failed with exit 139 on two successive runs; K9, DEED and fleet jobs passed.