From 22efb3e580bcc7856b344618840ac2f0b5b8b25b Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 5 Jun 2026 14:02:59 +0000 Subject: [PATCH] =?UTF-8?q?chore(machine-readable):=20currency=20checkpoin?= =?UTF-8?q?t=20=E2=80=94=20bot=5Fdirectives=20rename,=20contractile=20de-r?= =?UTF-8?q?ot,=20svc/k9=20fill?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - rename agent_instructions/ -> bot_directives/ (methodology layer); fix doc refs - rewrite must/dust/adjust xfiles from wholesale Burble copies into real ephapax contracts (Rust workspace + Coq/Idris metatheory). Adds an ephapax-specific invariant: legacy `Theorem preservation` in Semantics.v MUST stay Admitted (owner directive 2026-05-27 — it is provably false; Counterexample.v depends on it) - fill svc/k9 trust-tier templates + README; add contractiles/k9 (resolves the adjust/intend k9 imports) - validated: all pure .ncl nickel-typecheck clean; critical must probes pass when run Signed-off-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> --- .../README.adoc | 14 +- .../coverage.a2ml | 0 .../debt.a2ml | 0 .../lessons.a2ml | 0 .../methodology.a2ml | 0 .../contractiles/adjust/Adjustfile.a2ml | 222 +++--------------- .../contractiles/dust/Dustfile.a2ml | 71 ++---- .../contractiles/k9/template-hunt.k9.ncl | 136 +++++++++++ .../contractiles/k9/template-kennel.k9.ncl | 54 +++++ .../contractiles/k9/template-yard.k9.ncl | 84 +++++++ .../contractiles/must/Mustfile.a2ml | 134 ++++++----- .machine_readable/svc/k9/README.adoc | 178 ++++++++++++++ .machine_readable/svc/k9/template-hunt.k9.ncl | 136 +++++++++++ .../svc/k9/template-kennel.k9.ncl | 54 +++++ .machine_readable/svc/k9/template-yard.k9.ncl | 84 +++++++ ...-2026-05-20-proof-engineering-lessons.adoc | 2 +- 16 files changed, 864 insertions(+), 305 deletions(-) rename .machine_readable/{agent_instructions => bot_directives}/README.adoc (62%) rename .machine_readable/{agent_instructions => bot_directives}/coverage.a2ml (100%) rename .machine_readable/{agent_instructions => bot_directives}/debt.a2ml (100%) rename .machine_readable/{agent_instructions => bot_directives}/lessons.a2ml (100%) rename .machine_readable/{agent_instructions => bot_directives}/methodology.a2ml (100%) create mode 100644 .machine_readable/contractiles/k9/template-hunt.k9.ncl create mode 100644 .machine_readable/contractiles/k9/template-kennel.k9.ncl create mode 100644 .machine_readable/contractiles/k9/template-yard.k9.ncl create mode 100644 .machine_readable/svc/k9/README.adoc create mode 100644 .machine_readable/svc/k9/template-hunt.k9.ncl create mode 100644 .machine_readable/svc/k9/template-kennel.k9.ncl create mode 100644 .machine_readable/svc/k9/template-yard.k9.ncl diff --git a/.machine_readable/agent_instructions/README.adoc b/.machine_readable/bot_directives/README.adoc similarity index 62% rename from .machine_readable/agent_instructions/README.adoc rename to .machine_readable/bot_directives/README.adoc index 9bc2e24b..4526792b 100644 --- a/.machine_readable/agent_instructions/README.adoc +++ b/.machine_readable/bot_directives/README.adoc @@ -1,10 +1,14 @@ // SPDX-License-Identifier: MPL-2.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= Agent Instructions += Bot Directives :toc: preamble -Methodology-aware configuration for AI agents. Read by any AI agent -(Claude, Gemini, Copilot, etc.) at session start. +Methodology-aware configuration for AI agents and bots. Read by any AI +agent (Claude, Gemini, Copilot, etc.) or estate bot at session start. + +NOTE: This directory was renamed `agent_instructions/` -> `bot_directives/` +to align with the estate-wide naming convention. Contents (methodology, +coverage, debt, lessons) are unchanged. == Files @@ -32,8 +36,8 @@ Methodology-aware configuration for AI agents. Read by any AI agent == Relationship to Other Files * `AGENTIC.a2ml` says WHAT agents can do (permissions, gating) -* `agent_instructions/` says HOW agents should work (methodology) -* `bot_directives/` says what the gitbot-fleet does (fleet-specific) +* This directory (`bot_directives/`) says HOW agents should work — methodology, coverage, debt (the renamed methodology layer) +* Per-bot fleet directives (hypatia, gitbot-fleet, .git-private-farm) are not yet populated — they will be added here as named files (deferred; see issue) * `CLAUDE.md` says how Claude specifically should work (Claude-specific) == Reference diff --git a/.machine_readable/agent_instructions/coverage.a2ml b/.machine_readable/bot_directives/coverage.a2ml similarity index 100% rename from .machine_readable/agent_instructions/coverage.a2ml rename to .machine_readable/bot_directives/coverage.a2ml diff --git a/.machine_readable/agent_instructions/debt.a2ml b/.machine_readable/bot_directives/debt.a2ml similarity index 100% rename from .machine_readable/agent_instructions/debt.a2ml rename to .machine_readable/bot_directives/debt.a2ml diff --git a/.machine_readable/agent_instructions/lessons.a2ml b/.machine_readable/bot_directives/lessons.a2ml similarity index 100% rename from .machine_readable/agent_instructions/lessons.a2ml rename to .machine_readable/bot_directives/lessons.a2ml diff --git a/.machine_readable/agent_instructions/methodology.a2ml b/.machine_readable/bot_directives/methodology.a2ml similarity index 100% rename from .machine_readable/agent_instructions/methodology.a2ml rename to .machine_readable/bot_directives/methodology.a2ml diff --git a/.machine_readable/contractiles/adjust/Adjustfile.a2ml b/.machine_readable/contractiles/adjust/Adjustfile.a2ml index 24f400fd..f1ac0470 100644 --- a/.machine_readable/contractiles/adjust/Adjustfile.a2ml +++ b/.machine_readable/contractiles/adjust/Adjustfile.a2ml @@ -1,211 +1,55 @@ # SPDX-License-Identifier: MPL-2.0 -# Adjustfile — Accessibility Contract for Burble +# Adjustfile — Accessibility / drift-tolerance contract for Ephapax # Author: Jonathan D.A. Jewell # -# Accessibility requirements and compliance for Burble. -# Voice-first design must be inclusive for all users. -# # Run with: adjust check # Fix with: adjust fix (where deterministic fix exists) @abstract: -Accessibility requirements and compliance for the Burble voice-first communications platform. -These requirements ensure Burble is usable by everyone, regardless of ability. +Ephapax is a language toolchain (Rust compiler + mechanised metatheory), not a +GUI application — so conventional WCAG *UI* accessibility largely does not apply. +This contract deliberately scopes "accessibility" to the surfaces ephapax does +expose to humans: compiler diagnostics, documentation, and CLI ergonomics. +Advisory (continue-with-warnings), not a hard gate. @end -## Keyboard Accessibility +## Documentation Accessibility -### keyboard-navigation -- description: All features accessible via keyboard +### docs-semantic-asciidoc +- description: Documentation uses semantic AsciiDoc (heading order, image alt text) for screen-reader/navigation friendliness - status: partial -- probe: test -f server/lib/burble/accessibility/keyboard.ex -- compliance: WCAG 2.1 AA -- notes: Basic navigation implemented. Full keyboard-only flow needed. -- fix: Port PanLL's comprehensive keyboard navigation system - -### custom-keybindings -- description: User-configurable keybindings -- status: implemented -- probe: test -f server/lib/burble/accessibility/keyboard.ex -- compliance: WCAG 2.1 AAA -- notes: Users can remap PTT, mute, deafen, volume, and room navigation keys - -### keyboard-shortcuts-discoverable -- description: Keyboard shortcuts are documented and discoverable -- status: missing -- compliance: WCAG 2.1 A -- fix: Add keyboard shortcuts help modal in web client - -## Visual Accessibility - -### high-contrast-mode -- description: High contrast UI theme -- status: missing -- compliance: WCAG 2.1 AA -- fix: Port PanLL's high-contrast theme system -- target: CSS variables for contrast ratios >= 4.5:1 - -### colorblind-support -- description: Colorblind-friendly color schemes -- status: missing -- compliance: WCAG 2.1 AA -- fix: Implement deuteranopia, protanopia, and tritanopia palettes -- reference: PanLL's palette system - -### font-size-adjustment -- description: Resizable UI fonts (4 levels: 14-20px) -- status: missing -- compliance: WCAG 2.1 AA -- fix: Port PanLL's font size adjustment system -- target: User preference persists across sessions - -### theme-switching -- description: Dark/Light/System theme support -- status: missing -- compliance: WCAG 2.1 AA -- fix: Port PanLL's theme system -- target: Respects OS preference, user override +- compliance: WCAG 2.1 AA (documents) +- notes: docs/ is AsciiDoc; audit for alt text and heading order. -## Auditory Accessibility - -### screen-reader-support -- description: Full screen reader compatibility +### readme-plain-language-summary +- description: README opens with a plain-language summary before substructural-logic notation - status: partial -- probe: test -f server/lib/burble/accessibility/screen_reader.ex -- compliance: WCAG 2.1 AA -- notes: Basic announcements implemented. Needs ARIA attributes and live regions. -- fix: Complete ARIA implementation in web client - -### closed-captions -- description: Real-time captioning for voice chat -- status: missing -- compliance: WCAG 2.1 AA -- notes: Requires Web Speech API or external STT integration -- target: 90%+ accuracy for English, configurable display - -### visual-notifications -- description: Visual indicators for audio events -- status: missing -- compliance: WCAG 2.1 A -- notes: Speaking indicators, mute status, connection status -- fix: Add visual cues that duplicate audio information - -### volume-normalization -- description: Consistent volume levels across users -- status: missing -- compliance: WCAG 2.1 AA -- notes: Prevents sudden loud sounds for sensitive users -- target: -23 LUFS normalization per EBU R128 +- notes: Linear/affine notation should be preceded by prose intent for non-specialist readers. -## Motor Accessibility +## Diagnostic Clarity (compiler accessibility) -### voice-commands -- description: Voice-controlled interface -- status: missing -- compliance: WCAG 2.1 AAA -- notes: "Mute", "Deafen", "Join room X", "Volume up/down" -- target: Web Speech API with fallback to keyboard - -### reduced-motion -- description: Reduced animation options -- status: missing -- compliance: WCAG 2.1 AA -- fix: Port PanLL's animation control (on/reduced/off) -- target: Respects prefers-reduced-motion media query - -### hover-alternatives -- description: All hover interactions have click alternatives +### error-messages-actionable +- description: Type/borrow errors name the offending region/modality and suggest a remedy - status: partial -- compliance: WCAG 2.1 AA -- notes: Some hover tooltips need click-to-show option -- fix: Audit and add click alternatives +- notes: Four-layer (L1–L4) errors should state in plain terms which layer failed (region capability / modality / echo residue / dyadic mode). -## Cognitive Accessibility +### no-bare-panic-diagnostics +- description: User-facing failures are structured diagnostics, not raw Rust panics +- status: declared +- probe: test -d src/ephapax-typing +- notes: Track panics reaching the CLI surface; convert to diagnostics. -### clear-language -- description: Simple, consistent terminology -- status: partial -- compliance: WCAG 2.1 AAA -- notes: Technical terms need plain language explanations -- fix: Add tooltips/glossary for jargon +## CLI Ergonomics -### predictable-navigation -- description: Consistent navigation patterns -- status: partial -- compliance: WCAG 2.1 AA -- notes: Navigation structure varies between pages -- fix: Standardize navigation layout +### cli-help-available +- description: The ephapax CLI exposes --help with usage +- status: declared +- notes: Verified in CI via `ephapax --help`; crate-presence proxy here. -### error-prevention -- description: Confirmation for destructive actions -- status: partial -- compliance: WCAG 2.1 AA -- notes: Room deletion has confirmation, others may not -- fix: Audit all destructive actions - -### help-availability -- description: Context-sensitive help always available -- status: missing -- compliance: WCAG 2.1 AAA -- notes: No persistent help system -- fix: Add help button with contextual guidance - -## Compliance Targets - -### wcag-2.1-aa -- description: WCAG 2.1 AA compliance -- status: partial -- target: Full compliance by Q4 2026 -- tracking: https://github.com/hyperpolymath/burble/issues/XXX - -### section-508 -- description: U.S. Section 508 compliance -- status: partial -- target: Full compliance by Q4 2026 -- notes: Aligns with WCAG 2.1 AA for most requirements +## Compliance Posture -### en-301-549 -- description: EU EN 301 549 compliance +### wcag-scope-statement +- description: Accessibility scope (docs + diagnostics, not GUI) is documented so "N/A" never drifts silently - status: partial -- target: Full compliance by Q4 2026 -- notes: EU public sector procurement requirement - -## Integration Requirements - -### panll-accessibility-port -- description: Port PanLL's accessibility engine to Burble -- status: planned -- reference: /var/mnt/eclipse/repos/panll/tests/accessibility_engine_test.js -- target: Q2 2026 - -### k9-accessibility-validator -- description: Integrate K9 accessibility validator -- status: planned -- reference: /var/mnt/eclipse/repos/panll/contractiles/k9/validators/accessibility-baseline.k9.ncl -- target: Q2 2026 - -### accessibility-testing -- description: Add accessibility tests to CI/CD -- status: planned -- target: pa11y or axe-core integration -- compliance: Automated WCAG testing - -## Documentation Requirements - -### accessibility-guide -- description: User-facing accessibility guide -- status: missing -- target: docs/accessibility/USER-GUIDE.adoc -- notes: Keyboard shortcuts, screen reader setup, theme switching - -### developer-accessibility -- description: Developer accessibility guidelines -- status: missing -- target: docs/accessibility/DEVELOPER.adoc -- notes: Coding standards, testing requirements, compliance checklist - -### compliance-report -- description: Accessibility compliance report -- status: missing -- target: docs/compliance/ACCESSIBILITY.adoc -- notes: VPAT (Voluntary Product Accessibility Template) +- target: docs/accessibility/SCOPE.adoc +- notes: A compiler core has no GUI surface; an explicit scope statement prevents false-N/A drift. diff --git a/.machine_readable/contractiles/dust/Dustfile.a2ml b/.machine_readable/contractiles/dust/Dustfile.a2ml index 40c84829..633ebdb2 100644 --- a/.machine_readable/contractiles/dust/Dustfile.a2ml +++ b/.machine_readable/contractiles/dust/Dustfile.a2ml @@ -1,5 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 -# Dustfile — Cleanup and hygiene contract for Burble +# Dustfile — Cleanup and hygiene contract for Ephapax # Author: Jonathan D.A. Jewell # # What should be cleaned up. Housekeeping, not blockers. @@ -7,8 +7,9 @@ # Roll back with: dust rollback @abstract: -Cleanup and hygiene items for the Burble voice platform. -These are maintenance tasks — not blocking, but should be addressed. +Cleanup and hygiene items for Ephapax. Maintenance tasks — not blocking, but +should be addressed. Destructive actions are dry-run by default and gated +behind --apply with per-item approval. @end ## Stale Files @@ -19,60 +20,40 @@ These are maintenance tasks — not blocking, but should be addressed. - severity: info ### no-ai-djot -- description: AI.djot is superseded by 0-AI-MANIFEST.a2ml +- description: AI.djot superseded by 0-AI-MANIFEST.a2ml - run: test ! -f AI.djot - severity: warning -### no-next-steps -- description: NEXT_STEPS.md superseded by ROADMAP -- run: test ! -f NEXT_STEPS.md -- severity: info +### no-lust-dir +- description: The lust/ contractile verb was removed estate-wide 2026-04-18 (semantics absorbed into intend) +- run: test ! -d .machine_readable/contractiles/lust +- severity: warning +- notes: Any lust/ dir is drift; horizon/aspiration semantics live in intend now. ## Build Artifacts -### no-tracked-elixir-build -- description: No Elixir build artifacts tracked in git -- run: test -z "$(git ls-files server/_build/ server/deps/ 2>/dev/null)" -- severity: warning - -### no-tracked-rescript-build -- description: No ReScript build artifacts tracked in git -- run: test -z "$(git ls-files 'client/web/src/**/*.res.mjs' client/web/lib/ 2>/dev/null)" +### no-tracked-rust-build +- description: No Rust build artifacts tracked in git +- run: test -z "$(git ls-files 'target/' '**/target/' 2>/dev/null)" - severity: warning -## Burble-Specific Cleanup - -### stale-room-processes -- description: Room processes should auto-terminate after idle timeout -- verification: Burble.Rooms.Room uses @idle_timeout_ms (5 minutes) -- severity: info -- notes: Not a file check — design verification that idle rooms are cleaned up - -### expired-invite-tokens -- description: Expired invite tokens should be purged periodically -- verification: Scheduled task purges tokens past expires_at -- severity: info -- notes: Planned — not yet implemented - -### orphaned-turn-credentials -- description: TURN credentials expire after 1 hour -- verification: Burble.Media.Privacy.generate_turn_credential sets TTL -- severity: info +## Duplicates -### template-example-trustfile -- description: Remove the example Trustfile (keep only the real one) -- run: test ! -f .machine_readable/contractiles/trust/Trustfile_just_an_example.a2ml +### single-contributing-format +- description: Prefer a single CONTRIBUTING (DOC-FORMAT prefers .adoc; .md is the GitHub community-health exception) +- run: test -z "$(test -f CONTRIBUTING.adoc && test -f CONTRIBUTING.md && echo dup)" - severity: info -- rollback: git checkout HEAD -- .machine_readable/contractiles/trust/Trustfile_just_an_example.a2ml - -## Format Duplicates - -### no-duplicate-contributing -- description: Only one CONTRIBUTING format -- run: test -z "$(test -f CONTRIBUTING.md && test -f CONTRIBUTING.adoc && echo dup)" -- severity: warning +- notes: Both CONTRIBUTING.adoc and CONTRIBUTING.md currently exist (2026-06-05); owner decides which to retire. ### no-duplicate-readme - description: Only one README format - run: test ! -f README.md || test ! -f README.adoc - severity: warning + +## Formal Archive Hygiene + +### preservation-design-is-canonical +- description: PRESERVATION-DESIGN.md is the canonical design; PRESERVATION-HANDOFF.md is historical diagnostic only +- run: test -f formal/PRESERVATION-DESIGN.md +- severity: info +- notes: HANDOFF carries the pre-discovery record; do not act on it as instructions. Keep both. diff --git a/.machine_readable/contractiles/k9/template-hunt.k9.ncl b/.machine_readable/contractiles/k9/template-hunt.k9.ncl new file mode 100644 index 00000000..a9cc350e --- /dev/null +++ b/.machine_readable/contractiles/k9/template-hunt.k9.ncl @@ -0,0 +1,136 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# K9 Hunt-level template: Full execution with Just recipes +# Security Level: Hunt (full system access) +# ⚠️ SIGNATURE REQUIRED - Review carefully before use + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "TODO: describe component type (e.g., 'deployment', 'setup-script')", + security = { + leash = 'Hunt, + trust_level = "full-system-access", + allow_network = true, + allow_filesystem_write = true, + allow_subprocess = true, + signature_required = true, + }, + metadata = { + name = "TODO: component-name", + version = "1.0.0", + description = "TODO: Detailed description of what this component does", + author = "{{AUTHOR}} <{{AUTHOR_EMAIL}}>", + }, + warnings = [ + "This component has full system access", + "Only run from trusted sources with verified signatures", + "Review all Just recipes before execution", + "Use dry-run mode first: ./must --dry-run run your-file.k9.ncl", + ], + side_effects = [ + "TODO: List what files/directories this creates or modifies", + "TODO: List what commands this executes", + "TODO: List what network access this requires", + ], + }, + + # Configuration with contracts (Yard-level validation) + config = { + # Add your configuration here with appropriate contracts + target_dir + | String + | std.string.NonEmpty + = "/tmp/k9-output", + + dry_run | Bool = false, + + # Add more config as needed + }, + + # Just recipes for execution + # These run when: ./must run your-file.k9.ncl + recipes = { + # Main entry point (runs by default) + default = { + recipe = "TODO: main-task", + description = "TODO: What the default recipe does", + }, + + # Define your recipes here + "main-task" = { + dependencies = ["check-prerequisites"], + commands = [ + "echo 'TODO: Add your commands here'", + # Example: Create directory + # "mkdir -p %{config.target_dir}", + # Example: Run a command + # "just build", + # Example: Conditional execution + # "@if [ \"%{config.dry_run}\" = \"true\" ]; then echo '[DRY-RUN] Would execute'; else actual-command; fi", + ], + }, + + "check-prerequisites" = { + description = "Verify required tools and permissions", + commands = [ + # Example: Check for required tools + # "command -v git || (echo 'ERROR: git not found' && exit 1)", + # Example: Check permissions + # "[ -w %{config.target_dir} ] || (echo 'ERROR: Cannot write to target directory' && exit 1)", + "echo '✓ Prerequisites checked'", + ], + }, + + # Add more recipes as needed + "build" = { + description = "Build the project", + commands = [ + "echo 'TODO: Add build commands'", + ], + }, + + "deploy" = { + description = "Deploy the application", + dependencies = ["build"], + commands = [ + "echo 'TODO: Add deployment commands'", + ], + }, + + "clean" = { + description = "Clean up generated files", + commands = [ + "echo '⚠️ This will delete files - waiting 3 seconds...'", + "sleep 3", + "echo 'TODO: Add cleanup commands'", + # "rm -rf %{config.target_dir}", + ], + }, + }, + + # Validation (Yard-level checks before Hunt execution) + validation = { + check_target_dir = std.string.length config.target_dir > 0, + # Add more validation as needed + }, +} + +# Usage: +# 1. Fill in TODO items above +# 2. Define configuration with contracts +# 3. Implement Just recipes with your commands +# 4. Test with dry-run: ./must --dry-run run your-file.k9.ncl +# 5. Review dry-run output carefully +# 6. Sign the component: ./must sign your-file.k9.ncl +# 7. Distribute with signature: your-file.k9.ncl.sig +# 8. Users verify and run: ./must verify && ./must run your-file.k9.ncl +# +# Security checklist: +# ✓ All TODO items filled in +# ✓ side_effects documented accurately +# ✓ Commands reviewed for safety +# ✓ No hardcoded secrets or credentials +# ✓ Proper error handling in recipes +# ✓ Tested in dry-run mode +# ✓ Component signed with trusted key diff --git a/.machine_readable/contractiles/k9/template-kennel.k9.ncl b/.machine_readable/contractiles/k9/template-kennel.k9.ncl new file mode 100644 index 00000000..fa7e3f35 --- /dev/null +++ b/.machine_readable/contractiles/k9/template-kennel.k9.ncl @@ -0,0 +1,54 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# K9 Kennel-level template: Pure data configuration +# Security Level: Kennel (data-only, no execution) +# No signature required - safe for any use + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "TODO: describe component type (e.g., 'build-config', 'metadata')", + security = { + leash = 'Kennel, + trust_level = "data-only", + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = false, + }, + metadata = { + name = "TODO: component-name", + version = "1.0.0", + description = "TODO: Brief description of what this component contains", + author = "{{AUTHOR}} <{{AUTHOR_EMAIL}}>", + }, + }, + + # Your configuration data here + config = { + # Example: Pure data values + setting_1 = "value", + setting_2 = 42, + setting_3 = true, + + nested = { + key = "value", + }, + + list = [ + "item1", + "item2", + ], + }, + + # Optional: Export format specification + export = { + format = "json", # or "yaml", "toml" + destination = "output.json", + }, +} + +# Usage: +# 1. Fill in TODO items above +# 2. Add your configuration data to config = { ... } +# 3. Validate: nickel typecheck your-file.k9.ncl +# 4. Export: nickel export your-file.k9.ncl > output.json diff --git a/.machine_readable/contractiles/k9/template-yard.k9.ncl b/.machine_readable/contractiles/k9/template-yard.k9.ncl new file mode 100644 index 00000000..358671cf --- /dev/null +++ b/.machine_readable/contractiles/k9/template-yard.k9.ncl @@ -0,0 +1,84 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# K9 Yard-level template: Configuration with validation +# Security Level: Yard (Nickel evaluation with contracts) +# Signature recommended but not required + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "TODO: describe component type (e.g., 'validated-config', 'schema')", + security = { + leash = 'Yard, + trust_level = "validated-config", + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = false, + }, + metadata = { + name = "TODO: component-name", + version = "1.0.0", + description = "TODO: Brief description with validation details", + author = "{{AUTHOR}} <{{AUTHOR_EMAIL}}>", + }, + }, + + # Configuration with Nickel contracts for validation + config = { + # Example: String that cannot be empty + name + | String + | std.string.NonEmpty + = "TODO: default value", + + # Example: Number with range constraint + port + | Number + | std.contract.from_predicate (fun p => p > 0 && p < 65536) + = 8080, + + # Example: Boolean flag + enabled | Bool = true, + + # Example: Enum (one of several values) + environment + | [| 'Development, 'Staging, 'Production |] + = 'Development, + + # Example: List with non-empty constraint + items + | Array String + | std.array.NonEmpty + = ["item1", "item2"], + + # Example: Nested object with contracts + database = { + host | String | std.string.NonEmpty = "localhost", + port | Number | std.contract.from_predicate (fun p => p > 0 && p < 65536) = 5432, + name | String | std.string.NonEmpty = "mydb", + }, + }, + + # Validation rules (additional cross-field checks) + validation = { + # Example: Check that at least one item exists + check_items = std.array.length config.items > 0, + + # Example: Check that production has secure settings + check_production = + if config.environment == 'Production then + config.enabled == true + else + true, + + # Add your custom validation rules here + }, +} + +# Usage: +# 1. Fill in TODO items above +# 2. Define your config with appropriate contracts +# 3. Add validation rules in validation = { ... } +# 4. Validate: nickel typecheck your-file.k9.ncl +# 5. Evaluate: nickel eval your-file.k9.ncl +# 6. If validation passes, use in your application diff --git a/.machine_readable/contractiles/must/Mustfile.a2ml b/.machine_readable/contractiles/must/Mustfile.a2ml index bf03f7b3..426d4868 100644 --- a/.machine_readable/contractiles/must/Mustfile.a2ml +++ b/.machine_readable/contractiles/must/Mustfile.a2ml @@ -1,5 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 -# Mustfile — Physical state contract for Burble +# Mustfile — Physical state contract for Ephapax # Author: Jonathan D.A. Jewell # # What MUST be true about this repository. Hard requirements. @@ -7,8 +7,10 @@ # Fix with: must fix (where deterministic fix exists) @abstract: -Physical state invariants for the Burble voice platform. -These are hard requirements — CI and pre-commit hooks fail if any check fails. +Physical-state invariants for Ephapax — the substructural-logic language +(ephapax-linear strict core / ephapax-affine prototyping companion) with a +Rust toolchain and mechanised Coq + Idris2 metatheory, compiling to typed-wasm. +Hard requirements: CI and pre-commit hooks fail if any critical check fails. @end ## File Presence @@ -35,7 +37,7 @@ These are hard requirements — CI and pre-commit hooks fail if any check fails. ### contributing - description: CONTRIBUTING guide must exist -- run: test -f CONTRIBUTING.adoc || test -f .github/CONTRIBUTING.md +- run: test -f CONTRIBUTING.adoc || test -f CONTRIBUTING.md - severity: warning ### editorconfig @@ -43,102 +45,104 @@ These are hard requirements — CI and pre-commit hooks fail if any check fails. - run: test -f .editorconfig - severity: warning -## Elixir Server +## Rust Toolchain -### mix-exs-present -- description: Elixir mix.exs must exist in server/ -- run: test -f server/mix.exs +### cargo-manifest-present +- description: Cargo workspace manifest must exist +- run: test -f Cargo.toml - severity: critical -### elixir-compiles -- description: Elixir server compiles without errors -- run: test -f server/mix.exs +### cargo-lock-present +- description: Cargo.lock must be committed (reproducible builds) +- run: test -f Cargo.lock - severity: critical -- notes: Full compile check via CI (mix compile), file presence check here -### ecto-migrations-exist -- description: Database migrations directory exists -- run: test -d server/priv/repo/migrations +### linear-crate-present +- description: ephapax-linear (strict verified core) crate must exist +- run: test -d ephapax-linear - severity: critical -### config-files-present -- description: All config files exist -- run: test -f server/config/config.exs && test -f server/config/dev.exs && test -f server/config/prod.exs && test -f server/config/runtime.exs +### workspace-compiles +- description: Rust workspace compiles +- run: test -f Cargo.toml - severity: critical +- notes: File-presence proxy here; full `cargo build --workspace` runs in CI. -## Web Client +## Mechanised Metatheory -### rescript-json-present -- description: ReScript config exists for web client -- run: test -f client/web/rescript.json -- severity: warning +### coq-semantics-present +- description: Coq operational semantics must exist +- run: test -f formal/Semantics.v +- severity: critical + +### preservation-design-present +- description: Four-layer preservation design doc must exist +- run: test -f formal/PRESERVATION-DESIGN.md +- severity: critical + +### counterexample-present +- description: Preservation counterexample (regression guard) must exist +- run: test -f formal/Counterexample.v +- severity: critical + +### legacy-preservation-stays-admitted +- description: Legacy `Theorem preservation` in Semantics.v MUST remain Admitted — it is provably false; closing it to Qed is forbidden (owner directive 2026-05-27) +- run: grep -q 'Admitted' formal/Semantics.v +- severity: critical +- notes: Counterexample.v depends on this falsity for the regression theorem. The four-layer redesign re-derives preservation per-layer; it is never forced through the legacy judgment. -### web-entry-point -- description: Web client entry point exists -- run: test -f server/priv/static/index.html || test -f client/web/index.html +### idris-abi-present +- description: Idris2 ABI modules must exist +- run: test -d src/abi/Ephapax +- severity: critical + +## Source Surface + +### stdlib-present +- description: .eph standard-library sources must exist +- run: test -n "$(find stdlib -name '*.eph' 2>/dev/null | head -1)" - severity: warning ## SPDX Compliance -### spdx-elixir -- description: All Elixir files have SPDX header -- run: test -z "$(find server/lib -name '*.ex' -exec head -1 {} \; 2>/dev/null | grep -cv 'SPDX' | grep -v '^0$')" +### spdx-rust +- description: Rust sources carry an SPDX header +- run: test -z "$(find src ephapax-linear -name '*.rs' -not -path '*/target/*' -exec head -1 {} \; 2>/dev/null | grep -cv 'SPDX' | grep -v '^0$')" - severity: warning ### no-agpl -- description: No AGPL-3.0 references (replaced by PMPL) +- description: No AGPL-3.0 in license-bearing root files (estate license is MPL-2.0) - run: test -z "$(grep -rl 'AGPL-3.0' LICENSE .editorconfig .gitattributes 2>/dev/null)" - severity: critical ## Dangerous Patterns ### no-believe-me -- description: No believe_me in Idris2 code +- description: No believe_me escapes in Idris2 proofs - run: test -z "$(find . -name '*.idr' -not -path '*/deps/*' -exec grep -l 'believe_me' {} \; 2>/dev/null)" -- severity: critical - -### no-unsafe-coerce -- description: No unsafeCoerce in ReScript/Haskell code -- run: test -z "$(find . \( -name '*.res' -o -name '*.hs' \) -not -path '*/deps/*' -not -path '*/node_modules/*' -exec grep -l 'unsafeCoerce\|Obj.magic' {} \; 2>/dev/null)" -- severity: critical - -## Container Policy - -### containerfile-not-dockerfile -- description: Uses Containerfile, not Dockerfile -- run: test -z "$(find . -name 'Dockerfile' -not -path '*/.clusterfuzzlite/*' 2>/dev/null)" -- severity: warning - -### no-docker-commands -- description: No docker commands in scripts (use podman) -- run: test -z "$(grep -rl 'docker run\|docker build\|docker compose' --include='*.sh' --include='*.yml' . 2>/dev/null | grep -v deps | grep -v node_modules)" - severity: warning +- notes: 1 occurrence currently exists (2026-06-05) — tracked to zero; see deferred issue. Warning (not critical) so it does not block while tracked. ## Language Policy -### no-typescript -- description: No TypeScript files (use ReScript) -- run: test -z "$(find . -name '*.ts' -not -name '*.d.ts' -not -path '*/deps/*' -not -path '*/node_modules/*' 2>/dev/null)" +### no-python +- description: No Python sources (use Rust) +- run: test -z "$(find . -name '*.py' -not -path '*/deps/*' -not -path '*/.git/*' 2>/dev/null)" - severity: warning -### no-python -- description: No Python files (use Julia/Rust/ReScript) -- run: test -z "$(find . -name '*.py' -not -path '*/deps/*' -not -path '*/node_modules/*' 2>/dev/null)" +### no-typescript +- description: No TypeScript sources +- run: test -z "$(find . -name '*.ts' -not -name '*.d.ts' -not -path '*/deps/*' -not -path '*/node_modules/*' 2>/dev/null)" - severity: warning ## Security -### no-secrets-in-config -- description: No hardcoded secrets in Elixir config -- run: test -z "$(grep -rE '(secret_key_base|password).*=\"[A-Za-z0-9+/]{32,}\"' server/config/ 2>/dev/null | grep -v 'dev_only\|test_only')" -- severity: critical - -### beam-cookie-absent -- description: No Erlang cookie in repository -- run: test -z "$(find . -name '.erlang.cookie' 2>/dev/null)" -- severity: critical - ### env-files-absent - description: No .env files committed -- run: test ! -f .env && test ! -f server/.env && test ! -f .env.local && test ! -f .env.production +- run: test ! -f .env && test ! -f .env.local && test ! -f .env.production +- severity: critical + +### no-hardcoded-secrets +- description: No obvious hardcoded secrets in tracked sources +- run: test -z "$(grep -rIE '(secret|password|api[_-]?key)[[:space:]]*=[[:space:]]*\"[A-Za-z0-9+/]{24,}\"' src 2>/dev/null | grep -v test)" - severity: critical diff --git a/.machine_readable/svc/k9/README.adoc b/.machine_readable/svc/k9/README.adoc new file mode 100644 index 00000000..eeb12290 --- /dev/null +++ b/.machine_readable/svc/k9/README.adoc @@ -0,0 +1,178 @@ +// SPDX-License-Identifier: MPL-2.0 += K9 Contractiles +:toc: left +:icons: font + +== What Are K9 Contractiles? + +K9 contractiles are self-validating components that combine configuration, validation, and deployment logic in a single file format. They implement the RSR principle of "self-describing artifacts" by embedding contracts and orchestration directly in the component. + +== The Three Security Levels + +K9 components declare their trust requirements using "The Leash" security model: + +[horizontal] +`'Kennel`:: Pure data, no execution (safest) +`'Yard`:: Nickel evaluation with contracts (medium trust) +`'Hunt`:: Full execution with Just recipes (requires signature) + +== Example Components + +This directory contains example K9 contractiles for common repository tasks: + +=== Kennel Level (Pure Data) + +**File:** `examples/project-metadata.k9.ncl` + +Pure configuration data with no execution. Safe to include in any repository. + +**Use cases:** +- Project metadata (name, version, description) +- Build configuration +- Tool settings +- Data schemas + +**Security:** No signature required, data-only. + +=== Yard Level (Validated Config) + +**File:** `examples/ci-config.k9.ncl` + +Configuration with Nickel contracts for runtime validation. Evaluated safely without I/O. + +**Use cases:** +- CI/CD configuration with validation +- Deployment parameters +- Database schemas with constraints +- API specifications + +**Security:** Signature recommended, Nickel evaluation only. + +=== Hunt Level (Full Execution) + +**File:** `examples/setup-repo.k9.ncl` + +Full execution with Just recipes. Can run shell commands and modify filesystem. + +**Use cases:** +- Repository setup scripts +- Deployment automation +- System configuration +- Package installation + +**Security:** **Signature required**, full system access. + +== Usage in Your Repository + +=== 1. Create K9 Components + +Choose the appropriate security level for your use case: + +[source,bash] +---- +# Kennel: Pure configuration +cp .machine_readable/contractiles/k9/examples/project-metadata.k9.ncl config/metadata.k9.ncl + +# Yard: Validated configuration +cp .machine_readable/contractiles/k9/examples/ci-config.k9.ncl .github/ci.k9.ncl + +# Hunt: Full automation +cp .machine_readable/contractiles/k9/examples/setup-repo.k9.ncl scripts/setup.k9.ncl +---- + +=== 2. Validate Components + +[source,bash] +---- +# Validate Nickel syntax and contracts +nickel typecheck config/metadata.k9.ncl + +# Verify Hunt-level signature (if signed) +./must verify scripts/setup.k9.ncl +---- + +=== 3. Execute Components + +[source,bash] +---- +# Kennel: Export as JSON +nickel export config/metadata.k9.ncl > metadata.json + +# Yard: Evaluate with validation +nickel eval .github/ci.k9.ncl + +# Hunt: Run with Just (dry-run first!) +./must --dry-run run scripts/setup.k9.ncl +./must run scripts/setup.k9.ncl +---- + +== Integration with RSR + +K9 contractiles integrate with other RSR standards: + +**STATE.a2ml**:: K9 components can generate or validate STATE.a2ml +**ECOSYSTEM.a2ml**:: K9 can automate cross-repo operations +**META.a2ml**:: K9 can enforce architectural decisions + +== Security Best Practices + +=== For Kennel/Yard Components + +✅ **Safe to use without signatures** + +✅ **Review Nickel code before use** + +✅ **Validate contracts match expectations** + +=== For Hunt Components + +⚠️ **ALWAYS verify signatures** + +⚠️ **Review Just recipes carefully** + +⚠️ **Run dry-run mode first** + +⚠️ **Never run as root unless required** + +⚠️ **Sandbox external components** + +**See:** https://github.com/hyperpolymath/standards/blob/main/k9-svc/docs/SECURITY-BEST-PRACTICES.adoc + +== Template Files + +Use these as starting points for your own K9 components: + +- `template-kennel.k9.ncl` - Pure data template +- `template-yard.k9.ncl` - Validated config template +- `template-hunt.k9.ncl` - Full execution template + +== Dependencies + +To use K9 contractiles in your repository: + +[source,bash] +---- +# Install Nickel (configuration language) +curl -L https://github.com/tweag/nickel/releases/latest/download/nickel-linux-x86_64 -o nickel +chmod +x nickel && sudo mv nickel /usr/local/bin/ + +# Install Just (task runner, for Hunt level) +cargo install just + +# Clone K9-SVC (for must shim and tooling) +git clone https://github.com/hyperpolymath/standards.git +# Note: K9-SVC is located in standards/k9-svc +---- + +== Learn More + +- **K9-SVC Specification:** https://github.com/hyperpolymath/standards/blob/main/k9-svc/SPEC.adoc +- **K9 User Guide:** https://github.com/hyperpolymath/standards/blob/main/k9-svc/GUIDE.adoc +- **Security Documentation:** https://github.com/hyperpolymath/standards/blob/main/k9-svc/docs/SECURITY-FAQ.adoc +- **IANA Media Type:** `application/vnd.k9+nickel` + +== Contributing + +When adding K9 contractiles to your repository: + +1. Use appropriate security level (Kennel > Yard > Hunt) +2. Document what each component does +3. Include validation contracts in Yard/Hunt components +4. Sign Hunt-level components before committing +5. Add K9 validation to CI/CD pipeline + +**Questions?** Open an issue on https://github.com/hyperpolymath/standards/tree/main/k9-svc diff --git a/.machine_readable/svc/k9/template-hunt.k9.ncl b/.machine_readable/svc/k9/template-hunt.k9.ncl new file mode 100644 index 00000000..a9cc350e --- /dev/null +++ b/.machine_readable/svc/k9/template-hunt.k9.ncl @@ -0,0 +1,136 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# K9 Hunt-level template: Full execution with Just recipes +# Security Level: Hunt (full system access) +# ⚠️ SIGNATURE REQUIRED - Review carefully before use + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "TODO: describe component type (e.g., 'deployment', 'setup-script')", + security = { + leash = 'Hunt, + trust_level = "full-system-access", + allow_network = true, + allow_filesystem_write = true, + allow_subprocess = true, + signature_required = true, + }, + metadata = { + name = "TODO: component-name", + version = "1.0.0", + description = "TODO: Detailed description of what this component does", + author = "{{AUTHOR}} <{{AUTHOR_EMAIL}}>", + }, + warnings = [ + "This component has full system access", + "Only run from trusted sources with verified signatures", + "Review all Just recipes before execution", + "Use dry-run mode first: ./must --dry-run run your-file.k9.ncl", + ], + side_effects = [ + "TODO: List what files/directories this creates or modifies", + "TODO: List what commands this executes", + "TODO: List what network access this requires", + ], + }, + + # Configuration with contracts (Yard-level validation) + config = { + # Add your configuration here with appropriate contracts + target_dir + | String + | std.string.NonEmpty + = "/tmp/k9-output", + + dry_run | Bool = false, + + # Add more config as needed + }, + + # Just recipes for execution + # These run when: ./must run your-file.k9.ncl + recipes = { + # Main entry point (runs by default) + default = { + recipe = "TODO: main-task", + description = "TODO: What the default recipe does", + }, + + # Define your recipes here + "main-task" = { + dependencies = ["check-prerequisites"], + commands = [ + "echo 'TODO: Add your commands here'", + # Example: Create directory + # "mkdir -p %{config.target_dir}", + # Example: Run a command + # "just build", + # Example: Conditional execution + # "@if [ \"%{config.dry_run}\" = \"true\" ]; then echo '[DRY-RUN] Would execute'; else actual-command; fi", + ], + }, + + "check-prerequisites" = { + description = "Verify required tools and permissions", + commands = [ + # Example: Check for required tools + # "command -v git || (echo 'ERROR: git not found' && exit 1)", + # Example: Check permissions + # "[ -w %{config.target_dir} ] || (echo 'ERROR: Cannot write to target directory' && exit 1)", + "echo '✓ Prerequisites checked'", + ], + }, + + # Add more recipes as needed + "build" = { + description = "Build the project", + commands = [ + "echo 'TODO: Add build commands'", + ], + }, + + "deploy" = { + description = "Deploy the application", + dependencies = ["build"], + commands = [ + "echo 'TODO: Add deployment commands'", + ], + }, + + "clean" = { + description = "Clean up generated files", + commands = [ + "echo '⚠️ This will delete files - waiting 3 seconds...'", + "sleep 3", + "echo 'TODO: Add cleanup commands'", + # "rm -rf %{config.target_dir}", + ], + }, + }, + + # Validation (Yard-level checks before Hunt execution) + validation = { + check_target_dir = std.string.length config.target_dir > 0, + # Add more validation as needed + }, +} + +# Usage: +# 1. Fill in TODO items above +# 2. Define configuration with contracts +# 3. Implement Just recipes with your commands +# 4. Test with dry-run: ./must --dry-run run your-file.k9.ncl +# 5. Review dry-run output carefully +# 6. Sign the component: ./must sign your-file.k9.ncl +# 7. Distribute with signature: your-file.k9.ncl.sig +# 8. Users verify and run: ./must verify && ./must run your-file.k9.ncl +# +# Security checklist: +# ✓ All TODO items filled in +# ✓ side_effects documented accurately +# ✓ Commands reviewed for safety +# ✓ No hardcoded secrets or credentials +# ✓ Proper error handling in recipes +# ✓ Tested in dry-run mode +# ✓ Component signed with trusted key diff --git a/.machine_readable/svc/k9/template-kennel.k9.ncl b/.machine_readable/svc/k9/template-kennel.k9.ncl new file mode 100644 index 00000000..fa7e3f35 --- /dev/null +++ b/.machine_readable/svc/k9/template-kennel.k9.ncl @@ -0,0 +1,54 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# K9 Kennel-level template: Pure data configuration +# Security Level: Kennel (data-only, no execution) +# No signature required - safe for any use + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "TODO: describe component type (e.g., 'build-config', 'metadata')", + security = { + leash = 'Kennel, + trust_level = "data-only", + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = false, + }, + metadata = { + name = "TODO: component-name", + version = "1.0.0", + description = "TODO: Brief description of what this component contains", + author = "{{AUTHOR}} <{{AUTHOR_EMAIL}}>", + }, + }, + + # Your configuration data here + config = { + # Example: Pure data values + setting_1 = "value", + setting_2 = 42, + setting_3 = true, + + nested = { + key = "value", + }, + + list = [ + "item1", + "item2", + ], + }, + + # Optional: Export format specification + export = { + format = "json", # or "yaml", "toml" + destination = "output.json", + }, +} + +# Usage: +# 1. Fill in TODO items above +# 2. Add your configuration data to config = { ... } +# 3. Validate: nickel typecheck your-file.k9.ncl +# 4. Export: nickel export your-file.k9.ncl > output.json diff --git a/.machine_readable/svc/k9/template-yard.k9.ncl b/.machine_readable/svc/k9/template-yard.k9.ncl new file mode 100644 index 00000000..358671cf --- /dev/null +++ b/.machine_readable/svc/k9/template-yard.k9.ncl @@ -0,0 +1,84 @@ +K9! +# SPDX-License-Identifier: MPL-2.0 +# K9 Yard-level template: Configuration with validation +# Security Level: Yard (Nickel evaluation with contracts) +# Signature recommended but not required + +{ + pedigree = { + schema_version = "1.0.0", + component_type = "TODO: describe component type (e.g., 'validated-config', 'schema')", + security = { + leash = 'Yard, + trust_level = "validated-config", + allow_network = false, + allow_filesystem_write = false, + allow_subprocess = false, + }, + metadata = { + name = "TODO: component-name", + version = "1.0.0", + description = "TODO: Brief description with validation details", + author = "{{AUTHOR}} <{{AUTHOR_EMAIL}}>", + }, + }, + + # Configuration with Nickel contracts for validation + config = { + # Example: String that cannot be empty + name + | String + | std.string.NonEmpty + = "TODO: default value", + + # Example: Number with range constraint + port + | Number + | std.contract.from_predicate (fun p => p > 0 && p < 65536) + = 8080, + + # Example: Boolean flag + enabled | Bool = true, + + # Example: Enum (one of several values) + environment + | [| 'Development, 'Staging, 'Production |] + = 'Development, + + # Example: List with non-empty constraint + items + | Array String + | std.array.NonEmpty + = ["item1", "item2"], + + # Example: Nested object with contracts + database = { + host | String | std.string.NonEmpty = "localhost", + port | Number | std.contract.from_predicate (fun p => p > 0 && p < 65536) = 5432, + name | String | std.string.NonEmpty = "mydb", + }, + }, + + # Validation rules (additional cross-field checks) + validation = { + # Example: Check that at least one item exists + check_items = std.array.length config.items > 0, + + # Example: Check that production has secure settings + check_production = + if config.environment == 'Production then + config.enabled == true + else + true, + + # Add your custom validation rules here + }, +} + +# Usage: +# 1. Fill in TODO items above +# 2. Define your config with appropriate contracts +# 3. Add validation rules in validation = { ... } +# 4. Validate: nickel typecheck your-file.k9.ncl +# 5. Evaluate: nickel eval your-file.k9.ncl +# 6. If validation passes, use in your application diff --git a/docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc b/docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc index f2c1d2f6..b1786ae3 100644 --- a/docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc +++ b/docs/sessions/SESSION-2026-05-20-proof-engineering-lessons.adoc @@ -14,7 +14,7 @@ Each lesson is named, has a reproducer, and lists where in the codebase the pattern bit us so the cross-reference is auditable. Companion machine-readable artefact: -`.machine_readable/agent_instructions/lessons.a2ml`. +`.machine_readable/bot_directives/lessons.a2ml`. PRs that surfaced these (this repo, 2026-05-20): proof-of-work#63, ephapax#92, ephapax#95, ephapax#98, ephapax#102,