Elevate KitchenSpeak toward standalone repo; commence proofs-first work#63
Merged
Merged
Conversation
Prepare KitchenSpeak's elevation from an in-tree directory to its own canonical repository (matching every sibling language), list it as a DSL in the monorepo README/EXPLAINME, and commence the roadmap to bring it to AffineScript-level toolchain parity — leading with proofs. Standalone-repo scaffolding under kitchenspeak/: - README.adoc (standalone), LICENSE (Palimpsest/MPL-2.0), .gitignore, CHANGELOG.adoc - ROADMAP.adoc: proofs-first plan to AffineScript parity, with a per-axis parity scorecard - decisions/0002: ADR recording the elevation Proofs commenced (Phase 1): - proofs/agda/PoachedEgg.agda: lowers examples/poached-egg.ks; discharges termination, on_fail totality, echo-witness extraction, and the first Tropical refinement (no-binary-overheat envelope). Linear + Tropical + Echo - proofs/Makefile + proofs/agda/kitchenspeak.agda-lib: proof build harness (make -C proofs) Monorepo: - README.adoc, EXPLAINME.adoc: KitchenSpeak listed as an experimental DSL - scripts/elevate-kitchenspeak.sh: runnable final elevation step (create repo + git subtree split + convert to submodule). Split out because repo creation needs permissions/network this session lacked.
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
| @@ -0,0 +1,382 @@ | |||
| -- SPDX-License-Identifier: MPL-2.0 | |||
🔍 Hypatia Security ScanFindings: 61 issues detected
View findings[
{
"reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "codeql.yml lists `language: javascript-typescript` but the repo has no source files in any CodeQL-scannable language. The analyze job will exit 'no source files' on every run. Switch the matrix to `actions` (which scans workflow files — every repo has those).",
"type": "codeql_language_matrix_mismatch",
"file": "codeql.yml",
"action": "switch_codeql_matrix_to_actions",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in boj-build.yml",
"type": "missing_timeout_minutes",
"file": "boj-build.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
…se policy) Annotate every Agda postulate with a leading AXIOM: comment and enumerate them in PROOF-NEEDS.md, satisfying the trusted-base reduction policy. These postulates are deliberate trust boundaries (postulated sensor oracles + the GENTLE controller spec), not undocumented escape hatches.
Owner
Author
CI triageSorting the failures into "caused by this PR" vs "pre-existing repo-wide": Fixed in this PR (
|
🔍 Hypatia Security ScanFindings: 61 issues detected
View findings[
{
"reason": "Action perpolymath/standards/.github/workflows/governance-reusable.yml@main\n needs attention",
"type": "unpinned_action",
"file": "governance.yml",
"action": "pin_sha",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "codeql.yml lists `language: javascript-typescript` but the repo has no source files in any CodeQL-scannable language. The analyze job will exit 'no source files' on every run. Switch the matrix to `actions` (which scans workflow files — every repo has those).",
"type": "codeql_language_matrix_mismatch",
"file": "codeql.yml",
"action": "switch_codeql_matrix_to_actions",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in boj-build.yml",
"type": "missing_timeout_minutes",
"file": "boj-build.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in casket-pages.yml",
"type": "missing_timeout_minutes",
"file": "casket-pages.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in codeql.yml",
"type": "missing_timeout_minutes",
"file": "codeql.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in dogfood-gate.yml",
"type": "missing_timeout_minutes",
"file": "dogfood-gate.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
hyperpolymath
added a commit
that referenced
this pull request
Jun 2, 2026
Follow-up to #63, addressing the **pre-existing, repo-wide** CI failures and Hypatia workflow-audit findings (61) that were unrelated to the KitchenSpeak elevation but surfaced alongside it. Work was fanned out across the workflow files in parallel. ## Changes **`timeout-minutes` (the bulk of the `missing_timeout_minutes` findings)** — added to every real `runs-on`+`steps` job that lacked one: - `boj-build` (trigger-boj), `casket-pages` (build, deploy), `codeql` (analyze), `dogfood-gate` (5 jobs), `instant-sync` (dispatch), `scorecard-enforcer` (scorecard, check-critical), `semgrep`, `workflow-linter`. -⚠️ **Deliberately not added** to reusable-workflow *caller* jobs (`governance`, `hypatia-scan`, `mirror`, `scorecard`, `secret-scanner`) — GitHub Actions **rejects** `timeout-minutes` on a job whose body is `uses:`, so adding it there would break those workflows. Those findings are effectively false positives for caller jobs. **`codeql.yml`** — switch the analysis matrix `javascript-typescript` → `actions`. The repo has no JS/TS sources, so `analyze` failed *"no source files"* on every run; `actions` scans the workflow files every repo has. Fixes the recurring **analyze** failure. **`dependabot.yml`** — remove the spurious `nuget` ecosystem entry. The repo has zero .NET projects (verified), which is what underpins the always-failing **submit-nuget** check. Note: the `submit-nuget` *check* itself is org-level (`hyperpolymath/.github`), not defined in this repo, so this removes the local root cause but the org workflow may still need adjusting. **`instant-sync.yml`** — fix a **pre-existing YAML error**: a stray `K9-SVC Validation` step was mis-indented to `jobs:` level, making the entire workflow invalid YAML (confirmed broken on `main`, not introduced here). Re-nested it into the `dispatch` job's `steps`. Validated with PyYAML. ## Validation All 9 changed files parse cleanly (`yaml.safe_load_all`). ## Not done (needs your hands) - **One unpinned action**: `hyperpolymath/standards/.github/workflows/governance-reusable.yml@main`. I couldn't resolve its SHA from here (the `standards` repo is outside this session's API scope; the unauthenticated commits API returned 403). The `governance` check is currently green, so I left `@main` rather than guess a SHA and risk breaking it. Pin manually: ``` gh api 'repos/hyperpolymath/standards/commits?path=.github/workflows/governance-reusable.yml&sha=main&per_page=1' --jq '.[0].sha' ``` then replace `@main` with `@<sha> # main` in `governance.yml`. https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY --- _Generated by [Claude Code](https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jun 2, 2026
…iles, branch hygiene (#67) Documentation + configuration wrap-up for the KitchenSpeak / echo-types / CI-hygiene work, and the change that makes recurring CI advisories **self-handling**. Intended to **merge to main** once CI is green (per maintainer authorization). ## Documentation (highest-standards refresh) - **README.adoc** — new "Shared Formal Substrate — echo-types" section. - **EXPLAINME.adoc** — echo-types/ADR-0004 note on KitchenSpeak + new "Governance & CI Posture" section. - **6a2**: `STATE` (kitchenspeak + ci-governance), `META` (ADRs, practices, external rulesets), `ECOSYSTEM` (echo-types, EchoTypes.jl, standards, typed-wasm). `CHANGELOG.md` + `TOOLING-STATUS.adoc` refreshed. ## Hypatia / gitbot self-handling The enforcing ruleset lives in `hyperpolymath/standards` (out of scope), so the in-repo lever is a **machine-readable waiver registry**: - **`6a2/NEUROSYM.a2ml` `[waivers]`** — every recurring advisory triaged once: reusable-caller `timeout` false-positives, `governance@main` pin (track), scorecard/instant-sync detector mismatches (addressed), by-design `agda_postulate` axioms. - **`6a2/PLAYBOOK.a2ml`** — gitbot runbook (consult the registry, skip accepted findings, don't re-fix) + branch-hygiene + merge-gating. - **`6a2/AGENTIC.a2ml`** — agent CI-handling + branch-hygiene contract. ## Contractiles - **`MUST.contractile`** — project-specific invariants (proofs-first, trusted-base documentation, echo-types attachment, waiver discipline). - **`Trustfile`** — branch-hygiene reconciliation: deleting **merged** PR branches is now permitted; force-push / CI-secret modification / publish remain denied. ## Also done outside this PR - The four merged feature branches (#63–#66) were deleted (they were already auto-removed on merge; local refs pruned). ## Validation - All six `6a2/*.a2ml` parse as valid TOML; `MUST.contractile` s-expr paren-balanced; SPDX headers intact on all changed files (README has none on `main` either — docs exempt). ## Honest limitation Hypatia's enforcing ruleset is external; this PR records the accepted findings repo-side so agents stop re-litigating them, but **full auto-suppression of the addressed/false-positive items needs a one-time `standards`-side change** — tracked in each waiver's `action`. https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY --- _Generated by [Claude Code](https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY)_ Co-authored-by: Claude <noreply@anthropic.com>
2 tasks
hyperpolymath
added a commit
that referenced
this pull request
Jun 2, 2026
) ## Summary - **`LANGUAGES.a2ml`**: First structured `[languages.kitchenspeak]` TOML entry — name, kind, phase, all 7 types, Agda-Proven invariant, ADRs 0001–0004, echo-attachment strategy (B-now/C-later/A-shim per ADR 0004), standalone-repo status. Updates `last-updated` to 2026-06-02. - **`contractiles/intend/Intentfile.a2ml`**: Language-family table enumerates all DSLs the repo coordinates; KitchenSpeak marked as the only member with active Agda proof work (the Agda-Proven invariant). - **`contractiles/must/Mustfile.a2ml`**: New `[KitchenSpeak]` section with five executable invariants that machine-check the Agda-Proven invariant: proofs dir present, echo-types dep declared, `-- AXIOM:` annotation on all postulates, `PROOF-NEEDS.md` present, ADR 0004 present. This is the final documentation gap from the KitchenSpeak elevation work (PRs #63–#67). All CI should be green; this is documentation-only. ## Test plan - [ ] CI / K9 gate passes (TOML valid, no structural changes to existing gates) - [ ] `contractiles/must/Mustfile.a2ml` invariants evaluate correctly against the current repo state: - `test -d kitchenspeak/proofs/agda` ✓ - `grep -q 'echo-types' kitchenspeak/proofs/agda/kitchenspeak.agda-lib` ✓ - `test -f kitchenspeak/proofs/PROOF-NEEDS.md` ✓ - `test -f kitchenspeak/decisions/0004-echo-attaches-to-linear-dyadic.adoc` ✓ https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY --- _Generated by [Claude Code](https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY)_ Co-authored-by: Claude <noreply@anthropic.com>
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
3 participants
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.
What this does
Prepares KitchenSpeak's elevation from an in-tree directory to its own canonical repository (matching every sibling language), lists it as a DSL in the monorepo
README.adocandEXPLAINME.adoc, examines where AffineScript is up to, and commences the development work to bring KitchenSpeak to AffineScript's position — leading, deliberately, with proofs.Where AffineScript is (the target)
The standalone
hyperpolymath/affinescriptrepo is outside this session's GitHub scope, so its position is taken from the monorepo's own authoritative docs (EXPLAINME.adoc§Claim 1,TOOLING-STATUS.adoc,PROOF-NEEDS.md):affine-lsp/affine-dap(Rust), linter, formatter (stub), tree-sitter, doc-gen, pkg-mgr, conformance ✓src/abi/, Idris2 + Zig) in progress; targets WasmGCARG-D,FRG-E,RSR FULLformal/dirThat gap is exactly why KitchenSpeak (identity: Agda-Proven) leads with proofs: it honours the language's invariant and overtakes the target on the axis that matters most for a safety DSL.
Changes
New standalone-repo content under
kitchenspeak/(moves with the directory when elevated):README.adoc(standalone),LICENSE(Palimpsest/MPL-2.0),.gitignore,CHANGELOG.adocROADMAP.adoc— proofs-first, 8-phase plan to AffineScript parity, with a per-axis parity scorecarddecisions/0002-elevation-to-standalone-repo.adoc— ADR for the elevationProofs commenced (ROADMAP Phase 1):
proofs/agda/PoachedEgg.agda— lowersexamples/poached-egg.ks; discharges termination,on_failtotality (ABORT + RECOVER), echo-witness extraction for bothsyncblocks, and the first Tropical refinement (the GENTLE controller never crosses the boil envelope). Linear + Tropical + Echo.proofs/Makefile+proofs/agda/kitchenspeak.agda-lib— proof build harness (make -C proofs)Monorepo:
README.adoc,EXPLAINME.adoc— KitchenSpeak listed as an experimental DSL in the project list / language tables / file mapI could not finish the literal "create
hyperpolymath/kitchenspeak+ flip to submodule" step from here: the GitHub App backing this session is not permitted to create repositories (POST /user/repos → 403 Resource not accessible by integration). Rather than leave the monorepo pointing at a submodule that doesn't exist, I kept the content in-tree (so the repo stays valid and the proofs are reviewable) and provided the mechanical finisher:It creates the public repo, preserves history via
git subtree split, pushes, then convertskitchenspeak/into a submodule and commits. Run it locally (or anywhere withgh+ repo-create rights). ADR 0002's status documents this precisely.Proof caveat
Agda isn't installed in this environment, so
PoachedEgg.agdais hand-verified, not yet machine-checked — the same standard the existingDough.agdais held to (seeproofs/README.adoc). ROADMAP Phase 1a adds Agda to CI somake -C proofsruns on every push.Test plan
./scripts/elevate-kitchenspeak.sh(needsgh+ repo-create permission)make -C proofs(needs Agda 2.6.4+ / stdlib 2.0+) → zero unsolved goalshttps://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY
Generated by Claude Code