Skip to content

Commit 4812f1c

Browse files
hyperpolymathhyperpolymath
committed
docs: relocate proof/audit/example reference material from Desktop staging
Consolidates reference material that had been living loose in ~/Desktop/Project_Work/ into its canonical home in standards/: - docs/proofs/REQUIREMENTS-MASTER.md — 292-repo proof tier catalog (T1-T5 x TP/INV/SEC/CONC/ALG/ABI/DOM), generated 2026-04-04 - docs/proofs/spec-templates/ — per-tier spec template tree - docs/audits/dogfooding-matrix-2026-04-04.md — 437-line dogfooding audit matrix, synced 2026-04-04 session 10 - docs/audits/2026-03-30/ — 7 pre-remediation audit snapshots - k9-svc/examples/{simple,complex}.k9, conversation-walkthrough.txt — K9 usage examples AI-WORK.md section C3 and M3 updated to point at these new paths instead of the Desktop locations.
1 parent 547fb91 commit 4812f1c

293 files changed

Lines changed: 15822 additions & 0 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎docs/audits/2026-03-30/AI-PROOF-DISCLOSURE-STATEMENT.md‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
# AI-Assisted Proof and Publication Disclosure Statement
2+
3+
Last updated: 2026-03-30
4+
Status: Working statement; review against venue policy before each submission.
5+
6+
## Core Position
7+
8+
Using an LLM for proof drafting, search, refactoring, or explanation is not, by itself, disqualifying.
9+
What matters is whether the final mathematical and engineering claims are:
10+
11+
- correctly stated
12+
- honestly scoped
13+
- mechanically checked where formal claims are made
14+
- owned by the human authors
15+
16+
The trusted object is not the LLM. The trusted objects are:
17+
18+
- the proof assistant kernel or checker
19+
- the checked artifact
20+
- the stated assumptions
21+
- the authors' review and responsibility
22+
23+
## What We Should Say
24+
25+
Recommended framing:
26+
27+
> We used LLM tools for proof-script drafting, search, and refactoring. Final theorem statements, assumptions, and proofs were reviewed by the authors and mechanically checked in the proof assistant. No `sorry`, `admit`, `postulate`, `believe_me`, or analogous escape hatches remain in the checked artifact. The authors remain fully responsible for the correctness and scope of all claims.
28+
29+
## What We Should Not Say
30+
31+
Avoid wording like:
32+
33+
- "The LLM proved it."
34+
- "Claude proved the theorem."
35+
- "ChatGPT did the mathematics for us."
36+
37+
That framing weakens credibility because it sounds like responsibility and understanding were outsourced.
38+
39+
## Practical Rule
40+
41+
- Trust the LLM as a drafter and search assistant.
42+
- Trust the checker for formal validity.
43+
- Trust human review for theorem choice, assumptions, and claim discipline.
44+
- Do not make a publication-grade claim if any shortcut or unreviewed assumption remains.
45+
46+
## Review Trigger
47+
48+
Before any conference, journal, archive, or talk submission:
49+
50+
1. Check the venue's current AI/disclosure policy.
51+
2. Check that the wording still matches the artifact.
52+
3. Check that the statement does not outrun what is actually machine-checked.

