Repository navigation
fix(proofs): NaN-safe trust base, estate proof-debt ledger, POSIX-sh gate port (follow-up to #18; closes #4) - #19
Merged
Merged
Conversation
Follow-up to the merged PR #18 (main was left red on the two checks this PR owns — the Agda job and the anti-pattern policy). Incorporates the full review outcome, including one genuine soundness find: 1. SOUNDNESS: the draft `mul-sign` axiom (0 <= a -> b <= 0 -> 0 <= -(a*b)) was REFUTABLE: at a = 0, b = log2 0 = -inf the product is NaN, and T (0 <=b NaN) is inhabited — an inhabited-refutable axiom proves False. Fixed structurally, not by hypothesis-tightening: plogp/klTerm now carry a strict positivity guard (0.0 <b v) inside the term, are NaN-safe for every input (v <= 0 or NaN -> 0.0; v = 1 -> -0.0 with 0 <=b -0.0 true), and the mul-sign + log2-nonpos pair collapses to one honest per-entry ffi-fact `plogp-nonneg`. Trust base 6 -> 5 postulates; entropy-nonneg and js-symmetric remain proven top-level theorems; sanity is pinned by refl/T lemmas (klTerm-zero-left, plogp-zero, plogp-one-boundary). 2. ESTATE cross-dependency: adds docs/proof-debt.md in the Trusted-Base Reduction Policy schema (§a discharged / §c necessary / §d dated debt, owner @hyperpolymath, deadline 2027-03-31 tied to standards#124) and AXIOM:/TRUSTED: leading comment blocks on both postulate keywords, so the long-red governance job `Trusted-base reduction policy` now passes locally against standards@main check-trusted-base.sh. 3. LANGUAGE POLICY: scripts/audit-trust-base.py deleted (estate bans .py); the validated gate is re-implemented as scripts/audit-trust-base.sh (POSIX sh + awk, same 7 check families; negative tests re-passed). 4. CI ROBUSTNESS (review ports + prior findings): conservative detect-step (failed diff => verify, never skip), per-file OPTIONS-pragma regex (not substring), apt-layout stdlib probe (-i /usr/share/agda-stdlib; the find-*.agda-lib logic can never succeed on noble), --compile-dir into a writable dir, ubuntu-24.04 pin (ubuntu-latest drifts on 2026-10-19), explicit lower d {i} implicits. Gate logic unchanged where it was already validated; audit + estate checker both pass on this tree locally; first real agda type-check runs in CI. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Contributor
|
Warning Review limit reachedYou've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository. Next included review available in 7 minutes. View limit detailsLimit details: You’ve used the included review currently available. Review configuration: ⚙️ Run configuration
📒 Files selected for processing (16)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
…compile-dir The first live run of the Agda job died with a bare "exit code 42" (Agda's universal error code) because the script ran agda unguarded under set -eu inside the stdlib probe — the runner log (the only place the real error text lives) is not retrievable from this environment, and GitHub annotations showed nothing. Changes: - every agda invocation now goes through run_agda: captures combined output, echoes it indented to the step log (and thus the artifact), and on failure re-emits the first 14 lines as a workflow ::error:: annotation with %0A/ %25/%3A%3A escaping (annotations are API-readable; raw logs are not); - `agda --version` no longer aborts the script under set -e (fake-agda negative test exposed it); - probe fallback: on failure with --compile-dir, retry without it (packaged pre-compiled .agdai trees can reject a foreign compile-dir); corpus loop honours whichever mode won; - explicit fail-closed ::error:: naming the detected STDLIB_DIR when the probe is unsalvageable. Validated locally with a stub agda (exit 42 + error text): annotations render escaped and correctly; clean exit 1 from the probe guard. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Live annotation exposed it: the probe module lived in a temp dir outside every include path, so Agda rejected `module Probe` with its filename check (the same rule our corpus naming was designed around). Stdlib discovery itself worked (/usr/share/agda-stdlib detected). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…tes go next to the source, not into --compile-dir Live annotation (2nd iteration): with /usr/share/agda-stdlib detected fine, Agda re-checked Data.Unit.Base (packaged .agdai fingerprint mismatch) and died on `removeLink: permission denied` rewriting the root-owned interface file. The initial belief that --compile-dir relocates .agdai outputs is wrong (it only moves executables), so the gate now copies the stdlib tree into $HOME/.cache when it is not user-writable and points -i at the mirror. tar preserves mtimes, so no additional staleness is introduced; the mirror is reused if a later run finds it already populated. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
….Fin / Data.Vec tops CI iteration 3 evidence: the run reached `Checking Data.Fin -> Data.Fin.Properties` and failed on a stdlib-internal without-K/cubical interaction — but the apt agda-stdlib in noble is 1.7 (tag v1.7: `--without-K --safe` in those files; the cubical-compatible variant is v1.7.2, not this package). The pragmatic and strictly cheaper fix: our corpus only needs the constructors/operations, which live in *.Base — importing the tops drags in Properties machinery we never use (and, with it, whatever flag archaeology a distro tree hides). Foundations already compiled clean through Data.Nat/Data.Float/PropEq in the same run, so those stay as-is. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…safe
Live annotation (iteration 4): "Cannot postulate plogp-nonneg with safe
flag" — Agda inherits *command-line* flags into every imported module and
an OPTIONS pragma cannot revoke them, so passing --safe while checking the
top InformationTheory header poisoned the quarantined Axioms import. The
corpus files carry their flags in `{-# OPTIONS ... #-}` (Theory and
Foundations: --safe --without-K; Axioms: --without-K), and the audit step
independently enforces that safe modules keep their pragma — so per-file
pragmas lose no guarantee while isolating each module's flag set. Probe
aligned (no flag) so stdlib interfaces are built once per run, not twice.
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…not import the quarantine Iteration 5's annotation was the last honest obstacle: "Importing module InformationTheory.Axioms not using the --safe flag from a module which does" — Agda's flag inheritance forbids a --safe module to depend on anything unsafe. Rather than launder the axioms, the corpus now treats the rule as a feature and encodes it: - InformationTheory.agda (theorem header): drops its --safe claim, keeps --without-K, and says why in its header. It contains no postulates — the census still proves that — its --safe-forbidden status is *exactly* the statement "this header rests on FFI facts", machine-checked by Agda itself. - Foundations remains the sole --safe module: every definition, order relation and NaN guard carries the real certificate. - trust-base.json gains `derived_modules`; scripts/audit-trust-base.sh registers it exhaustively and adds the inverse honesty check (a derived file CLAIMING --safe is now a hard audit failure — negative-tested; and a safe module dropping its pragma still fails, so graduation between classes is only possible with an honest manifest update). - README/Axioms headers reworded; layering story = safe definitions / quarantine / derived theorems, with the audit's "add to safe_modules/derived_modules" guidance. If the corpus type-checks now (its imports all did), the gate goes green for the first time in this repo's history. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
First genuine PROOF error in the corpus's history (every import chain now compiles): Agda reported "blocked on _a_" — the where-bound midpoint module of jsdF is opaque to the unifier when the matching proof also destructs under it, so the add-comm/cong₂ chain could not see the shared midpoint. Two changes, both strictly more transparent: - Foundations.jsdF inlines `zipWith midpointF ps qs` in both KL terms (comment records why: where-clauses become local modules); - InformationTheory.js-symmetric is rewritten pointfree-end-to-end: each endpoint is syntactically the reduct of `jensen-shannon`, with explicit arguments to add-comm/zipWith-comm instead of holes, and no local where bindings in the proof term either. Semantics untouched; entropy-nonneg and the sanity lemmas were already accepted by the compiler in the same pass (the failure report listed only the js constraints). Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Owner
Author
Final state — all own checks green on 9a8c900/76bda5e
The iteration trail (each step driven by the new
Ready for review; nothing here needs the earlier PR #18 branch anymore (that head was auto-deleted at merge). |
|
hyperpolymath
enabled auto-merge (squash)
October 4, 2026 02:27
hyperpolymath
disabled auto-merge
October 4, 2026 06:23
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
1 participant
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.
Why this PR exists
PR #18 merged (a4e33a9) but main went red on both of its checks: the governance
anti-pattern policyjob (the merged tree carriedscripts/audit-trust-base.py; estate bans Python files) and theAgda — proofs/theoriesjob (the merged workflow still used the.agda-lib-only stdlib registration, which can never succeed with Ubuntu'sagda-stdliblayout). And the review surfaced a genuine soundness bug in the axiom set. This branch carries the full resolution — it is the continuation of #18, not a replacement design.1. Soundness fix (the important one)
CodeRabbit's review caught that my original
mul-sign : 0.0 ≤ᶠ a → b ≤ᶠ 0.0 → 0.0 ≤ᶠ - (a * b)was refutable: ata = 0.0,b = log₂ 0 = −∞, the product is0·(−∞) = NaN, andT (0.0 ≤ᵇ NaN)is inhabited — a refutable axiom inhabits⊥and proves anything. Tightening the hypothesis to0.0 <ᶠ a(the suggestion) makes that entry axiom true, but the merged corpus then fed the non-strictlower dhypothesis into the strict mul-sign, so the chain wouldn't even type-check.This PR fixes it structurally instead of hypothesis-wise: the strict guard moves into the term.
0.0, which is what the0·log 0 = 0convention prescribes; no caller can ever observe an unguarded product).v = 1→−0.0, and0 ≤ᵇ −0.0computes true, so the boundary is consistent (plogp-one-boundary : 0.0 ≤ᶠ plogp 1.0 = ttpins this).log₂-nonpos+mul-sign+neg-nonposentry-wise machinery collapses to one honest FFI axiom:plogp-nonneg : (v) → 0.0 ≤ᶠ v → v ≤ᶠ 1.0 → 0.0 ≤ᶠ plogp v.plogp-nonnegadd-nonnegadd-comm; conjecture 2:kl-nonnegjs-bounded).entropy-nonnegandjs-symmetricremain proven top-level theorems (per-entry float lemma postulated, top-level theorem proven — exactly the split POSTULATE-AUDIT Phase 2 prescribed); theDistributionhypothesis transport (lower d {i}, per the review) is kept.with-abstraction stuck-term gymnastics anymore:plogpB/klTermBare deleted, so the definitional-equality fragility in the old entropy chain is gone too.2. Estate cross-dependency: the
Trusted-base reduction policyjobstandards/scripts/check-trusted-base.sh(governancetrusted-basejob) has been red on this repo since the pre-2026 corpus — it demands everypostulatemarker be inline-annotated or ledgered. Done properly:postulatekeyword now has a contiguous-- AXIOM:/-- TRUSTED:leading comment block (the checker walks back only through comment lines — this is why the estate marker must sit above the keyword, not per-declaration);docs/proof-debt.mdin the policy schema: §(a) three discharged items (entropy-nonneg, js-symmetric, the five 2024 float "axioms" that are now plain re-exports), §(c) the three necessary ffi-facts with justifications/citations, §(d) the two conjectures with owner + deadline (2027-03-31, standards#124 sweep boundary);standards@mainscript:[OK] All 2 escape hatch(es) are documented.3. Language policy: Python is banned — gate ported to POSIX shell
scripts/audit-trust-base.pydeleted (anti-pattern job fail); all gate logic now lives in two.shfiles that both CI systems (GH Actions + GitLab) andjust prove-*share:scripts/prove-agda.sh— apt-layout stdlib probe (-i /usr/share/agda-stdlibwhen/usr/share/agda-stdlib/Dataexists;.agda-libdiscovery only as fallback),--compile-dirinto a writable dir (the shipped.agdaitree is root-owned), fail-closed on empty corpus, per-file flags chosen by a{-# OPTIONS … --saferegex (not substring — per review), and--safeiff the pragma claims it.scripts/audit-trust-base.sh— the seven check families ported 1:1 from the python audit whose negative-test battery (smuggled postulate, foreign file, rename drift both directions, vacuouswhere-relation, budget overflow) is re-validated on the port (see below).4. CI robustness ports
Detect proof changes: ongit difffailure → warn +proofs=true(conservative; the old|| truepath could skip verification on error — suggestion adopted with the polarity flipped to fail-safe).runs-on: ubuntu-24.04pinned on the correctness job (ubuntu-latestfloats to 26 on 2026-10-19 mid-review-window).paths:filter remains (issue Agda proofs under proofs/ have no CI here — the verifying job is stranded in standards #4 req [1]); corpus non-empty assertion (req [2]) kept in both the sh audit and prove-agda.Validation
sh scripts/audit-trust-base.sh .→OK — 5 postulate(s) (conjecture=2 ffi-fact=3), 2 safe module(s); negative battery T1 (smuggledpostulateinto Foundations) and T2 (extra tagged axiom) both exit 1 with all expected::error::families; estatecheck-trusted-base.shgreen as above.agda 2.6.4type-check of this corpus runs in this PR's CI — the job previously died before invoking Agda on main. If residual errors surface, fixes land here.Refs: #4, #18.
Closes #4(issue body's remaining acceptance: verified corpus — this PR makes it actually verify).