docs: register KitchenSpeak in LANGUAGES.a2ml, Intentfile, Mustfile#68
Merged
Merged
Conversation
LANGUAGES.a2ml gains the first structured [languages.kitchenspeak] TOML entry — name, kind, phase, 7 types, Agda-Proven invariant, ADRs, echo- attachment strategy (B-now/C-later/A-shim), and standalone-repo status. Intentfile.a2ml gains a language-family table so the repo's purpose statement enumerates the DSLs it coordinates, with KitchenSpeak marked as the only member with active Agda proof work. Mustfile.a2ml gains a [KitchenSpeak] section with five executable invariants: proofs directory present, echo-types dep declared, all postulates annotated -- AXIOM:, PROOF-NEEDS.md present, ADR 0004 present. These machine-check the Agda-Proven invariant on every run. https://claude.ai/code/session_01RZWK1vf9QfP2H2JTFWCdJY
🔍 Hypatia Security ScanFindings: 30 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": "Issue in governance.yml",
"type": "missing_timeout_minutes",
"file": "governance.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in hypatia-scan.yml",
"type": "missing_timeout_minutes",
"file": "hypatia-scan.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in mirror.yml",
"type": "missing_timeout_minutes",
"file": "mirror.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard.yml",
"type": "missing_timeout_minutes",
"file": "scorecard.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in secret-scanner.yml",
"type": "missing_timeout_minutes",
"file": "secret-scanner.yml",
"action": "flag",
"rule_module": "workflow_audit",
"severity": "medium"
},
{
"reason": "Issue in scorecard-enforcer.yml",
"type": "scorecard_publish_with_run_step",
"file": "scorecard-enforcer.yml",
"action": "split_scorecard_publish_job",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Issue in instant-sync.yml",
"type": "secret_action_without_presence_gate",
"file": "instant-sync.yml",
"action": "peter-evans/repository-dispatch",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (2 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/nextgen-languages/nextgen-languages/kitchenspeak/proofs/agda/PoachedEgg.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/nextgen-languages/nextgen-languages/kitchenspeak/proofs/agda/Dough.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
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.
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. Updateslast-updatedto 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.mdpresent, 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
contractiles/must/Mustfile.a2mlinvariants 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