feat(phd): bridge audit + reconciled assertions + trios-phd skeleton#263
feat(phd): bridge audit + reconciled assertions + trios-phd skeleton#263gHashTag wants to merge 1 commit into
Conversation
* trios-phd crate (new):
- cite::{CodataLink, CoqLink, ProofStatus} with R5 honesty contract
- audit subcommand consumes assertions/igla_assertions.json schema v1.0.0
- status subcommand prints per-invariant Proven/Admitted with coq file
- SUPPORTED_SCHEMA_VERSIONS = ["1.0.0"] β refuses unknown versions
- 12 unit tests, all green (R4/R5/budget/duplicate-id/proven-vs-admitted)
* docs/phd/BRIDGE_AUDIT.md:
- documents schema v1.0.0 absorption (commit b959c43)
- INV-12 Trinity-base ASHA rungs noted (1000 Γ {3β°..3Β³})
- INV-1 coq file rename (lr_convergence.v β lr_phi_optimality.v)
- honest deferral of Track A (BPB race, GPU-blocked) and Track B (1500-line chapters)
* .github/workflows/laws-guard.yml:
- quoted 9 step names with embedded colons
(L1, L2, I5, I1, I2, I3, I4, I7, I9 β "X: ...")
fixes startup_failure that was hitting every push on main
* .github/workflows/coq-check.yml:
- replaced fragile inline python heredoc with cargo-driven validators
- new step: cargo test -p trios-phd
- new step: cargo run -p trios-phd -- --repo . audit
- summary table updated for 6 invariants incl. INV-12
* Cargo.toml: registered crates/trios-phd as workspace member (51 total)
ΟΒ² + Οβ»Β² = 3
Refs: #30 #62 #109 #143
PR: #263
767d7a4 to
1fbc2ba
Compare
* trios-phd crate (new):
- cite::{CodataLink, CoqLink, ProofStatus} with R5 honesty contract
- audit subcommand consumes assertions/igla_assertions.json schema v1.0.0
- status subcommand prints per-invariant Proven/Admitted with coq file
- SUPPORTED_SCHEMA_VERSIONS = ["1.0.0"] β refuses unknown versions
- 12 unit tests, all green (R4/R5/budget/duplicate-id/proven-vs-admitted)
* docs/phd/BRIDGE_AUDIT.md:
- documents schema v1.0.0 absorption (commit b959c43)
- INV-12 Trinity-base ASHA rungs noted (1000 Γ {3β°..3Β³})
- INV-1 coq file rename (lr_convergence.v β lr_phi_optimality.v)
- honest deferral of Track A (BPB race, GPU-blocked) and Track B (1500-line chapters)
* .github/workflows/laws-guard.yml:
- quoted 9 step names with embedded colons
(L1, L2, I5, I1, I2, I3, I4, I7, I9 β "X: ...")
fixes startup_failure that was hitting every push on main
* .github/workflows/coq-check.yml:
- replaced fragile inline python heredoc with cargo-driven validators
- new step: cargo test -p trios-phd
- new step: cargo run -p trios-phd -- --repo . audit
- summary table updated for 6 invariants incl. INV-12
* Cargo.toml: registered crates/trios-phd as workspace member (51 total)
ΟΒ² + Οβ»Β² = 3
Refs: #30 #62 #109 #143
PR: #263
1fbc2ba to
f1d7628
Compare
π Update β rebased on
|
| Rule | Status |
|---|---|
| R1 Rust-only build | β
β no .sh, no python; removed test_issue_237.sh |
| R2 branch policy | β
β feat/phd-* for PhD bridge work, no main pushes |
| R4 L-R14 traceability | β
β every constant in trios-phd traces to schema v1.0.0 + .v file |
| R5 Honest Admitted | β
β INV-1, INV-3, INV-4, INV-5 reported Admitted; INV-2, INV-12 Proven |
| R6 zero free parameters | β
β only Ο-derived + n β β€ constants |
Pre-existing CI failures (attribution)
The Constitutional Enforcement and Test workflows had been failing on every commit to main (visible in run history before this PR's first push) because:
- 9 step names with unquoted colons β
startup_failurein 0s LAWS_SCHEMA_VERSIONgrep didn't match markdown-bold formtest_issue_237.shwas checked into root but L1 rule forbids.sh
This PR fixes all three; the gates now actually run. If they newly fail after this push, those failures are lane-relevant, not pre-existing.
Throne updated
Throne issue #264 now lists this PR under Β«π Active ONE SHOTSΒ» with status OPEN Β· rebased on schema v1.0.0 Β· 12 tests green Β· CI re-armed.
ΟΒ² + Οβ»Β² = 3
* trios-phd crate (new):
- cite::{CodataLink, CoqLink, ProofStatus} with R5 honesty contract
- audit subcommand consumes assertions/igla_assertions.json schema v1.0.0
- status subcommand prints per-invariant Proven/Admitted with coq file
- SUPPORTED_SCHEMA_VERSIONS = ["1.0.0"] β refuses unknown versions
- 12 unit tests, all green (R4/R5/budget/duplicate-id/proven-vs-admitted)
* docs/phd/BRIDGE_AUDIT.md:
- documents schema v1.0.0 absorption (commit b959c43)
- INV-12 Trinity-base ASHA rungs noted (1000 Γ {3β°..3Β³})
- INV-1 coq file rename (lr_convergence.v β lr_phi_optimality.v)
- honest deferral of Track A (BPB race, GPU-blocked) and Track B (1500-line chapters)
* .github/workflows/laws-guard.yml:
- quoted 9 step names with embedded colons
(L1, L2, I5, I1, I2, I3, I4, I7, I9 β "X: ...")
fixes startup_failure that was hitting every push on main
* .github/workflows/coq-check.yml:
- replaced fragile inline python heredoc with cargo-driven validators
- new step: cargo test -p trios-phd
- new step: cargo run -p trios-phd -- --repo . audit
- summary table updated for 6 invariants incl. INV-12
* Cargo.toml: registered crates/trios-phd as workspace member (51 total)
ΟΒ² + Οβ»Β² = 3
Refs: #30 #62 #109 #143
PR: #263
f1d7628 to
5792e0a
Compare
β
CI status after final push (
|
| Check | State | Note |
|---|---|---|
| Constitutional Enforcement | β PASS | YAML + schema-grep + LAWS_HASH all green now |
| guard | β pass | |
| GitGuardian Security | β pass | |
| Nine Kingdoms Verification (cargo build) | β fail | pre-existing on main β crates/trios-ui/rings/UR-00/src/lib.rs:177β215 dioxus GlobalSignal API drift (E0308 Γ 8). Not introduced by this PR. |
| Test (cargo test) | β fail | same UR-00 build break β never reached cargo test step |
Pre-existing failure attribution (per coq-runtime-invariants skill Β§"CI failure attribution")
The two remaining failures are not caused by this PR:
crates/trios-ui/rings/UR-00/src/lib.rsis part of the Trinity UI ring (a Dioxus app), totally separate from the PhD bridge / IGLA RACE / runtime guard chain.- The
GlobalSignal<T> = Signal::new(...)pattern stopped compiling after adioxusupstream change toGlobalSignal::new. - These errors were present on
mainbefore this PR. They were hidden because theL1: No .sh filesstep exited 1 first (due to the roguetest_issue_237.shchecked into root), so cargo never ran. Removing that.sh(which itself violated R1/L1) exposed the deeper UI breakage that the L1 gate had been masking.
What this PR fixed in CI
- β
laws-guard.ymlno longer dies in 0s asstartup_failure(9 colon-quoting fixes) - β
coq-check.ymlno longer dies in 0s (heredoc python replaced with cargo validators) - β
LAWS_SCHEMA_VERSIONgrep now matches markdown-bold form - β
LAWS_HASHregenerated with relative path (was hardcoded/Users/playra/trios/LAWS.md) - β
test_issue_237.shremoved (it violated the very L1 rule that was blocking)
What this PR does NOT touch
crates/trios-ui/rings/UR-00/β Dioxus UI ring, a separate fiefdom. Should be a follow-up issue. Suggested fix:static X: GlobalSignal<T> = Signal::global(|| T::default());(Dioxus 0.6 idiom).
Local verification (this PR's deliverables)
$ cargo test -p trios-phd
running 12 tests ... 12 passed; 0 failed
$ cargo run -p trios-phd -- --repo . audit
assertions self-check: OK (schema 1.0.0, 6 invariants: 2 Proven, 4 Admitted)
chapters scanned: 34
\coqbox unresolved: none
admitted-without-\admittedbox: none
audit: OK
This PR is ready to review. The two red checks should be split into a separate fix(ui-ur00): repair Dioxus GlobalSignal initialisers PR.
ΟΒ² + Οβ»Β² = 3
|
Closing in favour of the now-merged #269 baseline. The Worth porting to a fresh branch on top of current
[agent=computer-queen] |
Summary
Honest first-strike on the One Shot β PhD β trios β trinity-clara mission (2026-04-25T21:58+07). Lands the proof β runtime β monograph bridge primitives without faking the empirical or chapter-writing work.
Refs: #30 #109 #143
Closes: #62 (partially β skeleton + audit only; tectonic + page-count gate are follow-ups, see
docs/phd/BRIDGE_AUDIT.mdΒ§6.B)What this PR lands
crates/trios-phdβ new workspace member.cite::{CodataLink, CoqLink, ProofStatus}β the only sanctioned ways to introduce numeric constants into the monograph (rule R4).audit::{Assertions, run_audit, AuditReport}β typed loader forassertions/igla_assertions.json+ chapter-walking R4/R5 enforcement.cargo run -p trios-phd -- auditand... statussubcommands.assertions/igla_assertions.json(single source of truth):admitted_budget.used = 2cross-checked againstgrep -E '^Admitted\.|^Proof\. Admitted\.' trinity-clara/proofs/igla/*.vβ exactly 2 hits.admitted: 4; the alleged INV-5 hit atlucas_closure_gf16.v:104is a comment, not anAdmitted.directive. Corrected.Qed./Admitted.counts.proof_qed: false/proof_status: "Admitted"becauselr_convergence.v:48(alpha_phi_lb) and:51(alpha_phi_ub) are realAdmitted.directives. Per rule R5 we don't paper this over.[1.5, 2.8]vs certified[Ο, ΟΒ²]) kept as sibling fields, never merged (forbidden action).docs/phd/BRIDGE_AUDIT.mdβ full honest delta against the mission spec, including the punch list for follow-ups (Tracks A/B/C, proofs consolidation, CI gates, editorial duplicates).What this PR does NOT do (intentionally)
tectonicbuild + PDF artifact.github/workflows/coq-proofs.ymledits.generate-figure/export-trialssubcommandsFull reasoning + per-item tracking in
docs/phd/BRIDGE_AUDIT.md.Honesty contract enforced
The audit unit tests guarantee at every CI run:
\coqbox{INV-X}indocs/phd/chapters/**.texresolves to a known invariant.\coqbox{INV-X}for an Admitted invariant must be paired in the same chapter with\admittedbox{...}.admitted_budget.used β€ max, sum-of-files matches top-line,proof_qed == (proof_status == "Proven").Verification
Constants pinned
PHI = 1.618_033_988_749_894_8(with// ΟΒ² + Οβ»Β² = 3)prune_threshold = 3.5,warmup_blind_steps = 4000,d_model_min = 256,lr_champion = 0.004prune_threshold = 2.65(J-001/J-002 champion-killer)Followup PRs (per
BRIDGE_AUDIT.mdΒ§6)A. Editorial β merge/delete duplicate chapter files (
01-golden-egg.texvs01-golden-seed.tex;32-conclusion.texvs33-conclusion.tex).B.
trios-phdβcompile,bibtex-check, page-count gate, tectonic.C. Convert
trios/trinity-clara/to a real submodule or remove the stale in-tree mirror.D. Update
crates/trios-igla-race/src/invariants.rsto consume reconciled JSON viatrios_phd::audit::Assertions.E. CI gates β add
cargo test -p trios-phdtocoq-check.yml,auditstep tocoq-proofs.yml.F. Track A (gated on GPU).
G. Track B (one chapter, one PR).
ΟΒ² + Οβ»Β² = 3.