‎docs/audits/2026-03-30/LLM-PROOF-TRUST.md‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
# LLM Proof Trust Statement — 2026-03-30
2+
3+
## Context
4+
5+
This note responds to the question: *“How much can you trust proofs proposed by large language models, and what signals matter when those proofs are offered in a conference or publication?”* The short answer is: LLMs can help generate ideas or structure for proofs, but the only proof that counts is one that has survived a machine-checker, so we treat every LLM-contributed argument as a draft that still needs full mechanisation.
6+
7+
## Trust Boundaries
8+
9+
1. **Human-in-the-loop discovery**: LLMs can suggest definitions, lemmas, or proof structure, but they do not know the current codebase state the way a domain expert does. Their outputs are statistically likely but not guaranteed to be correct. We therefore treat their contributions as “propositional sketches” that only become evidence once formalised.
10+
11+
2. **Mechanised verification requirement**: Every claim that reaches a conference or software release must be checked by a legitimate proof assistant (Idris2, Lean 4, Agda, Coq, or a specialist system). The checklist is: (a) the LLM proposal has been ported into the target language; (b) the body compiles/executes with `%default total` (or equivalent); (c) there are zero `believe_me`, `sorry`, `postulate`, or placeholder gaps in the proof tree; (d) CI reproduces the result cleanly. Without those steps, the claim remains an *informal idea*, not a formal proof.
12+
13+
3. **Publication posture**: If we submit a paper or talk and mention “LLM-assisted proof work,” make it clear that the human team controlled the mecanisation and the proof assistant produced the final acceptance. Audiences expect that a “LLM-enabled” proof was vetted with a proof checker. If they ask “did you run it through Idris/Lean/Agda?” the honest answer is “yes, and here is the proof script and log.” Saying “an LLM or Claude wrote the proof” without the machine-checked artefact invites skepticism; reviewers will look for the actual proofs, not the chat transcript.
14+
15+
4. **Community credibility**: Presenting an LLM-assisted proof without the mechanised artefact is a reputational risk. Even if the idea is sound, the community will remain hesitant until they can rerun it themselves. In contrast, showing the mechanised artefact—annotated, tested, and reproducible—signals that we treated the LLM output with the same rigor as any other contribution.
16+
17+
## Actionable Notes
18+
19+
* Always store the mechanised proof file under version control, with the proof assistant command needed to produce it documented in the repo.
20+
* Log the proof assistant version and command line so reviewers can reproduce the result. If the proof depends on Idris2, record `idris2 --check Proof.idr`; if Lean 4, record `lean --make theorem.lean`.
21+
* When a paper cites our proof, include the reference path (e.g., `proofs/Idris/TypeLL/Totality.idr`) and the proof assistant output (CI logs or local run). That way the reviewer can confirm the evidence themselves, independent of the LLM conversation.
22+
* If a claim is still at the “LLM sketch” stage, label it clearly as *proposed* or *conjectured* and do not elevate it to “proven”, “verified”, or “formal” in any README, paper, or release note.
23+
24+
## Summary
25+
26+
LLMs can help brainstorm proofs, but the only trust we extend is to proofs that have been mechanised, type/totality-checked, and reproduced by our CI. Mentioning LLMs in a paper should come with the disclaimer that the final artefact was verified by a theorem prover and that the LLM’s role was limited to the exploratory phase. Without that verification, reviewers will treat the output as low-trust research notes, and our release-pre-flight gate will not clear the claim.

‎docs/audits/2026-03-30/PAPER-STATUS.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
# PAPER-STATUS — 2026-03-30
2+
3+
| Paper / Repo | Venue Target | Evidence Status | Next Steps |
4+
|-------------|--------------|-----------------|------------|
5+
| `007-lang-private-docs/paper/007-agent-meta-language.tex` | HOL / Zenodo | Proofs outstanding (soundness/budget/isolation), tests missing → not ready. | Finish declaring theorems in Idris2/Lean4, run e2e and panic-attack, then rerun PPPPP gate. |
6+
| `typed-wasm/docs/arxiv/typed-wasm.tex` | arXiv/HAL | Claims: cross-module memory safety, linearity levels; proof modules exist but not fully audited; tests/benchmarks insufficient. | Extend proofs (multi-module, lifetime/linear) and bench pipeline, rerun PPPPP. |
7+
| `vql-ut/arcvix-10-level-query-safety.tex` | HOL / Zenodo | Idris2 core proofs still labelled `needs proving`; 10-level type system lacking level-specific coverage. | Finish Idris2 proofs, add LSP/DAP/E2E tests, align PPPPP content, re-run audit. |
8+
| `stapeln/arcvix-logic-driven-container-security.tex` | HOL / Zenodo | Accessibility audit present; release tagging depends on bigger proofs/tests in other repos. | Highlight PPPPP pipeline outputs and cite `ACCESSIBILITY-AUDIT-2026-03-29`; ensure contractiles logged. |
9+
| `wokelang/arxiv-consent-aware-programming.tex` | arXiv | Release pending once VQL-UT proofs settle (shared infrastructure). | Wait for VQL-UT to hit beta stable; then confirm docs reference the final PPPPP evidence. |
10+
| Additional candidates (`verisimdb/WHITEPAPER.md`, `valence-shell/arcvix-formally-verified-reversible-shell.tex`, `ephapax/arcvix-code-as-matter.tex`) | HAL / Zenodo | Varies; mostly behind standard release gating (proof/test/bench). | Collect PPPPP evidence, ensure `PAPER-STATUS` updated before submission. |
11+
12+
## Action items
13+
- No publication (paper, blog, release note) is allowed until the PPPPP pipeline in `AUDIT-V2.adoc` is green.
14+
- When a paper cites LLM assistance, attach the mechanised proof logs as required by `LLM-PROOF-TRUST.md`.
15+
- Mark any paper that still describes conjectures as “DRAFT” and keep it in the special backlog until the proof/test audits are complete.

‎docs/audits/2026-03-30/PROOF-AUDIT-SUMMARY.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
# PROOF-AUDIT-SUMMARY — 2026-03-30
2+
3+
## Emergency tranche (still blocking any release/publication)
4+
- **007-lang**: Type soundness progress/preservation, Harvard separation without `believe_me`, session duality, linear resource safety, budget monotonicity, actor isolation, and the Elixir codegen bisimulation theorem all still live in `PROOF-NEEDS.md` (Idris2/Lean4 primary). None of these have machine-checked replacements yet, so the compound “Proven” pillar in the PPPPP gate is incomplete.
5+
- **typed-wasm**: Multi-module safety, lifetime/region interaction, tropical type semantics, and linear consumption proofs are flagged as “needs finishing” inside `PROOF-NEEDS.md`; the repo already has 11 Idris2 modules, but they need completion and CI proof logs before any claim about memory safety can stand.
6+
- **vql-ut**: The Idris2 core (Checker, Grammar, Levels, Schema) needs total verifier proofs, and the ReScript bridge must be formally linked to the Idris2 semantics; the `PROOF-NEEDS` page calls these “high priority.”
7+
- **patch-bridge**: ABI folder is empty; CVE classification, reachability, registry lookup, and patch decision gate proofs still await Idris2 definitions.
8+
9+
## Pillars to shore up next
10+
- **panic-attacker**, **verisimdb**, **echidna**, **hypatia**, **absolute-zero**, **januskey**, **panll**, etc. — each repo needs contractile-triggered proofs (k9 + intent) before we can bump the CRG grade. Continue to feed their proof debt into `CLAUDE-WORK.md`.
11+
12+
## Action items
13+
- Ensure every proof release includes the command + tool version that generated it (Idris2/Lean4/Agda logs) so we can cite the “LLM Proof Trust Statement.”
14+
- Keep `PROOF-NEEDS.md` up to date when we replace `believe_me`/`postulate` with real proofs.
15+
- When a proof is complete, log it in the PPPPP pipeline (per `AUDIT-V2.adoc`) before touching `PAPER-STATUS`.

‎docs/audits/2026-03-30/STATISTEASE-PLAN.md‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
# STATISTEASE-PLAN — 2026-03-30
2+
3+
## Mission
4+
Ensure StatistEase (the data analysis / diagnostics stack) meets the new PPPPP gate before any downstream release/paper, with full proofs/tests/contractiles/ability coverage plus the necessary HOL/HAL evidence.
5+
6+
## Key lines of work
7+
1. **Proofs**: Identify the mathematical claims within StatistEase papers or docs that require Idris2/Lean4/Agda mechanisation; add them to the `PROOF-NEEDS` ledger and schedule totality checks.
8+
2. **Tests & Benches**: Run point-to-point tests (parsing, pipeline, statistics engine), e2e flows, panic-attack/Hypatia scans, and authenticity benches (heavy datasets). Replace any placeholder fuzz entries with real harnesses.
9+
3. **Contractiles & Ability**: Document the invariants (must, trust, dust, intent) inside `contractiles/` and ensure the ability/access doc is live for dataset pipelines; tie the logs into `k9`.
10+
4. **Publication Readiness**: Connect StatistEase outputs to `PAPER-STATUS.md` + `LLM-PROOF-TRUST.md` + `AUDIT-V2.adoc`. Do not call anything “beta stable” until the entire PPPPP pipeline (proofs, tests, benches, contractiles, ability/access review) is satisfied.
11+
12+
## Coordination
13+
- Report progress in the desktop `chatgpt work` ledger and update `CLAUDE-WORK.md` for proof-heavy edits.
14+
- Keep the ability/access doc and the `stapeln/ACCESSIBILITY.md` reference alive as the Statement for high-visibility releases.
15+
- Invite peers (HOL, Zenodo, security community) to review this plan and propose additional audit steps when they challenge a claim.

‎docs/audits/2026-03-30/TEST-AUDIT-SUMMARY.md‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
# TEST-AUDIT-SUMMARY — 2026-03-30
2+
3+
## Emergency tranche (blocking the PPPPP gate)
4+
- **007-lang** (`TEST-NEEDS.md`): 728 unit tests mostly cover parser/evaluator; zero P2P tests for modules like codegen, optimizer, JIT, module system, etc.; no E2E pipeline, no panic-attack/Hypatia runs, no benchmarks covering multi-module or JIT performance, no `panic-attack assail`, and no accessible self-tests.
5+
- **typed-wasm**: Only one parser unit test (`ParserTests.res`), a 43-assertion smoke E2E, and a placeholder fuzz file labelled as fake — still no benchmarks, no coverage for the 10-level type system, no multi-module linking test, and no security/performance aspects.
6+
- **vql-ut**: 49 unit tests for 27 modules; zero E2E workflows (parse→typecheck→execute), zero LSP/DAP/formatter integration, no concurrency/error handling/bench aspect tests, and the same fake fuzz placeholder.
7+
- **patch-bridge**: ~14 inline tests, zero E2E/cross-format lockfile multi-stage pipelines, no benchmarks, no panic-attack/Hypatia, no security/performance/execution tests, and the placeholder fuzz file flagged as “fake.”
8+
9+
## Next tier (paper-worthy) tests
10+
- Pillar repos (panic-attacker, verisimdb, echidna, hypatia, etc.) must each run aspect tests (security, performance, concurrency, accessibility) plus the release-level benchmarks described in their `TEST-NEEDS` page before being allowed to claim B-level maturity.
11+
- `statist ease` (once located) needs its own test plan; use `STATISTEASE-PLAN.md` to map the bench/analysis matrix once the document is available.
12+
13+
## Action items
14+
- Add panic-attack/Hypatia/bench logs to the PPPPP pipeline for each release candidate before upgrading the CRG grade.
15+
- Replace any `tests/fuzz/placeholder.txt` with real harnesses or delete the files to avoid fake coverage.
16+
- Each repo flagged as “beta unstable” must still have an accessible regression suite before it graduates to “beta stable.”

‎docs/audits/2026-03-30/nuj-prc-email-redirects.md‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,46 @@
1+
# NUJ-PRC Email Redirects
2+
3+
Incoming redirects only.
4+
5+
## Alias Normalization Rule
6+
7+
- If an alias starts with `branch-` or `council-`, replace only that first hyphen with `_`.
8+
- Keep internal role hyphens such as `vice-chair`, `assistant-secretary`, and `deputy-chair`.
9+
10+
## Redirects
11+
12+
| Branch Email | Redirects To | Notes |
13+
|--------------|--------------|-------|
14+
| general@nuj-prc.org.uk | jonathan.jewell@gmail.com, philmorcom@yahoo.com, carmelmchenry@hotmail.com, sianharrison@gmail.com | Fallback for unfilled posts; goes to chair, vice-chair, and secretary |
15+
| committee@nuj-prc.org.uk | council_chair@nuj-prc.org.uk, council_vice-chair@nuj-prc.org.uk, council_treasurer@nuj-prc.org.uk, council_deputy-treasurer@nuj-prc.org.uk, council_secretary@nuj-prc.org.uk, council_assistant-secretary@nuj-prc.org.uk, council_equalities@nuj-prc.org.uk, council_welfare@nuj-prc.org.uk, council_safety@nuj-prc.org.uk, council_membership@nuj-prc.org.uk, branch_chair@nuj-prc.org.uk, branch_vice-chair@nuj-prc.org.uk, branch_treasurer@nuj-prc.org.uk, branch_deputy-treasurer@nuj-prc.org.uk, branch_secretary@nuj-prc.org.uk, branch_assistant-secretary@nuj-prc.org.uk, branch_equalities@nuj-prc.org.uk, branch_welfare@nuj-prc.org.uk, branch_safety@nuj-prc.org.uk, branch_training@nuj-prc.org.uk, branch_membership@nuj-prc.org.uk, training@nuj-prc.org.uk | Internal mailing list to all current PRC post aliases |
16+
| council_committee@nuj-prc.org.uk | council_chair@nuj-prc.org.uk, council_vice-chair@nuj-prc.org.uk, council_treasurer@nuj-prc.org.uk, council_deputy-treasurer@nuj-prc.org.uk, council_secretary@nuj-prc.org.uk, council_assistant-secretary@nuj-prc.org.uk, council_equalities@nuj-prc.org.uk, council_welfare@nuj-prc.org.uk, council_safety@nuj-prc.org.uk, council_membership@nuj-prc.org.uk | Internal mailing list to all current PRC council post aliases |
17+
| branch_committee@nuj-prc.org.uk | branch_chair@nuj-prc.org.uk, branch_vice-chair@nuj-prc.org.uk, branch_treasurer@nuj-prc.org.uk, branch_deputy-treasurer@nuj-prc.org.uk, branch_secretary@nuj-prc.org.uk, branch_assistant-secretary@nuj-prc.org.uk, branch_equalities@nuj-prc.org.uk, branch_welfare@nuj-prc.org.uk, branch_safety@nuj-prc.org.uk, branch_training@nuj-prc.org.uk, branch_membership@nuj-prc.org.uk | Internal mailing list to all current PRC branch post aliases |
18+
| training@nuj-prc.org.uk | carmelmchenry@hotmail.com, jonathan.jewell@gmail.com | Senior unionwide training seat; Carmel and Jonathan |
19+
| council_chair@nuj-prc.org.uk | jonathan.jewell@gmail.com | Jonathan |
20+
| council_vice-chair@nuj-prc.org.uk | philmorcom@yahoo.com, carmelmchenry@hotmail.com | Phil Morcom and Carmel |
21+
| council_treasurer@nuj-prc.org.uk | natasha.hirst@gmail.com | Natasha Hirst |
22+
| council_deputy-treasurer@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
23+
| council_secretary@nuj-prc.org.uk | sianharrison@gmail.com | Sian Harrison |
24+
| council_assistant-secretary@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
25+
| council_equalities@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
26+
| council_welfare@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
27+
| council_safety@nuj-prc.org.uk | jonathan.jewell@gmail.com | Jonathan |
28+
| council_membership@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
29+
| nec@nuj-prc.org.uk | jonathan.jewell@gmail.com | Jonathan |
30+
| safety@nuj-prc.org.uk | jonathan.jewell@gmail.com | Jonathan |
31+
| ethics@nuj-prc.org.uk | jonathan.jewell@gmail.com | Jonathan |
32+
| branch_chair@nuj-prc.org.uk | carmelmchenry@hotmail.com | Carmel |
33+
| branch_vice-chair@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
34+
| branch_treasurer@nuj-prc.org.uk | natasha.hirst@gmail.com | Natasha Hirst |
35+
| branch_deputy-treasurer@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
36+
| branch_secretary@nuj-prc.org.uk | sianharrison@gmail.com | Sian Harrison |
37+
| branch_assistant-secretary@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
38+
| branch_equalities@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
39+
| branch_welfare@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
40+
| branch_safety@nuj-prc.org.uk | jonathan.jewell@gmail.com | Jonathan |
41+
| branch_training@nuj-prc.org.uk | carmelmchenry@hotmail.com | Branch training seat; Carmel |
42+
| branch_membership@nuj-prc.org.uk | general@nuj-prc.org.uk | Unfilled; routes to general |
43+
| servicing@nuj-prc.org.uk | andys@nuj.org.uk | Andy Smith |
44+
| jeab@nuj-prc.org.uk | sianharrison@gmail.com | Sian Harrison |
45+
| editor@nuj-prc.org.uk | sanajanjuais@hotmail.com | Sana |
46+
| disability@nuj-prc.org.uk | anngalpin@gmail.com | Ann Galpin |

0 commit comments

Comments
 (0)