From 136a05bf6c59bdc4d0b7d23f64532ea904e97d8b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 02:26:48 +0100 Subject: [PATCH 01/14] fix(proof): preserve complete Isabelle obligations and fail closed --- .github/workflows/actions.lock | 19 +++ .github/workflows/proof-safety.yml | 61 ++++++++++ crates/burrower-core/src/attempt.rs | 121 ++++++++++++++++---- crates/burrower-core/tests/live_isabelle.rs | 55 +++++++++ 4 files changed, 235 insertions(+), 21 deletions(-) create mode 100644 .github/workflows/actions.lock create mode 100644 .github/workflows/proof-safety.yml create mode 100644 crates/burrower-core/tests/live_isabelle.rs diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock new file mode 100644 index 0000000..fa47800 --- /dev/null +++ b/.github/workflows/actions.lock @@ -0,0 +1,19 @@ +# This file is machine-generated by `gh actions-lock`. +# Do not edit by hand; run `gh actions-lock` to update. +# Docs: https://gh.io/actions-lockfile +version: 'v0.0.2' +workflows: + '.github/workflows/proof-safety.yml': + - 'actions/checkout@v7.0.1' + - 'swatinem/rust-cache@v2.9.2' +dependencies: + 'actions/checkout@v7.0.1': + ref: 'v7.0.1' + commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1' + owner_id: 44036562 + repo_id: 197814629 + 'swatinem/rust-cache@v2.9.2': + ref: 'v2.9.2' + commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6' + owner_id: 580492 + repo_id: 298565987 diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml new file mode 100644 index 0000000..0dde912 --- /dev/null +++ b/.github/workflows/proof-safety.yml @@ -0,0 +1,61 @@ +# This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 +name: Proof Safety +on: + pull_request: + push: + branches: [main] +permissions: + contents: read +concurrency: + group: proof-safety-${{ github.ref }} + cancel-in-progress: true +jobs: + isabelle: + name: Burrower proof safety + runs-on: ubuntu-24.04 + timeout-minutes: 45 + steps: + - uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + - uses: actions/checkout@v7.0.1 + with: + repository: hyperpolymath/echidna + ref: 556d64687a8872026c81e4689ac3d574c7acc6ce + path: _echidna + persist-credentials: false + - uses: Swatinem/rust-cache@v2.9.2 + with: + workspaces: | + . -> target + _echidna -> target + - name: Install native build dependencies + run: | + sudo apt-get update + sudo apt-get install -y capnproto pkg-config libssl-dev + - name: Install checksum-verified Isabelle + shell: bash + run: | + set -euo pipefail + cd "$RUNNER_TEMP" + curl --fail --location --retry 3 -o isabelle.tar.gz https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2025-2_linux.tar.gz + echo 'a20a507bc7c1270d8be96a9f3fbec06345387789d2dc2c4d3df6260d47bfb33c isabelle.tar.gz' | sha256sum --check --strict + tar -xzf isabelle.tar.gz + echo "$RUNNER_TEMP/Isabelle2025-2/bin" >> "$GITHUB_PATH" + echo "USER_HOME=$RUNNER_TEMP/isabelle-user" >> "$GITHUB_ENV" + mkdir -p "$RUNNER_TEMP/isabelle-user/.isabelle/Isabelle2025-2/etc" + cat > "$RUNNER_TEMP/isabelle-user/.isabelle/Isabelle2025-2/etc/settings" <<'SETTINGS' + ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms256m -Xmx1536m -Xss16m" + ML_OPTIONS="--minheap 256 --maxheap 2048" + SETTINGS + - name: Build ECHIDNA and run Burrower unit tests + run: | + cargo build --locked --manifest-path _echidna/Cargo.toml --bin echidna + cargo test --locked --workspace + - name: Require real accepted and rejected Isabelle goals + env: + ECHIDNA_BIN: ${{ github.workspace }}/_echidna/target/debug/echidna + run: | + isabelle version + cargo test --locked -p burrower-core --test live_isabelle -- --ignored --nocapture diff --git a/crates/burrower-core/src/attempt.rs b/crates/burrower-core/src/attempt.rs index 34a0877..41e1b00 100644 --- a/crates/burrower-core/src/attempt.rs +++ b/crates/burrower-core/src/attempt.rs @@ -127,8 +127,7 @@ pub struct ProofAttempt { /// /// The probe wraps the goal as a `lemma probe_lemma:` with the /// supplied tactic as the proof script. We strip the original lemma -/// name + assumes/shows scaffolding and reformulate as a single -/// `lemma probe_lemma: "" `. +/// name and proof script while retaining assumptions and every conclusion. /// /// For complex goals this is best-effort. The function returns the /// probe text on success; callers write it to disk and pass the path @@ -148,8 +147,9 @@ pub fn generate_probe(goal_text: &str, tactic: &TacticTemplate) -> String { ) } -/// Heuristic: extract the lemma statement (the part inside the outer -/// quotes, or the whole text if quotes aren't present). +/// Extract a simple Isabelle statement, retaining every quoted clause. +/// This is not a complete Isabelle outer-syntax parser; unsupported syntax +/// is retained for the real prover to reject rather than dropping clauses. /// /// Examples handled: /// `lemma foo: "x + 0 = x" by simp` → `"x + 0 = x"` @@ -162,30 +162,58 @@ fn extract_statement(goal_text: &str) -> String { for kw in &lower_kws { if let Some(start) = goal_text.find(kw) { let rest = &goal_text[start + kw.len()..]; - if let Some(c) = rest.find(':') { + if let Some(c) = rest.find(':').filter(|c| { + // A colon inside a quoted proposition (e.g. x::nat) is + // not the separator after a theorem name. + rest.find('"').is_none_or(|quote| *c < quote) + }) { after_colon = Some(&rest[c + 1..]); break; + } else if rest.trim_start().starts_with('"') { + after_colon = Some(rest); + break; } } } let body = after_colon.unwrap_or(goal_text).trim(); - // If the body has a quoted segment, take the first quoted region. - if let Some(q1) = body.find('"') { - let after_q1 = &body[q1 + 1..]; - if let Some(q2) = after_q1.find('"') { - return format!("\"{}\"", &after_q1[..q2]); + // Preserve the complete statement, including fixes/assumes/shows and + // multiple quoted propositions. Taking the first quote can silently + // replace the conclusion with an assumption. Stop at an existing proof + // command only outside quoted terms; Isabelle checks the retained syntax. + let mut quoted = false; + let mut escaped = false; + let mut end = body.len(); + for (index, ch) in body.char_indices() { + if escaped { + escaped = false; + continue; + } + if quoted && ch == '\\' { + escaped = true; + continue; + } + if ch == '"' { + quoted = !quoted; + continue; + } + if !quoted && (index == 0 || body[..index].ends_with(char::is_whitespace)) { + let tail = &body[index..]; + if ["by", "proof", ":="].iter().any(|marker| { + tail.strip_prefix(marker).is_some_and(|rest| { + rest.is_empty() || rest.starts_with(char::is_whitespace) + }) + }) { + end = index; + break; + } } } - // No quotes — wrap the body up to the first `by`/`proof` marker. - let trimmed: String = body - .lines() - .take_while(|l| { - let t = l.trim_start(); - !(t.starts_with("by ") || t.starts_with("proof") || t.starts_with(":=")) - }) - .collect::>() - .join("\n"); - format!("\"{}\"", trimmed.trim()) + let statement = body[..end].trim(); + if statement.contains('"') { + statement.to_string() + } else { + format!("\"{}\"", statement) + } } /// Run a single probe through the prover. Returns the raw outcome. @@ -266,7 +294,7 @@ pub fn run_probe( }); let exit_failed = !o.status.success(); - if says_success { + if says_success && !says_failure && !exit_failed { AttemptResult::Succeeded { duration_ms: elapsed_ms } } else if says_failure || exit_failed { let err_excerpt: String = combined_lines @@ -458,6 +486,57 @@ mod tests { assert_eq!(s, "\"y + y = 2 * y\""); } + #[test] + fn extract_statement_preserves_assumptions_and_conclusion() { + let statement = "assumes \"True\" shows \"False\""; + assert_eq!(extract_statement(&format!("lemma bad: {statement} by simp")), statement); + } + + #[test] + fn extract_statement_preserves_multiple_conclusions() { + assert_eq!(extract_statement("lemma bad: \"True\" and \"False\" by simp"), + "\"True\" and \"False\""); + } + + #[test] + fn extract_statement_keeps_type_annotation_in_anonymous_lemma() { + assert_eq!(extract_statement("lemma \"(x::nat) = x\" by simp"), "\"(x::nat) = x\""); + } + + #[test] + fn extract_statement_keeps_proof_words_inside_terms() { + assert_eq!(extract_statement("lemma foo: \"by = proof\" by simp"), "\"by = proof\""); + } + + #[cfg(unix)] + #[test] + fn subprocess_failure_overrides_success_text() { + use std::os::unix::fs::PermissionsExt; + let workdir = std::env::temp_dir().join(format!( + "burrower-output-regression-{}-{}", std::process::id(), + std::time::SystemTime::now().duration_since(std::time::UNIX_EPOCH).unwrap().as_nanos() + )); + std::fs::create_dir_all(&workdir).unwrap(); + let executable = workdir.join("output-fixture.sh"); + let config = ProverConfig { + echidna_path: executable.clone(), timeout_secs: 5, + workdir: Some(workdir.clone()), project_root: None, sandbox: "none".into(), + }; + // These subprocesses test the output contract, not theorem proving. + for (diagnostic, exit, expected) in [ + ("", 0, true), + ("", 1, false), + ("Proof verification failed", 0, false), + ] { + std::fs::write(&executable, format!( + "#!/bin/sh\nprintf 'Proof verified successfully\\n'\nprintf '{diagnostic}\\n' >&2\nexit {exit}\n" + )).unwrap(); + std::fs::set_permissions(&executable, std::fs::Permissions::from_mode(0o700)).unwrap(); + assert_eq!(run_probe("fixture", &config, "fixture.thy").is_success(), expected); + } + std::fs::remove_dir_all(workdir).unwrap(); + } + #[test] fn generate_probe_makes_well_formed_theory() { let g = parse_goal("lemma foo: \"x + 0 = x\" by simp"); diff --git a/crates/burrower-core/tests/live_isabelle.rs b/crates/burrower-core/tests/live_isabelle.rs new file mode 100644 index 0000000..d0c347f --- /dev/null +++ b/crates/burrower-core/tests/live_isabelle.rs @@ -0,0 +1,55 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Real Burrower -> ECHIDNA -> Isabelle acceptance and rejection controls. +use burrower_core::attempt::{ + generate_probe, run_probe, AttemptResult, ProverConfig, TacticTemplate, +}; + +#[test] +#[ignore = "requires ECHIDNA_BIN and Isabelle; required explicitly by Proof Safety CI"] +fn isabelle_preserves_and_checks_the_complete_goal() { + let echidna_path = std::env::var_os("ECHIDNA_BIN") + .expect("ECHIDNA_BIN must identify the built ECHIDNA executable") + .into(); + let work = tempfile::tempdir().expect("probe directory"); + let config = ProverConfig { + echidna_path, + timeout_secs: 120, + workdir: Some(work.path().to_path_buf()), + ..ProverConfig::default() + }; + let mut tactic = TacticTemplate { + name: "simp".into(), + script: "by simp".into(), + description: "Real Isabelle regression control".into(), + }; + for (goal, expected) in [ + (r#"lemma good: "(x::nat) + 0 = x""#, true), + (r#"lemma bad: "(x::nat) + 1 = x""#, false), + ( + r#"lemma dropped_conclusion: assumes "True" shows "False""#, + false, + ), + ( + r#"lemma assumed: assumes "(x::nat) = 0" shows "x + 1 = 1""#, + true, + ), + (r#"lemma multiple: shows "True" and "False""#, false), + ] { + tactic.script = if goal.contains("assumes") { + "using assms by simp" + } else { + "by simp" + }.into(); + let probe = generate_probe(goal, &tactic); + let result = run_probe(&probe, &config, "Probe.thy"); + eprintln!("{goal}: {result:?}"); + if expected { + assert!( + matches!(result, AttemptResult::Succeeded { .. }), + "{result:?}" + ); + } else { + assert!(matches!(result, AttemptResult::Failed { .. }), "{result:?}"); + } + } +} From c12b7217951ef96f0b3be588e52861cc7918973b Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 02:46:27 +0100 Subject: [PATCH 02/14] fix(ci): restore pinned gates and canonical Burrower metadata --- .envrc | 2 +- .github/workflows/actions.lock | 140 +++++++++ .github/workflows/boj-build.yml | 3 +- .github/workflows/codeql.yml | 7 +- .github/workflows/dependabot-automerge.yml | 3 +- .github/workflows/dogfood-gate.yml | 17 +- .github/workflows/governance.yml | 1 + .github/workflows/guix-nix-policy.yml | 3 +- .github/workflows/hypatia-scan.yml | 1 + .github/workflows/instant-sync.yml | 3 +- .github/workflows/label-triage.yml | 1 + .github/workflows/labels.yml | 1 + .github/workflows/main-estate-audit.yml | 9 +- .github/workflows/mirror.yml | 1 + .github/workflows/openssf-compliance.yml | 13 +- .github/workflows/pages.yml | 9 +- .github/workflows/proof-safety.yml | 2 +- .github/workflows/push-email-notify.yml | 3 +- .github/workflows/quality.yml | 7 +- .github/workflows/release.yml | 11 +- .github/workflows/rhodibot.yml | 3 +- .github/workflows/runtime-policy.yml | 3 +- .github/workflows/rust-ci.yml | 3 + .github/workflows/scorecard.yml | 3 +- .github/workflows/secret-scanner.yml | 1 + .github/workflows/security-policy.yml | 3 +- .github/workflows/static-analysis-gate.yml | 23 +- .github/workflows/wellknown-enforcement.yml | 3 +- .github/workflows/workflow-linter.yml | 3 +- .machine_readable/contractiles/Justfile | 6 +- .machine_readable/contractiles/Mustfile.a2ml | 4 +- .../{6a2 => descriptiles}/0-AI-MANIFEST.a2ml | 0 .../{6a2 => descriptiles}/AGENTIC.a2ml | 0 .../{6a2 => descriptiles}/ECOSYSTEM.a2ml | 0 .../{6a2 => descriptiles}/META.a2ml | 0 .../{6a2 => descriptiles}/NEUROSYM.a2ml | 0 .../{6a2 => descriptiles}/PLAYBOOK.a2ml | 2 +- .../{6a2 => descriptiles}/README.adoc | 0 .../{6a2 => descriptiles}/STATE.a2ml | 0 .../anchor/0-AI-MANIFEST.a2ml | 0 .../{6a2 => descriptiles}/anchor/ANCHOR.a2ml | 0 .../anchor/ANCHOR_2026_05_21.a2ml | 0 .../{6a2 => descriptiles}/anchor/README.adoc | 0 .../self-validating/methodology-guard.k9.ncl | 2 +- 0-AI-MANIFEST.a2ml | 12 +- Justfile | 6 +- READINESS.adoc | 6 +- audits/assail-classifications.a2ml | 3 + crates/burrower-cli/src/main.rs | 72 +++-- crates/burrower-core/src/attempt.rs | 86 ++++-- crates/burrower-core/src/goal.rs | 39 ++- crates/burrower-core/src/ledger.rs | 14 +- crates/burrower-core/src/lib.rs | 32 +-- crates/burrower-core/src/oracle.rs | 50 +++- crates/burrower-core/src/ranking.rs | 16 +- crates/burrower-core/src/serve.rs | 51 +++- crates/burrower-core/src/specialist.rs | 267 +++++++++++++----- crates/burrower-core/tests/live_isabelle.rs | 3 +- docs/governance/CRG-AUDIT-TEMPLATE.adoc | 8 +- docs/governance/MAINTENANCE-CHECKLIST.a2ml | 1 + 60 files changed, 695 insertions(+), 267 deletions(-) rename .machine_readable/{6a2 => descriptiles}/0-AI-MANIFEST.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/AGENTIC.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/ECOSYSTEM.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/META.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/NEUROSYM.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/PLAYBOOK.a2ml (93%) rename .machine_readable/{6a2 => descriptiles}/README.adoc (100%) rename .machine_readable/{6a2 => descriptiles}/STATE.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/anchor/0-AI-MANIFEST.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/anchor/ANCHOR.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/anchor/ANCHOR_2026_05_21.a2ml (100%) rename .machine_readable/{6a2 => descriptiles}/anchor/README.adoc (100%) diff --git a/.envrc b/.envrc index d7c7d2f..b2128b4 100644 --- a/.envrc +++ b/.envrc @@ -20,7 +20,7 @@ fi export PROJECT_NAME="Proof Burrower" export RSR_TIER="infrastructure" # export DATABASE_URL="..." -# export API_KEY="..." +# Load credentials through the ignored .env file below. # Source .env if it exists (gitignored) dotenv_if_exists diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index fa47800..d41487c 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -3,15 +3,155 @@ # Docs: https://gh.io/actions-lockfile version: 'v0.0.2' workflows: + '.github/workflows/boj-build.yml': + - 'actions/checkout@v6.0.2' + '.github/workflows/codeql.yml': + - 'actions/checkout@v6.0.2' + - 'github/codeql-action@v4.34.0' + '.github/workflows/dependabot-automerge.yml': + - 'dependabot/fetch-metadata@v2.2.0' + '.github/workflows/dogfood-gate.yml': + - 'actions/checkout@v4.3.1' + - 'hyperpolymath/a2ml-ecosystem@main' + - 'hyperpolymath/k9-ecosystem@main' + '.github/workflows/guix-nix-policy.yml': + - 'actions/checkout@v6.0.2' + '.github/workflows/instant-sync.yml': + - 'peter-evans/repository-dispatch@v4.0.1' + '.github/workflows/main-estate-audit.yml': + - 'actions/checkout@v4.4.0' + - 'hyperpolymath/cicd-suite@main' + '.github/workflows/openssf-compliance.yml': + - 'actions/checkout@v4.3.1' + '.github/workflows/pages.yml': + - 'actions/checkout@v4.4.0' + - 'actions/deploy-pages@v4.0.5' + - 'actions/upload-pages-artifact@v3.0.1' '.github/workflows/proof-safety.yml': - 'actions/checkout@v7.0.1' - 'swatinem/rust-cache@v2.9.2' + '.github/workflows/push-email-notify.yml': + - 'hyperpolymath/smtp-notify-action@v0.2.0' + '.github/workflows/quality.yml': + - 'actions/checkout@v6.0.2' + - 'editorconfig-checker/action-editorconfig-checker@v2.1.0' + '.github/workflows/release.yml': + - 'actions/checkout@v6.0.2' + - 'actions/upload-artifact@v4.6.2' + - 'softprops/action-gh-release@v2.5.0' + '.github/workflows/rhodibot.yml': + - 'actions/checkout@v4.3.1' + '.github/workflows/runtime-policy.yml': + - 'actions/checkout@v6.0.2' + '.github/workflows/security-policy.yml': + - 'actions/checkout@v6.0.2' + '.github/workflows/static-analysis-gate.yml': + - 'actions/checkout@v6.0.2' + - 'actions/download-artifact@v4.1.8' + - 'actions/upload-artifact@v4.6.2' + - 'erlef/setup-beam@v1.20.4' + '.github/workflows/wellknown-enforcement.yml': + - 'actions/checkout@v6.0.2' + '.github/workflows/workflow-linter.yml': + - 'actions/checkout@v6.0.2' dependencies: + 'actions/checkout@v4.3.1': + ref: 'v4.3.1' + commit: 'sha1-34e114876b0b11c390a56381ad16ebd13914f8d5' + owner_id: 44036562 + repo_id: 197814629 + 'actions/checkout@v4.4.0': + ref: 'v4.4.0' + commit: 'sha1-11d5960a326750d5838078e36cf38b85af677262' + owner_id: 44036562 + repo_id: 197814629 + 'actions/checkout@v6.0.2': + ref: 'v6.0.2' + commit: 'sha1-de0fac2e4500dabe0009e67214ff5f5447ce83dd' + owner_id: 44036562 + repo_id: 197814629 'actions/checkout@v7.0.1': ref: 'v7.0.1' commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1' owner_id: 44036562 repo_id: 197814629 + 'actions/deploy-pages@v4.0.5': + ref: 'v4.0.5' + commit: 'sha1-d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e' + owner_id: 44036562 + repo_id: 438112499 + 'actions/download-artifact@v4.1.8': + ref: 'v4.1.8' + commit: 'sha1-fa0a91b85d4f404e444e00e005971372dc801d16' + owner_id: 44036562 + repo_id: 192626254 + 'actions/upload-artifact@v4': + ref: 'v4' + commit: 'sha1-ea165f8d65b6e75b540449e92b4886f43607fa02' + owner_id: 44036562 + repo_id: 192625955 + 'actions/upload-artifact@v4.6.2': + ref: 'v4.6.2' + commit: 'sha1-ea165f8d65b6e75b540449e92b4886f43607fa02' + owner_id: 44036562 + repo_id: 192625955 + 'actions/upload-pages-artifact@v3.0.1': + ref: 'v3.0.1' + commit: 'sha1-56afc609e74202658d3ffba0e8f6dda462b719fa' + owner_id: 44036562 + repo_id: 496012378 + uses: + - 'actions/upload-artifact@v4' + 'dependabot/fetch-metadata@v2.2.0': + ref: 'v2.2.0' + commit: 'sha1-dbb049abf0d677abbd7f7eee0375145b417fdd34' + owner_id: 27347476 + repo_id: 371068214 + 'editorconfig-checker/action-editorconfig-checker@v2.1.0': + ref: 'v2.1.0' + commit: 'sha1-4b6cd6190d435e7e084fb35e36a096e98506f7b9' + owner_id: 26415196 + repo_id: 297874902 + 'erlef/setup-beam@v1.20.4': + ref: 'v1.20.4' + commit: 'sha1-e6d7c94229049569db56a7ad5a540c051a010af9' + owner_id: 47606891 + repo_id: 331103973 + 'github/codeql-action@v4.34.0': + ref: 'v4.34.0' + commit: 'sha1-c6f931105cb2c34c8f901cc885ba1e2e259cf745' + owner_id: 9919 + repo_id: 259445878 + 'hyperpolymath/a2ml-ecosystem@main': + ref: 'main' + commit: 'sha1-aa4b836bd969df2bc58128cb8e3d20bbc88d5e79' + owner_id: 6759885 + repo_id: 1275649586 + 'hyperpolymath/cicd-suite@main': + ref: 'main' + commit: 'sha1-fc64172aa53e85289d5d7d6e15c2435a867cc1c9' + owner_id: 6759885 + repo_id: 1326697643 + 'hyperpolymath/k9-ecosystem@main': + ref: 'main' + commit: 'sha1-89f3c2702f4f650a92aa7411502f38da06abd562' + owner_id: 6759885 + repo_id: 1275650185 + 'hyperpolymath/smtp-notify-action@v0.2.0': + ref: 'v0.2.0' + commit: 'sha1-ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7' + owner_id: 6759885 + repo_id: 1352485172 + 'peter-evans/repository-dispatch@v4.0.1': + ref: 'v4.0.1' + commit: 'sha1-28959ce8df70de7be546dd1250a005dd32156697' + owner_id: 18365890 + repo_id: 220359305 + 'softprops/action-gh-release@v2.5.0': + ref: 'v2.5.0' + commit: 'sha1-a06a81a03ee405af7f2048a818ed3f03bbf83c7b' + owner_id: 2242 + repo_id: 204253808 'swatinem/rust-cache@v2.9.2': ref: 'v2.9.2' commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6' diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml index a0ab782..a064934 100644 --- a/.github/workflows/boj-build.yml +++ b/.github/workflows/boj-build.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # # OPTIONAL: BoJ Server Build Trigger # This workflow notifies a BoJ Server instance when code is pushed. @@ -19,7 +20,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Trigger BoJ Server (Casket/ssg-mcp) env: BOJ_URL: ${{ secrets.BOJ_SERVER_URL || vars.BOJ_SERVER_URL }} diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 46f9840..eeb0867 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: CodeQL Security Analysis on: push: @@ -36,13 +37,13 @@ jobs: build-mode: none steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Initialize CodeQL - uses: github/codeql-action/init@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3 + uses: github/codeql-action/init@v4.34.0 with: languages: ${{ matrix.language }} build-mode: ${{ matrix.build-mode }} - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@c6f931105cb2c34c8f901cc885ba1e2e259cf745 # v3 + uses: github/codeql-action/analyze@v4.34.0 with: category: "/language:${{ matrix.language }}" diff --git a/.github/workflows/dependabot-automerge.yml b/.github/workflows/dependabot-automerge.yml index e520ce0..f7a9261 100644 --- a/.github/workflows/dependabot-automerge.yml +++ b/.github/workflows/dependabot-automerge.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # # dependabot-automerge.yml — enable GitHub's native auto-merge on # Dependabot pull requests that match a declared severity / ecosystem @@ -52,7 +53,7 @@ jobs: steps: - name: Fetch Dependabot metadata id: meta - uses: dependabot/fetch-metadata@dbb049abf0d677abbd7f7eee0375145b417fdd34 # v2.2.0 + uses: dependabot/fetch-metadata@v2.2.0 with: github-token: ${{ secrets.GITHUB_TOKEN }} # --- Policy gate ------------------------------------------------------- diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index a1e38b5..be9fef1 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # dogfood-gate.yml — Hyperpolymath Dogfooding Quality Gate @@ -27,7 +28,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Check for A2ML files id: detect @@ -40,7 +41,7 @@ jobs: - name: Validate A2ML manifests if: steps.detect.outputs.count > 0 - uses: hyperpolymath/a2ml-ecosystem/validate-action@aa4b836bd969df2bc58128cb8e3d20bbc88d5e79 # main + uses: hyperpolymath/a2ml-ecosystem/validate-action@main with: path: '.' strict: 'false' @@ -72,7 +73,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Check for K9 files id: detect @@ -89,7 +90,7 @@ jobs: - name: Validate K9 contracts if: steps.detect.outputs.k9_count > 0 - uses: hyperpolymath/k9-ecosystem/validate-action@89f3c2702f4f650a92aa7411502f38da06abd562 # main + uses: hyperpolymath/k9-ecosystem/validate-action@main with: path: '.' strict: 'false' @@ -122,7 +123,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Scan for invisible characters id: lint @@ -187,7 +188,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Check for Groove manifest id: groove @@ -246,7 +247,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Check and validate eclexiaiser manifest id: eclex @@ -312,7 +313,7 @@ jobs: steps: - name: Checkout repository - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 - name: Generate dogfooding scorecard run: | diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 931cef9..80d53a1 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Governance on: diff --git a/.github/workflows/guix-nix-policy.yml b/.github/workflows/guix-nix-policy.yml index 7f4a7b9..1e5dc24 100644 --- a/.github/workflows/guix-nix-policy.yml +++ b/.github/workflows/guix-nix-policy.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Guix/Nix Package Policy on: push: @@ -20,7 +21,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 - name: Enforce Guix primary / Nix fallback run: | # Check for package manager files diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 3c08e0a..6e8ef44 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Hypatia Security Scan on: diff --git a/.github/workflows/instant-sync.yml b/.github/workflows/instant-sync.yml index 37618c4..ebdbbde 100644 --- a/.github/workflows/instant-sync.yml +++ b/.github/workflows/instant-sync.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # Instant Forge Sync - Triggers propagation to all forges on push/release name: Instant Sync on: @@ -15,7 +16,7 @@ jobs: timeout-minutes: 15 steps: - name: Trigger Propagation - uses: peter-evans/repository-dispatch@28959ce8df70de7be546dd1250a005dd32156697 # v3 + uses: peter-evans/repository-dispatch@v4.0.1 with: token: ${{ secrets.FARM_DISPATCH_TOKEN }} repository: hyperpolymath/.git-private-farm diff --git a/.github/workflows/label-triage.yml b/.github/workflows/label-triage.yml index 9886e92..fc79947 100644 --- a/.github/workflows/label-triage.yml +++ b/.github/workflows/label-triage.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Label Triage # Classify newly-filed issues against the estate label taxonomy. diff --git a/.github/workflows/labels.yml b/.github/workflows/labels.yml index c80b676..af34c6b 100644 --- a/.github/workflows/labels.yml +++ b/.github/workflows/labels.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Labels # Applies the canonical estate label set from .github/labels.json. diff --git a/.github/workflows/main-estate-audit.yml b/.github/workflows/main-estate-audit.yml index b602e97..05a1963 100755 --- a/.github/workflows/main-estate-audit.yml +++ b/.github/workflows/main-estate-audit.yml @@ -1,3 +1,7 @@ +# SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. +# This workflow is managed by gh actions-lock. + name: Central Estate CI/CD Audit on: @@ -6,11 +10,14 @@ on: pull_request: branches: [ "main" ] +permissions: + contents: read + jobs: estate-audit: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v4 + - uses: actions/checkout@v4.4.0 - name: Required Files Gate uses: hyperpolymath/cicd-suite/actions/required-files-check@main diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml index bd5da3d..c2149a3 100644 --- a/.github/workflows/mirror.yml +++ b/.github/workflows/mirror.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Mirror to Git Forges on: push: diff --git a/.github/workflows/openssf-compliance.yml b/.github/workflows/openssf-compliance.yml index 5d7b3d3..86a28c7 100644 --- a/.github/workflows/openssf-compliance.yml +++ b/.github/workflows/openssf-compliance.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # OpenSSF Best Practices compliance gate — blocks PRs and pushes that lack # required files or still contain unfilled placeholder tokens. name: OpenSSF Compliance @@ -18,7 +19,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + - uses: actions/checkout@v4.3.1 with: persist-credentials: false - name: Check SECURITY.md exists and has substance @@ -67,11 +68,11 @@ jobs: exit 1 fi - if [ ! -f ".machine_readable/STATE.a2ml" ]; then - echo "::error::.machine_readable/STATE.a2ml is required" + if [ ! -f ".machine_readable/descriptiles/STATE.a2ml" ]; then + echo "::error::.machine_readable/descriptiles/STATE.a2ml is required" exit 1 fi - echo ".machine_readable/STATE.a2ml: OK" + echo ".machine_readable/descriptiles/STATE.a2ml: OK" - name: Check CHANGELOG exists run: | if [ ! -f "CHANGELOG.md" ] && [ ! -f "CHANGELOG.adoc" ] && [ ! -f "CHANGES.md" ]; then @@ -87,8 +88,8 @@ jobs: # Collect all required files that exist for f in SECURITY.md SECURITY.adoc .github/SECURITY.md LICENSE LICENSE.txt \ CONTRIBUTING.md CONTRIBUTING.adoc README.md README.adoc \ - .machine_readable/STATE.a2ml .machine_readable/META.a2ml \ - .machine_readable/ECOSYSTEM.a2ml CHANGELOG.md CHANGELOG.adoc; do + .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml \ + .machine_readable/descriptiles/ECOSYSTEM.a2ml CHANGELOG.md CHANGELOG.adoc; do [ -f "$f" ] && REQUIRED_FILES="$REQUIRED_FILES $f" done diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index 0273437..adaf752 100755 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: GitHub Pages (Ddraig SSG) on: push: @@ -20,9 +21,9 @@ jobs: image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff steps: - name: Checkout Site - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4 + uses: actions/checkout@v4.4.0 - name: Checkout Ddraig SSG - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4 + uses: actions/checkout@v4.4.0 with: repository: hyperpolymath/ddraig-ssg path: .ddraig-ssg @@ -39,7 +40,7 @@ jobs: fi ./.ddraig-ssg/build/exec/ddraig build src _site https://hyperpolymath.github.io/${GITHUB_REPOSITORY#*/} - name: Upload artifact - uses: actions/upload-pages-artifact@56afc609e74202658d3ffba0e8f6dda462b719fa # v3 + uses: actions/upload-pages-artifact@v3.0.1 with: path: '_site' deploy: @@ -52,4 +53,4 @@ jobs: steps: - name: Deploy to GitHub Pages id: deployment - uses: actions/deploy-pages@d6db90164ac5ed86f2b6aed7e0febac5b3c0c03e # v4 + uses: actions/deploy-pages@v4.0.5 diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml index 0dde912..932a54d 100644 --- a/.github/workflows/proof-safety.yml +++ b/.github/workflows/proof-safety.yml @@ -1,5 +1,5 @@ -# This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Proof Safety on: pull_request: diff --git a/.github/workflows/push-email-notify.yml b/.github/workflows/push-email-notify.yml index 0689291..56f2d08 100644 --- a/.github/workflows/push-email-notify.yml +++ b/.github/workflows/push-email-notify.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # Dormant push-email notification. ARMED by setting the repo variable # PUSH_EMAIL_ENABLED=true (the single on/off switch). Addresses are pre-filled; # sending needs the org SMTP secrets (SMTP_HOST/PORT/USER/PASS). Inherited by @@ -39,7 +40,7 @@ jobs: timeout-minutes: 5 steps: - name: Send push notification email - uses: hyperpolymath/smtp-notify-action@ede1191ef6ff3ac02c4f4d9efdf837ee517e11d7 # v0.2.0 + uses: hyperpolymath/smtp-notify-action@v0.2.0 with: server_address: ${{ secrets.SMTP_HOST }} server_port: ${{ secrets.SMTP_PORT }} diff --git a/.github/workflows/quality.yml b/.github/workflows/quality.yml index cbf2855..7fe239c 100644 --- a/.github/workflows/quality.yml +++ b/.github/workflows/quality.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Code Quality on: push: @@ -20,7 +21,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 - name: Check file permissions run: | find . -type f -perm /111 -name "*.sh" | head -10 || true @@ -32,7 +33,7 @@ jobs: run: | find . -type f -size +1M -not -path "./.git/*" | head -10 || echo "No large files" - name: EditorConfig check - uses: editorconfig-checker/action-editorconfig-checker@4b6cd6190d435e7e084fb35e36a096e98506f7b9 # v2.1.0 + uses: editorconfig-checker/action-editorconfig-checker@v2.1.0 continue-on-error: true docs: runs-on: ubuntu-latest @@ -40,7 +41,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 - name: Check documentation run: | MISSING="" diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index e675c5d..0d7f9b0 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # Release workflow — triggered by version tags (v*). @@ -20,7 +21,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 - name: Detect project type and build id: build run: | @@ -81,7 +82,7 @@ jobs: changelog: ${{ steps.cliff.outputs.content }} version: ${{ steps.version.outputs.version }} steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Extract version from tag @@ -106,7 +107,7 @@ jobs: run: | git cliff --output CHANGELOG.md - name: Upload updated CHANGELOG.md - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2 + uses: actions/upload-artifact@v4.6.2 with: name: changelog path: CHANGELOG.md @@ -119,14 +120,14 @@ jobs: permissions: contents: write steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 # TODO: Download build artifacts if uploading to the release # - uses: actions/download-artifact@v4 # with: # name: release-artifacts # path: artifacts/ - name: Create GitHub Release - uses: softprops/action-gh-release@a06a81a03ee405af7f2048a818ed3f03bbf83c7b # v2 + uses: softprops/action-gh-release@v2.5.0 with: body: ${{ needs.changelog.outputs.changelog }} draft: false diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml index 15b299e..be9f22c 100644 --- a/.github/workflows/rhodibot.yml +++ b/.github/workflows/rhodibot.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # rhodibot.yml — Automated RSR compliance enforcement # # Reads root-hygiene rules and auto-fixes what it can: @@ -28,7 +29,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout - uses: actions/checkout@34e114876b0b11c390a56381ad16ebd13914f8d5 # v4 + uses: actions/checkout@v4.3.1 with: fetch-depth: 1 - name: Rhodibot — Scan and Fix diff --git a/.github/workflows/runtime-policy.yml b/.github/workflows/runtime-policy.yml index a376c70..bb83716 100644 --- a/.github/workflows/runtime-policy.yml +++ b/.github/workflows/runtime-policy.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # Runtime and package-manager policy check. # # Authority: hyperpolymath/standards LANGUAGE-POLICY.adoc §1. @@ -36,7 +37,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 - name: Report runtime tier and reject mixed toolchains run: | diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index e4fde20..cd4de61 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # Rust CI — thin wrapper calling the shared estate reusable in # hyperpolymath/standards. Configure once, propagate everywhere. # See: docs/CI-REUSABLE-WORKFLOWS.adoc in standards. @@ -14,3 +15,5 @@ permissions: jobs: rust-ci: uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@412a7031577112b31ee287cc6060179d638d6500 + with: + enable_audit: true diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 8511abf..e5f7123 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: OSSF Scorecard on: @@ -13,7 +14,7 @@ permissions: id-token: write jobs: scorecard: - uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@7fdc2705df74b4e352d2a1cde3e87a5923fdf329 + uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd permissions: contents: read security-events: write diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 7811bd5..d0c48df 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Secret Scanner on: pull_request: diff --git a/.github/workflows/security-policy.yml b/.github/workflows/security-policy.yml index 708fca5..6b44231 100644 --- a/.github/workflows/security-policy.yml +++ b/.github/workflows/security-policy.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Security Policy on: push: @@ -20,7 +21,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 - name: Security checks run: | FAILED=false diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml index bda5664..945c474 100644 --- a/.github/workflows/static-analysis-gate.yml +++ b/.github/workflows/static-analysis-gate.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # Static Analysis Gate — Required by branch protection rules. # Runs panic-attack and hypatia, deposits findings for gitbot-fleet learning. name: Static Analysis Gate @@ -20,7 +21,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Install panic-attack (if available) @@ -117,7 +118,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload panic-attack findings - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 + uses: actions/upload-artifact@v4.6.2 with: name: panic-attack-findings path: panic-attack-findings.json @@ -136,13 +137,13 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Setup Elixir for Hypatia scanner id: beam continue-on-error: true - uses: erlef/setup-beam@e6d7c94229049569db56a7ad5a540c051a010af9 # v1.18.2 + uses: erlef/setup-beam@v1.20.4 with: elixir-version: '1.19.4' otp-version: '28.3' @@ -243,7 +244,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: Hypatia scanner not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload hypatia findings - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 + uses: actions/upload-artifact@v4.6.2 with: name: hypatia-findings path: hypatia-findings.json @@ -262,7 +263,7 @@ jobs: timeout-minutes: 15 steps: - name: Checkout repository - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 with: fetch-depth: 0 - name: Install panic-attack (if available) @@ -324,7 +325,7 @@ jobs: echo "" >> "$GITHUB_STEP_SUMMARY" echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" - name: Upload bridge report - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 + uses: actions/upload-artifact@v4.6.2 with: name: bridge-report path: bridge-report.json @@ -346,17 +347,17 @@ jobs: if: always() steps: - name: Download panic-attack findings - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4 + uses: actions/download-artifact@v4.1.8 with: name: panic-attack-findings path: findings/ - name: Download hypatia findings - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4 + uses: actions/download-artifact@v4.1.8 with: name: hypatia-findings path: findings/ - name: Download bridge report - uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4 + uses: actions/download-artifact@v4.1.8 with: name: bridge-report path: findings/ @@ -416,7 +417,7 @@ jobs: echo "medium=$MEDIUM" >> "$GITHUB_OUTPUT" echo "low=$LOW" >> "$GITHUB_OUTPUT" - name: Upload unified findings (fleet scanner picks these up) - uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4 + uses: actions/upload-artifact@v4.6.2 with: name: unified-findings path: findings/unified-findings.json diff --git a/.github/workflows/wellknown-enforcement.yml b/.github/workflows/wellknown-enforcement.yml index f9988c1..d7db44f 100644 --- a/.github/workflows/wellknown-enforcement.yml +++ b/.github/workflows/wellknown-enforcement.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. name: Well-Known Standards (RFC 9116 + RSR) on: push: @@ -23,7 +24,7 @@ jobs: permissions: contents: read steps: - - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + - uses: actions/checkout@v6.0.2 - name: RFC 9116 security.txt validation run: | SECTXT="" diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml index fbbc52f..4ef23f7 100644 --- a/.github/workflows/workflow-linter.yml +++ b/.github/workflows/workflow-linter.yml @@ -1,4 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 +# This workflow is managed by gh actions-lock. # workflow-linter.yml - Validates GitHub workflows against RSR security standards # This workflow can be copied to other repos for consistent enforcement name: Workflow Security Linter @@ -25,7 +26,7 @@ jobs: steps: - name: Checkout - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + uses: actions/checkout@v6.0.2 - name: Check SPDX Headers run: | diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile index daf017a..9852e95 100644 --- a/.machine_readable/contractiles/Justfile +++ b/.machine_readable/contractiles/Justfile @@ -345,7 +345,7 @@ verify-template: fi # Check for empty SCM files - for f in .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml; do + for f in .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml .machine_readable/descriptiles/ECOSYSTEM.a2ml; do if [ -f "$f" ] && grep -q '{{'{{'}}' "$f" 2>/dev/null; then echo "⚠ $f still has template placeholders" FOUND=1 @@ -404,9 +404,9 @@ self-assess: done if [ -d ".machine_readable/6a2" ]; then - echo " ✓ .machine_readable/6a2/ — KEEP (SCM checkpoint files)" + echo " ✓ .machine_readable/descriptiles/ — KEEP (SCM checkpoint files)" else - echo " ✗ .machine_readable/6a2/ — MISSING (RSR violation!)" + echo " ✗ .machine_readable/descriptiles/ — MISSING (RSR violation!)" fi if [ -d ".github/workflows" ]; then diff --git a/.machine_readable/contractiles/Mustfile.a2ml b/.machine_readable/contractiles/Mustfile.a2ml index 55f8ab4..611ef25 100644 --- a/.machine_readable/contractiles/Mustfile.a2ml +++ b/.machine_readable/contractiles/Mustfile.a2ml @@ -63,12 +63,12 @@ hooks fail if any check fails. ### six-directory-present - description: 6a2 directory exists with required files -- run: test -d .machine_readable/6a2 && test -f .machine_readable/6a2/META.a2ml && test -f .machine_readable/6a2/ECOSYSTEM.a2ml && test -f .machine_readable/6a2/STATE.a2ml && test -f .machine_readable/6a2/PLAYBOOK.a2ml && test -f .machine_readable/6a2/AGENTIC.a2ml && test -f .machine_readable/6a2/NEUROSYM.a2ml +- run: test -d .machine_readable/6a2 && test -f .machine_readable/descriptiles/META.a2ml && test -f .machine_readable/descriptiles/ECOSYSTEM.a2ml && test -f .machine_readable/descriptiles/STATE.a2ml && test -f .machine_readable/descriptiles/PLAYBOOK.a2ml && test -f .machine_readable/descriptiles/AGENTIC.a2ml && test -f .machine_readable/descriptiles/NEUROSYM.a2ml - severity: critical ### anchors-directory - description: anchors directory exists in 6a2 -- run: test -d .machine_readable/6a2/anchors +- run: test -d .machine_readable/descriptiles/anchors - severity: warning ### self-validating-structure diff --git a/.machine_readable/6a2/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/0-AI-MANIFEST.a2ml similarity index 100% rename from .machine_readable/6a2/0-AI-MANIFEST.a2ml rename to .machine_readable/descriptiles/0-AI-MANIFEST.a2ml diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/descriptiles/AGENTIC.a2ml similarity index 100% rename from .machine_readable/6a2/AGENTIC.a2ml rename to .machine_readable/descriptiles/AGENTIC.a2ml diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/descriptiles/ECOSYSTEM.a2ml similarity index 100% rename from .machine_readable/6a2/ECOSYSTEM.a2ml rename to .machine_readable/descriptiles/ECOSYSTEM.a2ml diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/descriptiles/META.a2ml similarity index 100% rename from .machine_readable/6a2/META.a2ml rename to .machine_readable/descriptiles/META.a2ml diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/descriptiles/NEUROSYM.a2ml similarity index 100% rename from .machine_readable/6a2/NEUROSYM.a2ml rename to .machine_readable/descriptiles/NEUROSYM.a2ml diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/descriptiles/PLAYBOOK.a2ml similarity index 93% rename from .machine_readable/6a2/PLAYBOOK.a2ml rename to .machine_readable/descriptiles/PLAYBOOK.a2ml index 9b97cca..30cc636 100644 --- a/.machine_readable/6a2/PLAYBOOK.a2ml +++ b/.machine_readable/descriptiles/PLAYBOOK.a2ml @@ -14,7 +14,7 @@ notes = "This repo is a template and is not 'deployed' in the traditional sense. [incident-response] steps = [ "1. Read 0-AI-MANIFEST.a2ml for canonical locations.", - "2. Check .machine_readable/6a2/STATE.a2ml for active blockers.", + "2. Check .machine_readable/descriptiles/STATE.a2ml for active blockers.", "3. Run `just validate-rsr` to check for standards regressions.", "4. If standards have drifted, consult developer-ecosystem/standards for the source of truth.", ] diff --git a/.machine_readable/6a2/README.adoc b/.machine_readable/descriptiles/README.adoc similarity index 100% rename from .machine_readable/6a2/README.adoc rename to .machine_readable/descriptiles/README.adoc diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/descriptiles/STATE.a2ml similarity index 100% rename from .machine_readable/6a2/STATE.a2ml rename to .machine_readable/descriptiles/STATE.a2ml diff --git a/.machine_readable/6a2/anchor/0-AI-MANIFEST.a2ml b/.machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml similarity index 100% rename from .machine_readable/6a2/anchor/0-AI-MANIFEST.a2ml rename to .machine_readable/descriptiles/anchor/0-AI-MANIFEST.a2ml diff --git a/.machine_readable/6a2/anchor/ANCHOR.a2ml b/.machine_readable/descriptiles/anchor/ANCHOR.a2ml similarity index 100% rename from .machine_readable/6a2/anchor/ANCHOR.a2ml rename to .machine_readable/descriptiles/anchor/ANCHOR.a2ml diff --git a/.machine_readable/6a2/anchor/ANCHOR_2026_05_21.a2ml b/.machine_readable/descriptiles/anchor/ANCHOR_2026_05_21.a2ml similarity index 100% rename from .machine_readable/6a2/anchor/ANCHOR_2026_05_21.a2ml rename to .machine_readable/descriptiles/anchor/ANCHOR_2026_05_21.a2ml diff --git a/.machine_readable/6a2/anchor/README.adoc b/.machine_readable/descriptiles/anchor/README.adoc similarity index 100% rename from .machine_readable/6a2/anchor/README.adoc rename to .machine_readable/descriptiles/anchor/README.adoc diff --git a/.machine_readable/self-validating/methodology-guard.k9.ncl b/.machine_readable/self-validating/methodology-guard.k9.ncl index 9e8d062..616493d 100644 --- a/.machine_readable/self-validating/methodology-guard.k9.ncl +++ b/.machine_readable/self-validating/methodology-guard.k9.ncl @@ -43,7 +43,7 @@ let methodology_guard = { state_not_template = { description = "STATE.a2ml must not contain template placeholders", severity = "warning", - file = ".machine_readable/6a2/STATE.a2ml", + file = ".machine_readable/descriptiles/STATE.a2ml", reject_patterns = ["{{PLACEHOLDER}}", "Proof Burrower", "rsr-template-repo"], }, diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index 67602b1..1fe6bd3 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -11,9 +11,9 @@ This is the AI manifest for **rsr-template-repo**. It declares: ## CANONICAL LOCATIONS (UNIVERSAL RULE) -### Machine-Readable Metadata: `.machine_readable/6a2/` ONLY +### Machine-Readable Metadata: `.machine_readable/descriptiles/` ONLY -These 6 A2ML files MUST exist in `.machine_readable/6a2/` directory ONLY: +These 6 A2ML files MUST exist in `.machine_readable/descriptiles/` directory ONLY: 1. **STATE.a2ml** - Project state, progress, blockers 2. **META.a2ml** - Architecture decisions, governance 3. **ECOSYSTEM.a2ml** - Position in ecosystem, relationships @@ -41,7 +41,7 @@ Bot-specific instructions for: ## CORE INVARIANTS 1. **No A2ML duplication** - Root and `.machine_readable/` must NOT contain 6A2 files. -2. **Single source of truth** - `.machine_readable/6a2/` is authoritative. +2. **Single source of truth** - `.machine_readable/descriptiles/` is authoritative. 3. **No stale metadata** - If root A2ML files exist, they are OUT OF DATE. 4. **License consistency** - All code MPL-2.0 unless platform requires MPL-2.0. 5. **Author attribution** - Always "Jonathan D.A. Jewell ". @@ -72,19 +72,19 @@ rsr-template-repo/ ### on-enter (Session Start) 1. Read and acknowledge this manifest. -2. Read `.machine_readable/6a2/STATE.a2ml` for current status and v2 phase. +2. Read `.machine_readable/descriptiles/STATE.a2ml` for current status and v2 phase. 3. State understanding of canonical locations. ### on-exit (Session End) -1. Update `.machine_readable/6a2/STATE.a2ml` (v2 format). +1. Update `.machine_readable/descriptiles/STATE.a2ml` (v2 format). 2. Summarize outcomes and record new blockers if any. ## ATTESTATION PROOF After reading this file, demonstrate understanding by stating: -**"I have read the AI manifest. A2ML files are located in `.machine_readable/6a2/` ONLY, bot directives in `.bot_directives/`, and I will not create duplicate files in the root directory."** +**"I have read the AI manifest. A2ML files are located in `.machine_readable/descriptiles/` ONLY, bot directives in `.bot_directives/`, and I will not create duplicate files in the root directory."** ## META diff --git a/Justfile b/Justfile index 253a1aa..c5e9c08 100644 --- a/Justfile +++ b/Justfile @@ -346,7 +346,7 @@ verify-template: fi # Check for empty SCM files - for f in .machine_readable/6a2/STATE.a2ml .machine_readable/6a2/META.a2ml .machine_readable/6a2/ECOSYSTEM.a2ml; do + for f in .machine_readable/descriptiles/STATE.a2ml .machine_readable/descriptiles/META.a2ml .machine_readable/descriptiles/ECOSYSTEM.a2ml; do if [ -f "$f" ] && grep -q '{{'{{'}}' "$f" 2>/dev/null; then echo "⚠ $f still has template placeholders" FOUND=1 @@ -405,9 +405,9 @@ self-assess: done if [ -d ".machine_readable/6a2" ]; then - echo " ✓ .machine_readable/6a2/ — KEEP (SCM checkpoint files)" + echo " ✓ .machine_readable/descriptiles/ — KEEP (SCM checkpoint files)" else - echo " ✗ .machine_readable/6a2/ — MISSING (RSR violation!)" + echo " ✗ .machine_readable/descriptiles/ — MISSING (RSR violation!)" fi if [ -d ".github/workflows" ]; then diff --git a/READINESS.adoc b/READINESS.adoc index 210e67d..d216bce 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -36,7 +36,7 @@ ____ *Evidence gates (v2.0 is stricter than v1.0):* * *D*: RSR-compliant + per-capability tests + documented scope. Test -matrix must cite counts and live in `+.machine_readable/6a2/STATE.a2ml+` +matrix must cite counts and live in `+.machine_readable/descriptiles/STATE.a2ml+` or CI. * *C*: All of D, plus active dogfooding in home context with *no known home-context failures over an evidence window*, plus *deep per-file and @@ -63,7 +63,7 @@ Below B, any publication must be explicitly abstract or provisional. [width="100%",cols="36%,30%,34%",options="header",] |=== |Metric |Value |Source -|Test count |__ |`+.machine_readable/6a2/STATE.a2ml+` or CI +|Test count |__ |`+.machine_readable/descriptiles/STATE.a2ml+` or CI |Formal-verification posture |__ |grep of proof dirs @@ -200,7 +200,7 @@ assessment>_. from `+rsr-template-repo/docs/governance/CRG-AUDIT-TEMPLATE.adoc+`). * `+docs/practice/DOGFOOD-LOG.adoc+` — dated dogfood evidence (required for C). -* `+.machine_readable/6a2/STATE.a2ml+` — authoritative state (canonical +* `+.machine_readable/descriptiles/STATE.a2ml+` — authoritative state (canonical keys `+[dogfooding-status]+`, `+[external-targets]+`, `+[issues-fed-back]+`, `+[field-signal]+`). diff --git a/audits/assail-classifications.a2ml b/audits/assail-classifications.a2ml index e812b5c..1b3e468 100644 --- a/audits/assail-classifications.a2ml +++ b/audits/assail-classifications.a2ml @@ -1,4 +1,7 @@ %A2ML +# SPDX-License-Identifier: MPL-2.0 +project = "proof-burrower" +schema_version = "1.0" - suppression: file: 'affinescript/tools/affine-doc/assets/search.js' rule: 'DynamicCodeExecution' diff --git a/crates/burrower-cli/src/main.rs b/crates/burrower-cli/src/main.rs index 6790953..83ff0e4 100644 --- a/crates/burrower-cli/src/main.rs +++ b/crates/burrower-cli/src/main.rs @@ -87,7 +87,10 @@ enum Cmd { /// The proof goal as a string. Quote it. goal: String, /// Path to the echidna binary. - #[arg(long, default_value = "/var/mnt/eclipse/repos/echidna/target/debug/echidna")] + #[arg( + long, + default_value = "/var/mnt/eclipse/repos/echidna/target/debug/echidna" + )] echidna: PathBuf, /// Per-attempt timeout (seconds), passed to `echidna prove -t`. #[arg(long, default_value_t = 60)] @@ -174,7 +177,10 @@ fn handle_ledger(cmd: LedgerCmd) -> Result<()> { LedgerCmd::Recent { path, limit } => { let l = Ledger::open(&path)?; let recs = l.recent(limit)?; - println!("Burrow Ledger — last {} record(s) (newest first):\n", recs.len()); + println!( + "Burrow Ledger — last {} record(s) (newest first):\n", + recs.len() + ); for r in recs { println!("[{}] {} · {}", r.timestamp, r.specialist, r.goal_hash); println!(" goal: {}", r.goal_excerpt); @@ -206,7 +212,10 @@ fn handle_ledger(cmd: LedgerCmd) -> Result<()> { ); } } - LedgerCmd::AntiPatterns { path, for_specialist } => { + LedgerCmd::AntiPatterns { + path, + for_specialist, + } => { let l = Ledger::open(&path)?; let antis = l.anti_patterns_for(&for_specialist)?; println!( @@ -215,11 +224,7 @@ fn handle_ledger(cmd: LedgerCmd) -> Result<()> { antis.len() ); for a in antis { - println!( - " · {} — {}", - a.pattern_extracted, - a.generalisation - ); + println!(" · {} — {}", a.pattern_extracted, a.generalisation); } } LedgerCmd::Digest { path } => { @@ -299,10 +304,13 @@ fn handle_attempt( ); // Emit a json result-shape consistent with the normal path. if format == "json" { - println!("{}", serde_json::json!({ - "blocked_by_oracle": true, - "verdict_kind": verdict.pattern_kind(), - })); + println!( + "{}", + serde_json::json!({ + "blocked_by_oracle": true, + "verdict_kind": verdict.pattern_kind(), + }) + ); } return Ok(()); } @@ -369,14 +377,30 @@ fn main() -> Result<()> { let cli = Cli::parse(); match cli.cmd { Cmd::Attempt { - goal, echidna, timeout, ledger, format, - project_root, sandbox, - oracle, oracle_descriptor, oracle_project, oracle_julia, + goal, + echidna, + timeout, + ledger, + format, + project_root, + sandbox, + oracle, + oracle_descriptor, + oracle_project, + oracle_julia, } => { return handle_attempt( - goal, echidna, timeout, ledger, format, - project_root, sandbox, - oracle, oracle_descriptor, oracle_project, oracle_julia, + goal, + echidna, + timeout, + ledger, + format, + project_root, + sandbox, + oracle, + oracle_descriptor, + oracle_project, + oracle_julia, ) } Cmd::Ledger { sub } => return handle_ledger(sub), @@ -401,16 +425,8 @@ fn main() -> Result<()> { let corpus = Corpus::load(&index)?; let parsed = parse_goal(&goal); let swarm = Swarm::new(); - let ledger_handle = ledger - .as_ref() - .map(|p| Ledger::open(p)) - .transpose()?; - let readings = swarm.route_with_ledger( - &parsed, - &corpus, - top, - ledger_handle.as_ref(), - ); + let ledger_handle = ledger.as_ref().map(|p| Ledger::open(p)).transpose()?; + let readings = swarm.route_with_ledger(&parsed, &corpus, top, ledger_handle.as_ref()); match format.as_str() { "json" => { println!("{}", serde_json::to_string_pretty(&readings)?); diff --git a/crates/burrower-core/src/attempt.rs b/crates/burrower-core/src/attempt.rs index 41e1b00..853c96e 100644 --- a/crates/burrower-core/src/attempt.rs +++ b/crates/burrower-core/src/attempt.rs @@ -93,11 +93,18 @@ impl Default for ProverConfig { /// Outcome of one proof attempt. #[derive(Debug, Clone, Serialize, Deserialize)] pub enum AttemptResult { - Succeeded { duration_ms: u64 }, - Failed { error: String, duration_ms: u64 }, + Succeeded { + duration_ms: u64, + }, + Failed { + error: String, + duration_ms: u64, + }, Timeout, /// Prover binary missing, probe-file write failed, etc. - Skipped { reason: String }, + Skipped { + reason: String, + }, } impl AttemptResult { @@ -199,9 +206,8 @@ fn extract_statement(goal_text: &str) -> String { if !quoted && (index == 0 || body[..index].ends_with(char::is_whitespace)) { let tail = &body[index..]; if ["by", "proof", ":="].iter().any(|marker| { - tail.strip_prefix(marker).is_some_and(|rest| { - rest.is_empty() || rest.starts_with(char::is_whitespace) - }) + tail.strip_prefix(marker) + .is_some_and(|rest| rest.is_empty() || rest.starts_with(char::is_whitespace)) }) { end = index; break; @@ -217,11 +223,7 @@ fn extract_statement(goal_text: &str) -> String { } /// Run a single probe through the prover. Returns the raw outcome. -pub fn run_probe( - probe_text: &str, - config: &ProverConfig, - probe_filename: &str, -) -> AttemptResult { +pub fn run_probe(probe_text: &str, config: &ProverConfig, probe_filename: &str) -> AttemptResult { use std::fs; let workdir = config .workdir @@ -282,11 +284,10 @@ pub fn run_probe( // generic-failure anti-patterns. We now scan BOTH streams and // also fall back on the exit code so a non-zero exit with no // standard marker still becomes Failed (not Inconclusive). - let combined_lines: Vec<&str> = - stdout.lines().chain(stderr.lines()).collect(); - let says_success = combined_lines - .iter() - .any(|l| l.contains("Proof verified successfully") || l.contains("✓ Proof verified")); + let combined_lines: Vec<&str> = stdout.lines().chain(stderr.lines()).collect(); + let says_success = combined_lines.iter().any(|l| { + l.contains("Proof verified successfully") || l.contains("✓ Proof verified") + }); let says_failure = combined_lines.iter().any(|l| { l.contains("Proof verification failed") || l.contains("✗ Proof verification failed") @@ -295,7 +296,9 @@ pub fn run_probe( let exit_failed = !o.status.success(); if says_success && !says_failure && !exit_failed { - AttemptResult::Succeeded { duration_ms: elapsed_ms } + AttemptResult::Succeeded { + duration_ms: elapsed_ms, + } } else if says_failure || exit_failed { let err_excerpt: String = combined_lines .iter() @@ -351,9 +354,11 @@ pub fn run_playbook( for (i, tactic) in playbook.tactics.iter().enumerate() { let probe = generate_probe(&goal.raw, tactic); - let probe_filename = format!("probe_{}_{}.thy", - sanitize_filename(&playbook.specialist), - i); + let probe_filename = format!( + "probe_{}_{}.thy", + sanitize_filename(&playbook.specialist), + i + ); let result = run_probe(&probe, config, &probe_filename); let attempt = ProofAttempt { @@ -489,23 +494,34 @@ mod tests { #[test] fn extract_statement_preserves_assumptions_and_conclusion() { let statement = "assumes \"True\" shows \"False\""; - assert_eq!(extract_statement(&format!("lemma bad: {statement} by simp")), statement); + assert_eq!( + extract_statement(&format!("lemma bad: {statement} by simp")), + statement + ); } #[test] fn extract_statement_preserves_multiple_conclusions() { - assert_eq!(extract_statement("lemma bad: \"True\" and \"False\" by simp"), - "\"True\" and \"False\""); + assert_eq!( + extract_statement("lemma bad: \"True\" and \"False\" by simp"), + "\"True\" and \"False\"" + ); } #[test] fn extract_statement_keeps_type_annotation_in_anonymous_lemma() { - assert_eq!(extract_statement("lemma \"(x::nat) = x\" by simp"), "\"(x::nat) = x\""); + assert_eq!( + extract_statement("lemma \"(x::nat) = x\" by simp"), + "\"(x::nat) = x\"" + ); } #[test] fn extract_statement_keeps_proof_words_inside_terms() { - assert_eq!(extract_statement("lemma foo: \"by = proof\" by simp"), "\"by = proof\""); + assert_eq!( + extract_statement("lemma foo: \"by = proof\" by simp"), + "\"by = proof\"" + ); } #[cfg(unix)] @@ -513,14 +529,21 @@ mod tests { fn subprocess_failure_overrides_success_text() { use std::os::unix::fs::PermissionsExt; let workdir = std::env::temp_dir().join(format!( - "burrower-output-regression-{}-{}", std::process::id(), - std::time::SystemTime::now().duration_since(std::time::UNIX_EPOCH).unwrap().as_nanos() + "burrower-output-regression-{}-{}", + std::process::id(), + std::time::SystemTime::now() + .duration_since(std::time::UNIX_EPOCH) + .unwrap() + .as_nanos() )); std::fs::create_dir_all(&workdir).unwrap(); let executable = workdir.join("output-fixture.sh"); let config = ProverConfig { - echidna_path: executable.clone(), timeout_secs: 5, - workdir: Some(workdir.clone()), project_root: None, sandbox: "none".into(), + echidna_path: executable.clone(), + timeout_secs: 5, + workdir: Some(workdir.clone()), + project_root: None, + sandbox: "none".into(), }; // These subprocesses test the output contract, not theorem proving. for (diagnostic, exit, expected) in [ @@ -532,7 +555,10 @@ mod tests { "#!/bin/sh\nprintf 'Proof verified successfully\\n'\nprintf '{diagnostic}\\n' >&2\nexit {exit}\n" )).unwrap(); std::fs::set_permissions(&executable, std::fs::Permissions::from_mode(0o700)).unwrap(); - assert_eq!(run_probe("fixture", &config, "fixture.thy").is_success(), expected); + assert_eq!( + run_probe("fixture", &config, "fixture.thy").is_success(), + expected + ); } std::fs::remove_dir_all(workdir).unwrap(); } diff --git a/crates/burrower-core/src/goal.rs b/crates/burrower-core/src/goal.rs index b202adb..465510c 100644 --- a/crates/burrower-core/src/goal.rs +++ b/crates/burrower-core/src/goal.rs @@ -42,7 +42,7 @@ fn detect_language(raw: &str) -> Option { // Order matters — check the most distinctive keywords first. if raw.contains("theorem ") && (raw.contains(":=") || raw.contains("by ")) { Some("lean".to_string()) - } else if raw.contains("lemma ") && raw.contains("\\<") { + } else if raw.contains("lemma ") && raw.contains("\\<") { Some("isabelle".to_string()) } else if raw.contains("Theorem ") || raw.contains("Lemma ") || raw.contains("Definition ") { Some("coq".to_string()) @@ -62,11 +62,38 @@ fn extract_tokens(raw: &str, _language: Option<&str>) -> BTreeSet { // Common keywords across Isabelle / Coq / Lean that are pure // syntactic noise — drop them to focus on semantic content. const NOISE: &[&str] = &[ - "lemma", "theorem", "Lemma", "Theorem", "Definition", "definition", - "proof", "qed", "by", "using", "assumes", "shows", "fixes", - "where", "if", "then", "else", "let", "in", - "the", "a", "an", "of", "to", "from", "for", "with", - "Type", "Prop", "Set", "True", "False", + "lemma", + "theorem", + "Lemma", + "Theorem", + "Definition", + "definition", + "proof", + "qed", + "by", + "using", + "assumes", + "shows", + "fixes", + "where", + "if", + "then", + "else", + "let", + "in", + "the", + "a", + "an", + "of", + "to", + "from", + "for", + "with", + "Type", + "Prop", + "Set", + "True", + "False", ]; raw_tokens(&cleaned) diff --git a/crates/burrower-core/src/ledger.rs b/crates/burrower-core/src/ledger.rs index c83eb2a..953fb89 100644 --- a/crates/burrower-core/src/ledger.rs +++ b/crates/burrower-core/src/ledger.rs @@ -144,8 +144,15 @@ impl Ledger { } /// Filter records matching a predicate. - pub fn query(&self, mut predicate: impl FnMut(&LedgerRecord) -> bool) -> Result> { - Ok(self.read_all()?.into_iter().filter(|r| predicate(r)).collect()) + pub fn query( + &self, + mut predicate: impl FnMut(&LedgerRecord) -> bool, + ) -> Result> { + Ok(self + .read_all()? + .into_iter() + .filter(|r| predicate(r)) + .collect()) } /// Most-recent N records. @@ -271,7 +278,8 @@ mod tests { learning: Some(Learning { pattern_extracted: "tropical-not-ordered-class".to_string(), pattern_kind: "anti-pattern".to_string(), - generalisation: "Tropical algebra needs explicit hierarchy class instance".to_string(), + generalisation: "Tropical algebra needs explicit hierarchy class instance" + .to_string(), visible_to: vec![], }), extra: serde_json::Value::Null, diff --git a/crates/burrower-core/src/lib.rs b/crates/burrower-core/src/lib.rs index ee4220c..7ff7a48 100644 --- a/crates/burrower-core/src/lib.rs +++ b/crates/burrower-core/src/lib.rs @@ -26,27 +26,27 @@ //! Future work: tree-edit distance on parsed AST (v2), GNN embeddings //! once the ECHIDNA corpus training lands (v3). -pub mod goal; +pub mod attempt; pub mod corpus; -pub mod ranking; -pub mod specialist; +pub mod goal; pub mod ledger; -pub mod attempt; -pub mod serve; pub mod oracle; +pub mod ranking; +pub mod serve; +pub mod specialist; -pub use goal::{parse_goal, Goal}; -pub use corpus::{Corpus, IndexedLemma, LibraryKind}; -pub use ranking::{Home, rank}; -pub use specialist::{ - Algebraist, Combinatorialist, ConsensusHome, OrderTheorist, Reading, - Specialist, Swarm, Synthesis, +pub use attempt::{ + generate_probe, run_playbook, run_probe, AttemptResult, Playbook, ProofAttempt, ProverConfig, + TacticTemplate, }; +pub use corpus::{Corpus, IndexedLemma, LibraryKind}; +pub use goal::{parse_goal, Goal}; pub use ledger::{ - goal_hash, new_id, now_iso, record_reading, - Approach, Learning, Ledger, LedgerRecord, RecordResult, + goal_hash, new_id, now_iso, record_reading, Approach, Learning, Ledger, LedgerRecord, + RecordResult, }; -pub use attempt::{ - generate_probe, run_playbook, run_probe, - AttemptResult, Playbook, ProofAttempt, ProverConfig, TacticTemplate, +pub use ranking::{rank, Home}; +pub use specialist::{ + Algebraist, Combinatorialist, ConsensusHome, OrderTheorist, Reading, Specialist, Swarm, + Synthesis, }; diff --git a/crates/burrower-core/src/oracle.rs b/crates/burrower-core/src/oracle.rs index 97146cf..96c8774 100644 --- a/crates/burrower-core/src/oracle.rs +++ b/crates/burrower-core/src/oracle.rs @@ -22,10 +22,10 @@ //! computational work in Julia means proof-burrower stays prover-agnostic //! and the math lives next to the rest of the project's Julia helpers. +use crate::goal::Goal; use crate::ledger::{ goal_hash, new_id, now_iso, Approach, Learning, Ledger, LedgerRecord, RecordResult, }; -use crate::goal::Goal; use serde_json::Value; use std::path::PathBuf; use std::process::Command; @@ -72,7 +72,10 @@ impl OracleVerdict { /// True iff the swarm should SKIP the proof attempt (the lemma is /// suspect or the oracle hit a hard failure). pub fn blocks_attempt(&self) -> bool { - matches!(self, OracleVerdict::Disagree { .. } | OracleVerdict::FuzzCounter { .. }) + matches!( + self, + OracleVerdict::Disagree { .. } | OracleVerdict::FuzzCounter { .. } + ) } pub fn pattern_kind(&self) -> &'static str { @@ -111,7 +114,13 @@ pub fn run(config: &OracleConfig) -> OracleVerdict { reason: format!( "julia exit {} — stderr tail: {}", output.status.code().unwrap_or(-1), - stderr.lines().last().unwrap_or("").chars().take(160).collect::() + stderr + .lines() + .last() + .unwrap_or("") + .chars() + .take(160) + .collect::() ), }; } @@ -133,15 +142,25 @@ pub fn parse_verdict(stdout: &str) -> OracleVerdict { }; let verdict = if payload.starts_with("agree") { - OracleVerdict::Agree { detail: payload.to_string() } + OracleVerdict::Agree { + detail: payload.to_string(), + } } else if payload.starts_with("disagree") { - OracleVerdict::Disagree { detail: payload.to_string() } + OracleVerdict::Disagree { + detail: payload.to_string(), + } } else if payload.starts_with("fuzz-counter") { - OracleVerdict::FuzzCounter { detail: payload.to_string() } + OracleVerdict::FuzzCounter { + detail: payload.to_string(), + } } else if payload.starts_with("fuzz-clean") { - OracleVerdict::FuzzClean { detail: payload.to_string() } + OracleVerdict::FuzzClean { + detail: payload.to_string(), + } } else if payload.starts_with("inapplicable") { - OracleVerdict::Inapplicable { reason: payload.to_string() } + OracleVerdict::Inapplicable { + reason: payload.to_string(), + } } else { OracleVerdict::Inapplicable { reason: format!("unparsed verdict shape: {payload}"), @@ -207,7 +226,12 @@ pub fn record_to_ledger( preconditions_assumed: vec![], }), result: Some(RecordResult { - status: if verdict.blocks_attempt() { "blocked" } else { "advisory" }.to_string(), + status: if verdict.blocks_attempt() { + "blocked" + } else { + "advisory" + } + .to_string(), explanation: format!("{:?}", verdict), artifacts: vec![], }), @@ -225,7 +249,9 @@ mod tests { #[test] fn parse_agree_line() { - let v = parse_verdict("oracle: agree (family=tropical-determinant-min, computed=5, expected=5)"); + let v = parse_verdict( + "oracle: agree (family=tropical-determinant-min, computed=5, expected=5)", + ); assert!(matches!(v, OracleVerdict::Agree { .. })); assert!(!v.blocks_attempt()); } @@ -239,7 +265,9 @@ mod tests { #[test] fn parse_fuzz_counter_blocks_attempt() { - let v = parse_verdict("oracle: fuzz-counter (family=foo, trials=50, disagreements=3, sample=...)"); + let v = parse_verdict( + "oracle: fuzz-counter (family=foo, trials=50, disagreements=3, sample=...)", + ); assert!(v.blocks_attempt()); assert_eq!(v.pattern_kind(), "oracle-fuzz-counter"); } diff --git a/crates/burrower-core/src/ranking.rs b/crates/burrower-core/src/ranking.rs index 33b318f..35134b0 100644 --- a/crates/burrower-core/src/ranking.rs +++ b/crates/burrower-core/src/ranking.rs @@ -41,8 +41,7 @@ pub fn rank(goal: &Goal, corpus: &Corpus, k: usize) -> Vec { .filter_map(|lemma| { let shared: BTreeSet = goal.tokens.intersection(&lemma.tokens).cloned().collect(); - let union_count = - goal.tokens.union(&lemma.tokens).count(); + let union_count = goal.tokens.union(&lemma.tokens).count(); if union_count == 0 { return None; } @@ -82,7 +81,10 @@ mod tests { file: PathBuf::from("test"), line: 1, kind: LibraryKind::Isabelle, - tokens: tokens.iter().map(|s| s.to_string()).collect::>(), + tokens: tokens + .iter() + .map(|s| s.to_string()) + .collect::>(), } } @@ -91,12 +93,12 @@ mod tests { let goal = parse_goal("lemma foo: \"trop_walks_sum A S \\ trop_walks_sum A T\""); let corpus = Corpus { lemmas: vec![ - mk_lemma("trop_walks_sum_ge_member", &["trop_walks_sum", "path_weight"]), - mk_lemma("nat_add_comm", &["nat", "add", "comm"]), mk_lemma( - "trop_walks_sum_mono", - &["trop_walks_sum", "mono", "subset"], + "trop_walks_sum_ge_member", + &["trop_walks_sum", "path_weight"], ), + mk_lemma("nat_add_comm", &["nat", "add", "comm"]), + mk_lemma("trop_walks_sum_mono", &["trop_walks_sum", "mono", "subset"]), ], }; let ranked = rank(&goal, &corpus, 3); diff --git a/crates/burrower-core/src/serve.rs b/crates/burrower-core/src/serve.rs index e9c4e28..6eebbce 100644 --- a/crates/burrower-core/src/serve.rs +++ b/crates/burrower-core/src/serve.rs @@ -38,7 +38,7 @@ //! See `proof-burrower/docs/ECHIDNA-INTEGRATION.adoc` §BI-1. use crate::{ - attempt::{run_playbook, ProverConfig, TacticTemplate, Playbook}, + attempt::{run_playbook, Playbook, ProverConfig, TacticTemplate}, corpus::Corpus, goal::parse_goal, ledger::Ledger, @@ -86,10 +86,18 @@ pub struct Response { impl Response { fn ok(result: Value) -> Self { - Self { ok: true, result: Some(result), error: None } + Self { + ok: true, + result: Some(result), + error: None, + } } fn err(e: E) -> Self { - Self { ok: false, result: None, error: Some(e.to_string()) } + Self { + ok: false, + result: None, + error: Some(e.to_string()), + } } } @@ -104,10 +112,11 @@ pub fn run(socket_path: PathBuf) -> Result<()> { // Best-effort cleanup of any stale socket file. let _ = std::fs::remove_file(&socket_path); - let listener = UnixListener::bind(&socket_path).with_context(|| { - format!("failed to bind Unix socket at {}", socket_path.display()) - })?; - let _guard = SocketGuard { path: socket_path.clone() }; + let listener = UnixListener::bind(&socket_path) + .with_context(|| format!("failed to bind Unix socket at {}", socket_path.display()))?; + let _guard = SocketGuard { + path: socket_path.clone(), + }; eprintln!( "burrower serve: listening on {} (line-delimited JSON; \ @@ -188,13 +197,14 @@ struct SwarmArgs { #[serde(default)] ledger: Option, } -fn default_top() -> usize { 5 } +fn default_top() -> usize { + 5 +} fn handle_swarm(args: Value) -> Result { let a: SwarmArgs = serde_json::from_value(args).map_err(|e| anyhow!("swarm args: {e}"))?; - let corpus = Corpus::load(&a.index).with_context(|| { - format!("load index from {}", a.index.display()) - })?; + let corpus = + Corpus::load(&a.index).with_context(|| format!("load index from {}", a.index.display()))?; let parsed = parse_goal(&a.goal); let swarm = Swarm::new(); let ledger_handle = a.ledger.as_ref().map(|p| Ledger::open(p)).transpose()?; @@ -218,7 +228,9 @@ struct AttemptArgs { #[serde(default)] sandbox: Option, } -fn default_timeout() -> u32 { 60 } +fn default_timeout() -> u32 { + 60 +} fn handle_attempt(args: Value) -> Result { let a: AttemptArgs = serde_json::from_value(args).map_err(|e| anyhow!("attempt args: {e}"))?; @@ -242,7 +254,9 @@ struct LedgerArgs { #[serde(default = "default_limit")] limit: usize, } -fn default_limit() -> usize { 10 } +fn default_limit() -> usize { + 10 +} fn handle_ledger_recent(args: Value) -> Result { let a: LedgerArgs = serde_json::from_value(args).map_err(|e| anyhow!("ledger args: {e}"))?; @@ -256,8 +270,15 @@ fn handle_ledger_recent(args: Value) -> Result { // the dispatch tree is wired below. #[allow(dead_code)] fn _force_use_of_imports() { - let _ = TacticTemplate { name: String::new(), script: String::new(), description: String::new() }; - let _ = Playbook { specialist: String::new(), tactics: vec![] }; + let _ = TacticTemplate { + name: String::new(), + script: String::new(), + description: String::new(), + }; + let _ = Playbook { + specialist: String::new(), + tactics: vec![], + }; let _: Option> = None; let _ = run_playbook; } diff --git a/crates/burrower-core/src/specialist.rs b/crates/burrower-core/src/specialist.rs index 1c38850..7e42548 100644 --- a/crates/burrower-core/src/specialist.rs +++ b/crates/burrower-core/src/specialist.rs @@ -81,12 +81,16 @@ pub trait Specialist { let kws: Vec = self.keywords().iter().map(|s| s.to_lowercase()).collect(); let mut witnesses: Vec<&String> = Vec::new(); for kw in &kws { - if let Some(t) = goal.tokens.iter().find(|t| { - *t == kw || t.starts_with(&format!("{}_", kw)) || t.contains(kw) - }) { + if let Some(t) = goal + .tokens + .iter() + .find(|t| *t == kw || t.starts_with(&format!("{}_", kw)) || t.contains(kw)) + { witnesses.push(t); } - if witnesses.len() >= 5 { break; } + if witnesses.len() >= 5 { + break; + } } if witnesses.is_empty() { format!( @@ -94,11 +98,7 @@ pub trait Specialist { self.domain().to_lowercase() ) } else { - format!( - "{} structure detected via {:?}", - self.domain(), - witnesses - ) + format!("{} structure detected via {:?}", self.domain(), witnesses) } } /// Default relevance: how many of the specialist's keywords appear @@ -116,9 +116,7 @@ pub trait Specialist { .filter(|kw| { let kw_lc = kw.to_lowercase(); goal.tokens.iter().any(|t| { - t == &kw_lc - || t.starts_with(&format!("{}_", kw_lc)) - || t.contains(&kw_lc) + t == &kw_lc || t.starts_with(&format!("{}_", kw_lc)) || t.contains(&kw_lc) }) }) .count(); @@ -195,17 +193,49 @@ pub const MIN_DOMAIN_HITS: usize = 2; pub struct Algebraist; impl Specialist for Algebraist { - fn name(&self) -> &'static str { "Algebraist" } - fn domain(&self) -> &'static str { "Algebra" } + fn name(&self) -> &'static str { + "Algebraist" + } + fn domain(&self) -> &'static str { + "Algebra" + } fn keywords(&self) -> &'static [&'static str] { &[ - "group", "ring", "field", "semiring", "monoid", "semigroup", - "ideal", "module", "vector", "homomorphism", "isomorphism", - "kernel", "image", "quotient", "polynomial", "matrix", - "abelian", "commutative", "associative", "distributive", - "identity", "inverse", "comm_monoid", "comm_semiring", - "tropical", "trop", "tropm", "plus", "mult", "add", "mul", - "zero", "one", "neginf", "fin", + "group", + "ring", + "field", + "semiring", + "monoid", + "semigroup", + "ideal", + "module", + "vector", + "homomorphism", + "isomorphism", + "kernel", + "image", + "quotient", + "polynomial", + "matrix", + "abelian", + "commutative", + "associative", + "distributive", + "identity", + "inverse", + "comm_monoid", + "comm_semiring", + "tropical", + "trop", + "tropm", + "plus", + "mult", + "add", + "mul", + "zero", + "one", + "neginf", + "fin", ] } fn playbook(&self) -> Playbook { @@ -269,18 +299,49 @@ impl Specialist for Algebraist { pub struct OrderTheorist; impl Specialist for OrderTheorist { - fn name(&self) -> &'static str { "OrderTheorist" } - fn domain(&self) -> &'static str { "Order Theory" } + fn name(&self) -> &'static str { + "OrderTheorist" + } + fn domain(&self) -> &'static str { + "Order Theory" + } fn keywords(&self) -> &'static [&'static str] { &[ - "le", "leq", "lt", "ge", "geq", "gt", "subseteq", "subset", - "linorder", "preorder", "order_bot", "order_top", - "lattice", "complete_lattice", "sup", "inf", - "monotone", "mono", "antitone", "cofinal", - "fixpoint", "lfp", "gfp", "least", "greatest", - "well_founded", "well_order", "chain", "directed", - "max", "min", "supremum", "infimum", - "absorb", "idempotent", + "le", + "leq", + "lt", + "ge", + "geq", + "gt", + "subseteq", + "subset", + "linorder", + "preorder", + "order_bot", + "order_top", + "lattice", + "complete_lattice", + "sup", + "inf", + "monotone", + "mono", + "antitone", + "cofinal", + "fixpoint", + "lfp", + "gfp", + "least", + "greatest", + "well_founded", + "well_order", + "chain", + "directed", + "max", + "min", + "supremum", + "infimum", + "absorb", + "idempotent", ] } fn playbook(&self) -> Playbook { @@ -354,17 +415,45 @@ impl Specialist for OrderTheorist { pub struct Combinatorialist; impl Specialist for Combinatorialist { - fn name(&self) -> &'static str { "Combinatorialist" } - fn domain(&self) -> &'static str { "Combinatorics" } + fn name(&self) -> &'static str { + "Combinatorialist" + } + fn domain(&self) -> &'static str { + "Combinatorics" + } fn keywords(&self) -> &'static [&'static str] { &[ - "finite", "card", "sum", "prod", "card_eq", - "set", "list", "seq", "permutation", "perm", - "walk", "walks", "path", "path_weight", "cycle", - "graph", "vertex", "edge", "tree", "forest", - "n_choose_k", "binomial", "factorial", - "induction", "induct", "base", "step", - "sigma", "union", "insert", "filter", + "finite", + "card", + "sum", + "prod", + "card_eq", + "set", + "list", + "seq", + "permutation", + "perm", + "walk", + "walks", + "path", + "path_weight", + "cycle", + "graph", + "vertex", + "edge", + "tree", + "forest", + "n_choose_k", + "binomial", + "factorial", + "induction", + "induct", + "base", + "step", + "sigma", + "union", + "insert", + "filter", ] } fn playbook(&self) -> Playbook { @@ -464,7 +553,9 @@ impl Default for Swarm { } impl Swarm { - pub fn new() -> Self { Self::default() } + pub fn new() -> Self { + Self::default() + } /// Add a specialist. Used by the planned 007 loader to register /// dynamically-defined agents. @@ -580,9 +671,11 @@ impl Swarm { }) .collect(); consensus.sort_by(|a, b| { - b.votes - .cmp(&a.votes) - .then_with(|| b.weighted_score.partial_cmp(&a.weighted_score).unwrap_or(std::cmp::Ordering::Equal)) + b.votes.cmp(&a.votes).then_with(|| { + b.weighted_score + .partial_cmp(&a.weighted_score) + .unwrap_or(std::cmp::Ordering::Equal) + }) }); let domains: Vec = engaged.iter().map(|r| r.domain.clone()).collect(); @@ -595,10 +688,7 @@ impl Swarm { domains.join(", ") ) } else { - format!( - "Single-domain object: best read as {}.", - domains[0] - ) + format!("Single-domain object: best read as {}.", domains[0]) }; Synthesis { @@ -639,7 +729,8 @@ mod tests { #[test] fn algebraist_recognises_tropical_goal() { - let g = parse_goal("lemma trop_walks_sum_mono: trop_walks_sum A S \\ trop_walks_sum A T"); + let g = + parse_goal("lemma trop_walks_sum_mono: trop_walks_sum A S \\ trop_walks_sum A T"); let s = Algebraist; assert!(s.relevance(&g) > 0.0, "should engage on tropical content"); } @@ -666,12 +757,18 @@ mod tests { // Isabelle 2025-1 drift fixes (omega→linarith, sum.atLeastAtMost_Suc // deprecation, Fun.swap input-only). Lock in the new minimums so // future shrink-regressions are caught. - assert!(Algebraist.playbook().tactics.len() >= 10, - "Algebraist playbook should have ≥10 tactics post-2026-04-26 expansion"); - assert!(OrderTheorist.playbook().tactics.len() >= 12, - "OrderTheorist playbook should have ≥12 tactics post-2026-04-26 expansion"); - assert!(Combinatorialist.playbook().tactics.len() >= 12, - "Combinatorialist playbook should have ≥12 tactics post-2026-04-26 expansion"); + assert!( + Algebraist.playbook().tactics.len() >= 10, + "Algebraist playbook should have ≥10 tactics post-2026-04-26 expansion" + ); + assert!( + OrderTheorist.playbook().tactics.len() >= 12, + "OrderTheorist playbook should have ≥12 tactics post-2026-04-26 expansion" + ); + assert!( + Combinatorialist.playbook().tactics.len() >= 12, + "Combinatorialist playbook should have ≥12 tactics post-2026-04-26 expansion" + ); } #[test] @@ -679,32 +776,56 @@ mod tests { // The Tropical_Semirings session-close added these specific tactics // because real failures pointed at them. They must stay named-and- // findable so a future ledger entry can cite them by name. - let names: Vec = Combinatorialist.playbook().tactics - .iter().map(|t| t.name.clone()).collect(); - assert!(names.iter().any(|n| n == "permutes-in-image"), - "Combinatorialist must carry the Det 153/207 fix"); - assert!(names.iter().any(|n| n == "metis-append"), - "Combinatorialist must carry the Kleene 403 list-decomp fix"); - assert!(names.iter().any(|n| n == "induction-arbitrary"), - "Combinatorialist must carry the Matrices_Full generalised-induction pattern"); + let names: Vec = Combinatorialist + .playbook() + .tactics + .iter() + .map(|t| t.name.clone()) + .collect(); + assert!( + names.iter().any(|n| n == "permutes-in-image"), + "Combinatorialist must carry the Det 153/207 fix" + ); + assert!( + names.iter().any(|n| n == "metis-append"), + "Combinatorialist must carry the Kleene 403 list-decomp fix" + ); + assert!( + names.iter().any(|n| n == "induction-arbitrary"), + "Combinatorialist must carry the Matrices_Full generalised-induction pattern" + ); } #[test] fn order_theorist_carries_2025_drift_fixes() { - let names: Vec = OrderTheorist.playbook().tactics - .iter().map(|t| t.name.clone()).collect(); - assert!(names.iter().any(|n| n == "linarith"), - "OrderTheorist must carry linarith (omega→linarith drift in 2025-1)"); - assert!(names.iter().any(|n| n == "force"), - "OrderTheorist must carry force (Kleene 403 list-decomp fallback)"); + let names: Vec = OrderTheorist + .playbook() + .tactics + .iter() + .map(|t| t.name.clone()) + .collect(); + assert!( + names.iter().any(|n| n == "linarith"), + "OrderTheorist must carry linarith (omega→linarith drift in 2025-1)" + ); + assert!( + names.iter().any(|n| n == "force"), + "OrderTheorist must carry force (Kleene 403 list-decomp fallback)" + ); } #[test] fn algebraist_carries_ac_simps_replacement() { - let names: Vec = Algebraist.playbook().tactics - .iter().map(|t| t.name.clone()).collect(); - assert!(names.iter().any(|n| n == "ac-simps"), - "Algebraist must carry ac-simps (replaces looping metis chains)"); + let names: Vec = Algebraist + .playbook() + .tactics + .iter() + .map(|t| t.name.clone()) + .collect(); + assert!( + names.iter().any(|n| n == "ac-simps"), + "Algebraist must carry ac-simps (replaces looping metis chains)" + ); } #[test] diff --git a/crates/burrower-core/tests/live_isabelle.rs b/crates/burrower-core/tests/live_isabelle.rs index d0c347f..3afdbf7 100644 --- a/crates/burrower-core/tests/live_isabelle.rs +++ b/crates/burrower-core/tests/live_isabelle.rs @@ -39,7 +39,8 @@ fn isabelle_preserves_and_checks_the_complete_goal() { "using assms by simp" } else { "by simp" - }.into(); + } + .into(); let probe = generate_probe(goal, &tactic); let result = run_probe(&probe, &config, "Probe.thy"); eprintln!("{goal}: {result:?}"); diff --git a/docs/governance/CRG-AUDIT-TEMPLATE.adoc b/docs/governance/CRG-AUDIT-TEMPLATE.adoc index e7479db..25b244e 100644 --- a/docs/governance/CRG-AUDIT-TEMPLATE.adoc +++ b/docs/governance/CRG-AUDIT-TEMPLATE.adoc @@ -24,7 +24,7 @@ Evaluates the `proof-burrower` repository against - Standard: `standards/component-readiness-grades/COMPONENT-READINESS-GRADES.md` - Template (criteria boilerplate): `rsr-template-repo/docs/governance/CRG-CRITERIA.adoc` - Self-declared grade (prior art): - * `.machine_readable/6a2/STATE.a2ml` → `grade = ""` + * `.machine_readable/descriptiles/STATE.a2ml` → `grade = ""` * `docs/READINESS.md` (if present) → per-component grades * Third-party badges (Glama, OpenSSF, etc.) if any — note date and scope - Audit date: 2026-04-26 @@ -64,7 +64,7 @@ Do *not* mark PRESENT without citing the path. | PRESENT / PARTIAL (count) / ABSENT | `.github/workflows/` -| `.machine_readable/6a2/` canonical A2ML +| `.machine_readable/descriptiles/` canonical A2ML | PRESENT (STATE, META, ECOSYSTEM, AGENTIC, NEUROSYM, PLAYBOOK) / ABSENT | Layout matches CLAUDE.md invariant @@ -143,7 +143,7 @@ RSR compliance verdict: *met* / *partial* / *not met* — Grade D floor satisfie Cite *from authoritative source* (STATE.a2ml or CI log). Do not re-count by filesystem grep — grade the evidence that already exists. -- `total-tests = N` (from `.machine_readable/6a2/STATE.a2ml` or CI). +- `total-tests = N` (from `.machine_readable/descriptiles/STATE.a2ml` or CI). - Breakdown by suite: list each named suite and its count. - CI: `.github/workflows/.yml` runs on push / tag / schedule. - Last green run: date + commit SHA. @@ -280,7 +280,7 @@ them. Examples: == Related Files - `docs/READINESS.md` — per-component table. Note v1.0-vs-v2.0 schema alignment. -- `.machine_readable/6a2/STATE.a2ml` — authoritative self-declared state. +- `.machine_readable/descriptiles/STATE.a2ml` — authoritative self-declared state. - `docs/governance/CRG-LIFT-PLAN-2026-04-26.adoc` — companion plan for D→C (and medium-term C→B) lifts. - `docs/governance/CRG-CRITERIA.adoc` — boilerplate criteria doc. diff --git a/docs/governance/MAINTENANCE-CHECKLIST.a2ml b/docs/governance/MAINTENANCE-CHECKLIST.a2ml index 40db158..44cf789 100644 --- a/docs/governance/MAINTENANCE-CHECKLIST.a2ml +++ b/docs/governance/MAINTENANCE-CHECKLIST.a2ml @@ -2,6 +2,7 @@ # Cross-repo maintenance baseline (machine-readable canonical) [metadata] +name = "proof-burrower-maintenance-checklist" version = "1.1.0" last-updated = "2026-02-24" scope = "cross-repo" From 287d2e3e38473293320f240476f3aa3adaf0e646 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 03:03:57 +0100 Subject: [PATCH 03/14] fix(ci): validate K9 contracts and document safe buffer ownership --- .github/workflows/governance.yml | 2 +- .github/workflows/main-estate-audit.yml | 1 - .github/workflows/workflow-linter.yml | 22 +--- .../self-validating/methodology-guard.k9.ncl | 6 + Cargo.lock | 4 +- MAINTAINERS | 2 +- container/deploy.k9.ncl | 13 +- coordination.k9 | 120 +++++++++++------- crates/burrower-cli/src/main.rs | 2 +- crates/burrower-core/src/ranking.rs | 4 +- crates/burrower-core/src/serve.rs | 2 +- crates/burrower-wasm/src/lib.rs | 79 ++++++++++-- session/custom-checks.k9 | 60 ++++++--- 13 files changed, 219 insertions(+), 98 deletions(-) diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 80d53a1..fd42d2b 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -15,4 +15,4 @@ permissions: jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@81dbf2dd854b1444fd6236fa2352474383b2c2b9 + uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@571cc734cd69fb846032ec77a662aa8ee4fc32cd diff --git a/.github/workflows/main-estate-audit.yml b/.github/workflows/main-estate-audit.yml index 05a1963..83ef918 100755 --- a/.github/workflows/main-estate-audit.yml +++ b/.github/workflows/main-estate-audit.yml @@ -1,6 +1,5 @@ # SPDX-License-Identifier: MPL-2.0 # This workflow is managed by gh actions-lock. -# This workflow is managed by gh actions-lock. name: Central Estate CI/CD Audit diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml index 4ef23f7..61c3df0 100644 --- a/.github/workflows/workflow-linter.yml +++ b/.github/workflows/workflow-linter.yml @@ -63,24 +63,12 @@ jobs: fi echo "All workflows have permissions declared" - - name: Check SHA-Pinned Actions + - name: Verify immutable action lockfile with the authoritative tool + env: + GH_TOKEN: ${{ github.token }} run: | - echo "=== Checking Action Pinning ===" - # Find any uses: lines that don't have @SHA format - # Pattern: uses: owner/repo@<40-char-hex> - unpinned=$(grep -rnE "^[[:space:]]+uses:" .github/workflows/ | \ - grep -v "@[a-f0-9]\{40\}" | \ - grep -v "uses: \./\|uses: docker://\|uses: actions/github-script" || true) - - if [ -n "$unpinned" ]; then - echo "ERROR: Found unpinned actions:" - echo "$unpinned" - echo "" - echo "Replace version tags with SHA pins, e.g.:" - echo " uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.1" - exit 1 - fi - echo "All actions are SHA-pinned" + gh extension install github/gh-actions-lock --pin v0.1.6 + gh actions-lock --rescan --no-fix - name: Check for Duplicate Workflows run: | diff --git a/.machine_readable/self-validating/methodology-guard.k9.ncl b/.machine_readable/self-validating/methodology-guard.k9.ncl index 616493d..2d39e30 100644 --- a/.machine_readable/self-validating/methodology-guard.k9.ncl +++ b/.machine_readable/self-validating/methodology-guard.k9.ncl @@ -1,3 +1,4 @@ +K9! # SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # @@ -8,6 +9,11 @@ # Usage: k9 validate methodology-guard let methodology_guard = { + pedigree = { + name = "methodology-guard", + version = "1.0.0", + leash = 'Kennel, + }, name = "methodology-guard", version = "1.0.0", description = "Validates that agent work respects declared methodology constraints", diff --git a/Cargo.lock b/Cargo.lock index 71ae214..413b748 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -63,9 +63,9 @@ dependencies = [ [[package]] name = "anyhow" -version = "1.0.102" +version = "1.0.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c" +checksum = "330a5ed07fa54e4702c9d6c4174f74427fc0ef6e214bbd677ae50a5099946470" [[package]] name = "bitflags" diff --git a/MAINTAINERS b/MAINTAINERS index 37f6411..2bcd01d 100644 --- a/MAINTAINERS +++ b/MAINTAINERS @@ -6,7 +6,7 @@ This file lists the current maintainers of this project. | Name | GitHub | Role | Since | |------|--------|------|-------| -| Metadatastician | @metadatastician | Primary | Project Start | +| Jonathan D.A. Jewell | @hyperpolymath | Sole Maintainer | Project Start | ## Emeritus Maintainers diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index e99efc8..13eeb45 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -1,3 +1,4 @@ +K9! # SPDX-License-Identifier: MPL-2.0 # deploy.k9.ncl — Proof Burrower deployment component (Hunt level) # @@ -18,7 +19,7 @@ let component_pedigree = { # L1: The Snout — Identity # ───────────────────────────────────────────────────────────── metadata = { - name = "{{SERVICE_NAME}}-deploy", + name = "proof-burrower-deploy", version = "0.0.1", breed = "application/vnd.k9+nickel", magic_number = "K9!", @@ -94,7 +95,8 @@ let deployment = { # Container configuration container = { image = "{{REGISTRY}}/{{SERVICE_NAME}}", - port = {{PORT}}, + # Required deployment input; no network port has been selected here. + port | Number, health_check = "/health", readiness_check = "/ready", }, @@ -143,7 +145,12 @@ echo "K9: Rollback complete." # Export the component { - pedigree = component_pedigree, + pedigree = component_pedigree & { + name = "proof-burrower-deploy", + version = "0.0.1", + leash = 'Hunt, + signature_required = true, + }, deployment = deployment, scripts = scripts, diff --git a/coordination.k9 b/coordination.k9 index ba31125..58d42a1 100644 --- a/coordination.k9 +++ b/coordination.k9 @@ -1,43 +1,77 @@ -# Thin coordination bindings for central session-management standards - -session_management: - source_of_truth: "standards/session-management-standards" - canonical_commands: - - "intake repo " - - "checkpoint change " - - "verify maintenance " - - "verify substantial " - - "verify release " - - "close planned " - - "close urgent " - - "recover repo " - - "handover full " - - "handover split " - - "handover model " - - "handover human " - -signals: - - name: "session.intake" - command: "intake repo " - - name: "session.checkpoint" - command: "checkpoint change " - - name: "session.verify.maintenance" - command: "verify maintenance " - - name: "session.verify.substantial" - command: "verify substantial " - - name: "session.verify.release" - command: "verify release " - - name: "session.close.planned" - command: "close planned " - - name: "session.close.urgent" - command: "close urgent " - - name: "session.recover" - command: "recover repo " - - name: "session.handover.full" - command: "handover full " - - name: "session.handover.split" - command: "handover split " - - name: "session.handover.model" - command: "handover model " - - name: "session.handover.human" - command: "handover human " +K9! +# SPDX-License-Identifier: MPL-2.0 +# Declarative session policy data; this file does not execute checks. +{ + pedigree = { + name = "proof-burrower-coordination", + version = "0.1.0", + leash = 'Kennel, + }, + session_management = { + source_of_truth = "standards/session-management-standards", + canonical_commands = [ + "intake repo ", + "checkpoint change ", + "verify maintenance ", + "verify substantial ", + "verify release ", + "close planned ", + "close urgent ", + "recover repo ", + "handover full ", + "handover split ", + "handover model ", + "handover human ", + ], + }, + signals = [ + { + name = "session.intake", + command = "intake repo ", + }, + { + name = "session.checkpoint", + command = "checkpoint change ", + }, + { + name = "session.verify.maintenance", + command = "verify maintenance ", + }, + { + name = "session.verify.substantial", + command = "verify substantial ", + }, + { + name = "session.verify.release", + command = "verify release ", + }, + { + name = "session.close.planned", + command = "close planned ", + }, + { + name = "session.close.urgent", + command = "close urgent ", + }, + { + name = "session.recover", + command = "recover repo ", + }, + { + name = "session.handover.full", + command = "handover full ", + }, + { + name = "session.handover.split", + command = "handover split ", + }, + { + name = "session.handover.model", + command = "handover model ", + }, + { + name = "session.handover.human", + command = "handover human ", + }, + ], +} \ No newline at end of file diff --git a/crates/burrower-cli/src/main.rs b/crates/burrower-cli/src/main.rs index 83ff0e4..31ae86e 100644 --- a/crates/burrower-cli/src/main.rs +++ b/crates/burrower-cli/src/main.rs @@ -425,7 +425,7 @@ fn main() -> Result<()> { let corpus = Corpus::load(&index)?; let parsed = parse_goal(&goal); let swarm = Swarm::new(); - let ledger_handle = ledger.as_ref().map(|p| Ledger::open(p)).transpose()?; + let ledger_handle = ledger.as_ref().map(Ledger::open).transpose()?; let readings = swarm.route_with_ledger(&parsed, &corpus, top, ledger_handle.as_ref()); match format.as_str() { "json" => { diff --git a/crates/burrower-core/src/ranking.rs b/crates/burrower-core/src/ranking.rs index 35134b0..7fdd90d 100644 --- a/crates/burrower-core/src/ranking.rs +++ b/crates/burrower-core/src/ranking.rs @@ -12,10 +12,10 @@ //! //! Future versions: //! - v0.2: weight tokens by inverse document frequency (rare tokens -//! carry more signal). +//! carry more signal). //! - v0.3: tree-edit distance on parsed AST (requires real parsers). //! - v0.4: GNN embeddings (requires the trained model that ECHIDNA's -//! corpus is waiting for). +//! corpus is waiting for). use crate::corpus::{Corpus, IndexedLemma}; use crate::goal::Goal; diff --git a/crates/burrower-core/src/serve.rs b/crates/burrower-core/src/serve.rs index 6eebbce..b5d1b97 100644 --- a/crates/burrower-core/src/serve.rs +++ b/crates/burrower-core/src/serve.rs @@ -207,7 +207,7 @@ fn handle_swarm(args: Value) -> Result { Corpus::load(&a.index).with_context(|| format!("load index from {}", a.index.display()))?; let parsed = parse_goal(&a.goal); let swarm = Swarm::new(); - let ledger_handle = a.ledger.as_ref().map(|p| Ledger::open(p)).transpose()?; + let ledger_handle = a.ledger.as_ref().map(Ledger::open).transpose()?; let readings = swarm.route_with_ledger(&parsed, &corpus, a.top, ledger_handle.as_ref()); let synthesis = swarm.synthesise(&readings); Ok(json!({ diff --git a/crates/burrower-wasm/src/lib.rs b/crates/burrower-wasm/src/lib.rs index c23e635..30a169c 100644 --- a/crates/burrower-wasm/src/lib.rs +++ b/crates/burrower-wasm/src/lib.rs @@ -12,8 +12,8 @@ //! The exposed entry points take `*const u8` + `usize` length pairs //! for inputs (UTF-8 strings) and write outputs into a guest-supplied //! buffer, returning the number of bytes written (or a negative error -//! code). This is the conservative ABI — no allocator, no globals, -//! all data flows through caller-managed memory. +//! code). Data flows through caller-managed memory; optional `alloc` and +//! `dealloc` exports provide buffers for hosts without their own allocator. //! //! Future: ergonomic JS wrapper via `wasm-bindgen`. Today: minimal //! ABI to keep the artifact small and verifier-friendly. @@ -54,6 +54,12 @@ unsafe fn write_str(s: &str, out_ptr: *mut u8, out_cap: usize) -> i32 { /// /// Parses a goal string and writes the JSON-serialised `Goal` into /// the output buffer. +/// +/// # Safety +/// A non-null `goal_ptr` with nonzero `goal_len` must reference that many +/// initialized, readable bytes in one allocation. A non-null `out_ptr` must +/// permit exclusive writes of up to `out_cap` bytes. Both regions must remain +/// valid for this call; neither length may exceed `isize::MAX`. #[no_mangle] pub unsafe extern "C" fn parse_goal_json( goal_ptr: *const u8, @@ -67,9 +73,15 @@ pub unsafe extern "C" fn parse_goal_json( write_str(&json, out_ptr, out_cap) } -/// `goal_hash_hex(goal_ptr, goal_len, out_ptr, out_cap) -> 16` (always) +/// `goal_hash_hex(goal_ptr, goal_len, out_ptr, out_cap) -> bytes_written` +/// +/// Computes the goal hash and writes 16 hex chars, or returns a negative error. /// -/// Computes the goal hash and writes 16 hex chars. +/// # Safety +/// A non-null `goal_ptr` with nonzero `goal_len` must reference that many +/// initialized, readable bytes in one allocation. A non-null `out_ptr` must +/// permit exclusive writes of up to `out_cap` bytes. Both regions must remain +/// valid for this call; neither length may exceed `isize::MAX`. #[no_mangle] pub unsafe extern "C" fn goal_hash_hex( goal_ptr: *const u8, @@ -82,7 +94,11 @@ pub unsafe extern "C" fn goal_hash_hex( write_str(&h, out_ptr, out_cap) } -/// `version() -> bytes_written`. Writes the Burrower version into out_ptr. +/// Writes the Burrower version into `out_ptr`, returning its length or an error. +/// +/// # Safety +/// A non-null `out_ptr` must permit exclusive writes of up to `out_cap` bytes +/// within one live allocation; `out_cap` must not exceed `isize::MAX`. #[no_mangle] pub unsafe extern "C" fn version(out_ptr: *mut u8, out_cap: usize) -> i32 { write_str("burrower-core 0.0.1", out_ptr, out_cap) @@ -101,18 +117,59 @@ pub extern "C" fn add(a: u32, b: u32) -> u32 { // `dealloc(ptr, n)` to free it. // --------------------------------------------------------------------- +/// Allocate `n` uninitialized bytes, returning null for zero or allocation failure. +/// The caller must initialize bytes before passing them to the input functions. #[no_mangle] -pub unsafe extern "C" fn alloc(n: usize) -> *mut u8 { - let mut buf: Vec = Vec::with_capacity(n); - let ptr = buf.as_mut_ptr(); - core::mem::forget(buf); - ptr +pub extern "C" fn alloc(n: usize) -> *mut u8 { + if n == 0 { + return std::ptr::null_mut(); + } + let Ok(layout) = std::alloc::Layout::array::(n) else { + return std::ptr::null_mut(); + }; + // SAFETY: the checked layout is nonzero and describes an allocation of bytes. + unsafe { std::alloc::alloc(layout) } } +/// Release a buffer obtained from `alloc`, whether or not it was initialized. +/// +/// # Safety +/// For non-null `ptr` and nonzero `n`, `ptr` must be a live allocation returned +/// by this module's `alloc(n)`, with exactly the same `n`. It must not be used +/// after this call or freed more than once. Null or zero arguments are no-ops. #[no_mangle] pub unsafe extern "C" fn dealloc(ptr: *mut u8, n: usize) { if ptr.is_null() || n == 0 { return; } - let _ = Vec::from_raw_parts(ptr, n, n); + if let Ok(layout) = std::alloc::Layout::array::(n) { + std::alloc::dealloc(ptr, layout); + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn allocated_buffer_supports_output_and_uninitialized_release() { + let buffer = alloc(64); + assert!(!buffer.is_null()); + // SAFETY: this buffer is live, exclusively owned, and has capacity 64. + unsafe { + let written = version(buffer, 64); + assert!(written > 0); + assert_eq!( + slice::from_raw_parts(buffer, written as usize), + b"burrower-core 0.0.1" + ); + dealloc(buffer, 64); + } + let uninitialized = alloc(17); + assert!(!uninitialized.is_null()); + // SAFETY: release the unchanged allocation with its original size. + unsafe { dealloc(uninitialized, 17) }; + assert!(alloc(0).is_null()); + assert!(alloc(usize::MAX).is_null()); + } } diff --git a/session/custom-checks.k9 b/session/custom-checks.k9 index bd932fa..e173a6c 100644 --- a/session/custom-checks.k9 +++ b/session/custom-checks.k9 @@ -1,15 +1,45 @@ -# Local repository session checks (thin policy layer) -version: "0.1" - -checks: - - id: "session-state-has-next-action" - applies_to: ["close planned", "close urgent", "handover full", "handover split", "handover model", "handover human"] - requirement: "LAST-CANONICAL-COMMAND.md contains next intended action" - - - id: "session-state-has-residual-risks" - applies_to: ["verify maintenance", "verify substantial", "verify release", "recover repo"] - requirement: "Residual risks field is not left blank" - - - id: "session-state-has-recommended-next-protocol" - applies_to: ["intake repo", "checkpoint change", "recover repo", "handover full"] - requirement: "Recommended next protocol is set" +K9! +# SPDX-License-Identifier: MPL-2.0 +# Declarative session policy data; this file does not execute checks. +{ + pedigree = { + name = "proof-burrower-session-checks", + version = "0.1.0", + leash = 'Kennel, + }, + version = "0.1", + checks = [ + { + id = "session-state-has-next-action", + applies_to = [ + "close planned", + "close urgent", + "handover full", + "handover split", + "handover model", + "handover human", + ], + requirement = "LAST-CANONICAL-COMMAND.md contains next intended action", + }, + { + id = "session-state-has-residual-risks", + applies_to = [ + "verify maintenance", + "verify substantial", + "verify release", + "recover repo", + ], + requirement = "Residual risks field is not left blank", + }, + { + id = "session-state-has-recommended-next-protocol", + applies_to = [ + "intake repo", + "checkpoint change", + "recover repo", + "handover full", + ], + requirement = "Recommended next protocol is set", + }, + ], +} \ No newline at end of file From 39f30777c4bed686ec4dd16f0211d57f1503f9af Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 7 Sep 2026 03:27:37 +0100 Subject: [PATCH 04/14] fix(ci): track embedded compiler debt and run real prover E2E checks --- .github/workflows/main-estate-audit.yml | 1 + .github/workflows/proof-safety.yml | 3 +- affinescript/.claude/CLAUDE.md | 18 +-- .../editors/vscode/src/extension.affine | 2 +- affinescript/lib/formatter.ml | 4 +- affinescript/lib/linter.ml | 8 +- affinescript/lib/trait.ml | 8 +- .../packages/affine-js/types.d.affine | 2 +- .../affine-res/src/AffineScript.affine | 2 +- .../affine-res/src/AffineScriptValue.affine | 2 +- .../packages/affine-ts/types.d.affine | 2 +- affinescript/runtime/src/alloc.rs | 10 +- affinescript/runtime/src/effects.rs | 14 +- affinescript/runtime/src/ffi.rs | 20 +-- affinescript/runtime/src/gc.rs | 10 +- affinescript/runtime/src/lib.rs | 2 +- affinescript/runtime/src/panic.rs | 8 +- affinescript/stdlib/Option.affine | 2 +- affinescript/stdlib/Result.affine | 4 +- affinescript/stdlib/prelude.affine | 4 +- affinescript/stdlib/result.affine | 2 +- affinescript/test/test_main.ml | 2 +- affinescript/tools/affine-doc/src/extract.rs | 8 +- affinescript/tools/affine-doc/src/html.rs | 4 +- affinescript/tools/affine-doc/src/index.rs | 2 +- affinescript/tools/affine-doc/src/main.rs | 8 +- affinescript/tools/affine-doc/src/render.rs | 6 +- affinescript/tools/affine-pkg/src/build.rs | 10 +- affinescript/tools/affine-pkg/src/config.rs | 2 +- affinescript/tools/affine-pkg/src/lockfile.rs | 2 +- affinescript/tools/affine-pkg/src/main.rs | 36 ++--- affinescript/tools/affine-pkg/src/manifest.rs | 2 +- affinescript/tools/affine-pkg/src/registry.rs | 20 +-- affinescript/tools/affine-pkg/src/resolve.rs | 8 +- affinescript/tools/affine-pkg/src/storage.rs | 10 +- .../tools/affine-pkg/src/workspace.rs | 2 +- .../tools/affinescript-lsp/src/main.rs | 2 +- tests/e2e.sh | 148 ++---------------- 38 files changed, 135 insertions(+), 265 deletions(-) diff --git a/.github/workflows/main-estate-audit.yml b/.github/workflows/main-estate-audit.yml index 83ef918..c130fe9 100755 --- a/.github/workflows/main-estate-audit.yml +++ b/.github/workflows/main-estate-audit.yml @@ -15,6 +15,7 @@ permissions: jobs: estate-audit: runs-on: ubuntu-latest + timeout-minutes: 20 steps: - uses: actions/checkout@v4.4.0 diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml index 932a54d..98c5d6f 100644 --- a/.github/workflows/proof-safety.yml +++ b/.github/workflows/proof-safety.yml @@ -57,5 +57,4 @@ jobs: env: ECHIDNA_BIN: ${{ github.workspace }}/_echidna/target/debug/echidna run: | - isabelle version - cargo test --locked -p burrower-core --test live_isabelle -- --ignored --nocapture + bash tests/e2e.sh diff --git a/affinescript/.claude/CLAUDE.md b/affinescript/.claude/CLAUDE.md index 19ef37a..03ff680 100644 --- a/affinescript/.claude/CLAUDE.md +++ b/affinescript/.claude/CLAUDE.md @@ -24,13 +24,13 @@ The following files in `.machine_readable/` contain structured project metadata: | Language/Tool | Use Case | Notes | |---------------|----------|-------| | **AffineScript** | Primary application code | Compiles to JS, type-safe | -| **Deno** | Runtime & package management | Replaces Node/npm/bun | +| **Bun** | Runtime & package management | Estate JavaScript runtime | | **Rust** | Performance-critical, systems, WASM | Preferred for CLI tools | | **Tauri 2.0+** | Mobile apps (iOS/Android) | Rust backend + web UI | | **Dioxus** | Mobile apps (native UI) | Pure Rust, React-like | | **Gleam** | Backend services | Runs on BEAM or compiles to JS | | **Bash/POSIX Shell** | Scripts, automation | Keep minimal | -| **JavaScript** | Only where AffineScript cannot | MCP protocol glue, Deno APIs | +| **JavaScript** | Only where AffineScript cannot | MCP protocol glue, Bun APIs | | **Python** | SaltStack only | No other Python permitted | | **Nickel** | Configuration language | For complex configs | | **A2ML** | State/meta files | .machine_readable/6a2/STATE.a2ml, .machine_readable/6a2/META.a2ml, .machine_readable/6a2/ECOSYSTEM.a2ml | @@ -43,10 +43,10 @@ The following files in `.machine_readable/` contain structured project metadata: | Banned | Replacement | |--------|-------------| | TypeScript | AffineScript | -| Node.js | Deno | -| npm | Deno | -| Bun | Deno | -| pnpm/yarn | Deno | +| Node.js | Bun | +| npm | Bun | +| Deno | Bun | +| pnpm/yarn | Bun | | Go | Rust | | Python (general) | AffineScript/Rust | | Java/Kotlin | Rust/Tauri/Dioxus | @@ -66,8 +66,8 @@ Both are FOSS with independent governance (no Big Tech). ### Enforcement Rules 1. **No new TypeScript files** - Convert existing TS to AffineScript -2. **No package.json - use deno.json deps** - Use deno.json imports -3. **No node_modules in production** - Deno caches deps automatically +2. **Use Bun for JavaScript dependencies** - Record them in package.json with bun.lock +3. **Use locked installs** - Run bun install --frozen-lockfile in CI 4. **No Go code** - Use Rust instead 5. **Python only for SaltStack** - All other Python must be rewritten 6. **No Kotlin/Swift for mobile** - Use Tauri 2.0+ or Dioxus @@ -76,7 +76,7 @@ Both are FOSS with independent governance (no Big Tech). - **Primary**: Guix (guix.scm) - **Fallback**: Nix (flake.nix) -- **JS deps**: Deno (deno.json imports) +- **JS deps**: Bun (package.json and bun.lock) ### Security Requirements diff --git a/affinescript/editors/vscode/src/extension.affine b/affinescript/editors/vscode/src/extension.affine index 602bbed..cea6d32 100644 --- a/affinescript/editors/vscode/src/extension.affine +++ b/affinescript/editors/vscode/src/extension.affine @@ -3,7 +3,7 @@ module extension; -// TODO: Complete semantic implementation +// TODO(#84): Complete semantic implementation /* === ORIGINAL TYPESCRIPT CONTEXT === // SPDX-License-Identifier: MPL-2.0 diff --git a/affinescript/lib/formatter.ml b/affinescript/lib/formatter.ml index 8d28dc0..7242fbe 100644 --- a/affinescript/lib/formatter.ml +++ b/affinescript/lib/formatter.ml @@ -1,9 +1,9 @@ (* SPDX-License-Identifier: MPL-2.0 *) (* AffineScript Source Code Formatter - Stub Implementation - TODO: Implement code formatting. + TODO(#84): Implement code formatting. *) -(** Format a source file - STUB *) +(** Format a source file - STUB(#84) *) let format_file (_path : string) : unit = failwith "Code formatting not yet implemented" diff --git a/affinescript/lib/linter.ml b/affinescript/lib/linter.ml index ba36a06..69becef 100644 --- a/affinescript/lib/linter.ml +++ b/affinescript/lib/linter.ml @@ -137,7 +137,7 @@ let rec has_effects (ctx : context) (e : expr) : bool = (match Symbol.lookup ctx.symbols id.name with | Some entry -> (match entry.sym_kind with - | SKFunction -> (* TODO: check function signature for effects *) false + | SKFunction -> (* TODO(#84): check function signature for effects *) false | _ -> false) | None -> false) | ExprHandle _ -> true @@ -230,7 +230,7 @@ and span_of_expr (e : expr) : Span.t = | ExprLit (LitChar (_, s)) -> s | ExprLit (LitString (_, s)) -> s | ExprLit (LitUnit s) -> s - | _ -> Span.dummy (* TODO: add spans to all expressions *) + | _ -> Span.dummy (* TODO(#84): add spans to all expressions *) and span_of_pattern (pat : pattern) : Span.t = match pat with @@ -240,7 +240,7 @@ and span_of_pattern (pat : pattern) : Span.t = (match lit with | LitInt (_, s) | LitFloat (_, s) | LitBool (_, s) | LitChar (_, s) | LitString (_, s) | LitUnit s -> s) - | _ -> Span.dummy (* TODO: add spans to all patterns *) + | _ -> Span.dummy (* TODO(#84): add spans to all patterns *) (** Lint expression *) let rec lint_expr (ctx : context) (e : expr) : unit = @@ -325,7 +325,7 @@ let rec lint_expr (ctx : context) (e : expr) : unit = Option.iter (List.iter (fun arm -> lint_expr ctx arm.ma_body)) et_catch; Option.iter (fun blk -> List.iter (lint_stmt ctx) blk.blk_stmts) et_finally - | ExprUnsafe _ -> () (* TODO: lint unsafe operations *) + | ExprUnsafe _ -> () (* TODO(#84): lint unsafe operations *) | ExprRowRestrict (e, _) -> lint_expr ctx e | ExprSpan (e, _) -> lint_expr ctx e | ExprLit _ | ExprVariant _ -> () diff --git a/affinescript/lib/trait.ml b/affinescript/lib/trait.ml index 525aefa..6a5512a 100644 --- a/affinescript/lib/trait.ml +++ b/affinescript/lib/trait.ml @@ -201,7 +201,7 @@ let register_impl (registry : trait_registry) (impl_block : impl_block) (self_ty match item with | ImplType (name, _ty_expr) -> (* Convert ty_expr to ty - placeholder for now *) - (* TODO: Need context to properly convert ty_expr to ty *) + (* TODO(#84): Need context to properly convert ty_expr to ty *) let placeholder_var = ref (Unbound (0, 0)) in Some (name.name, TVar placeholder_var) | ImplFn _ -> None @@ -263,7 +263,7 @@ let check_impl_satisfies_trait (registry : trait_registry) (impl : trait_impl) : match List.assoc_opt method_def.tm_name impl.ti_methods with | None -> Error (MissingMethod (trait_def.td_name, method_def.tm_name)) | Some impl_method -> - (* TODO: Check signature matches *) + (* TODO(#84): Check signature matches *) (* For now, just check it exists *) let impl_param_count = List.length impl_method.fd_params in let trait_param_count = List.length method_def.tm_params in @@ -425,13 +425,13 @@ let check_coherence (registry : trait_registry) (trait_name : string) : unit res match Hashtbl.find_opt registry.impls trait_name with | None -> Ok () | Some impls -> - (* TODO: Check for overlapping impls *) + (* TODO(#84): Check for overlapping impls *) (* For now, just ensure no duplicate self types *) let rec check_pairs = function | [] -> Ok () | _impl :: rest -> (* Check if any impl in rest has same self_ty *) - (* TODO: Proper unification check *) + (* TODO(#84): Proper unification check *) check_pairs rest in check_pairs impls diff --git a/affinescript/packages/affine-js/types.d.affine b/affinescript/packages/affine-js/types.d.affine index 2888670..cac779b 100644 --- a/affinescript/packages/affine-js/types.d.affine +++ b/affinescript/packages/affine-js/types.d.affine @@ -3,7 +3,7 @@ module types.d; -// TODO: Complete semantic implementation +// TODO(#84): Complete semantic implementation /* === ORIGINAL TYPESCRIPT CONTEXT === // SPDX-License-Identifier: MPL-2.0 diff --git a/affinescript/packages/affine-res/src/AffineScript.affine b/affinescript/packages/affine-res/src/AffineScript.affine index 63522ae..74db16a 100644 --- a/affinescript/packages/affine-res/src/AffineScript.affine +++ b/affinescript/packages/affine-res/src/AffineScript.affine @@ -4,4 +4,4 @@ module AffineScript; -// TODO: Complete semantic implementation +// TODO(#84): Complete semantic implementation diff --git a/affinescript/packages/affine-res/src/AffineScriptValue.affine b/affinescript/packages/affine-res/src/AffineScriptValue.affine index 7341096..9ce23e4 100644 --- a/affinescript/packages/affine-res/src/AffineScriptValue.affine +++ b/affinescript/packages/affine-res/src/AffineScriptValue.affine @@ -4,4 +4,4 @@ module AffineScriptValue; -// TODO: Complete semantic implementation +// TODO(#84): Complete semantic implementation diff --git a/affinescript/packages/affine-ts/types.d.affine b/affinescript/packages/affine-ts/types.d.affine index d289774..65b43d5 100644 --- a/affinescript/packages/affine-ts/types.d.affine +++ b/affinescript/packages/affine-ts/types.d.affine @@ -3,7 +3,7 @@ module types.d; -// TODO: Complete semantic implementation +// TODO(#84): Complete semantic implementation /* === ORIGINAL TYPESCRIPT CONTEXT === // SPDX-License-Identifier: MPL-2.0 diff --git a/affinescript/runtime/src/alloc.rs b/affinescript/runtime/src/alloc.rs index aa8c5b6..5622eec 100644 --- a/affinescript/runtime/src/alloc.rs +++ b/affinescript/runtime/src/alloc.rs @@ -72,7 +72,7 @@ static mut ALLOCATOR: AllocatorState = AllocatorState { /// /// Called once at program startup. pub fn init() { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Query WASM memory size // - [ ] Set up heap region // - [ ] Initialize free lists @@ -91,7 +91,7 @@ pub fn init() { /// Pointer to allocated memory, or null on failure #[no_mangle] pub extern "C" fn allocate(size: usize, align: usize) -> *mut u8 { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Check free list for matching size class // - [ ] Fall back to bump allocation // - [ ] Handle out-of-memory (grow memory or fail) @@ -113,7 +113,7 @@ pub extern "C" fn allocate(size: usize, align: usize) -> *mut u8 { /// The pointer must have been allocated by this allocator and not yet freed. #[no_mangle] pub unsafe extern "C" fn deallocate(ptr: *mut u8, size: usize, align: usize) { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Validate pointer is in heap range // - [ ] Add to appropriate free list // - [ ] Coalesce adjacent free blocks (optional) @@ -139,7 +139,7 @@ pub unsafe extern "C" fn reallocate( new_size: usize, align: usize, ) -> *mut u8 { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] If shrinking, just update size // - [ ] If growing and space available, extend in place // - [ ] Otherwise allocate new block and copy @@ -159,7 +159,7 @@ pub extern "C" fn alloc_stats() -> (usize, usize, usize) { } } -// TODO: Phase 6 implementation +// TODO(#84): Phase 6 implementation // - [ ] Implement size class selection // - [ ] Implement free list management // - [ ] Add memory growth support diff --git a/affinescript/runtime/src/effects.rs b/affinescript/runtime/src/effects.rs index b176f90..27c5381 100644 --- a/affinescript/runtime/src/effects.rs +++ b/affinescript/runtime/src/effects.rs @@ -131,7 +131,7 @@ static mut HANDLER_STACK: HandlerStack = HandlerStack { /// Initialize the effect system pub fn init() { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Set up initial handler frame // - [ ] Install default handlers for built-in effects // - [ ] Initialize continuation pool @@ -149,7 +149,7 @@ pub fn init() { /// Opaque handle for uninstalling #[no_mangle] pub extern "C" fn install_handler(handler: *mut Handler, evidence: *mut Evidence) -> u32 { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Push handler onto stack // - [ ] Set up evidence // - [ ] Return handle @@ -164,7 +164,7 @@ pub extern "C" fn install_handler(handler: *mut Handler, evidence: *mut Evidence /// * `handle` - Handle returned by `install_handler` #[no_mangle] pub extern "C" fn uninstall_handler(handle: u32) { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Pop handler from stack // - [ ] Restore previous evidence } @@ -182,7 +182,7 @@ pub extern "C" fn uninstall_handler(handle: u32) { /// Result of the operation #[no_mangle] pub extern "C" fn perform(evidence: *mut Evidence, op_index: u32, arg: *mut ()) -> *mut () { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Look up handler in evidence // - [ ] Create continuation // - [ ] Call handler with continuation @@ -202,7 +202,7 @@ pub extern "C" fn perform(evidence: *mut Evidence, op_index: u32, arg: *mut ()) /// Result of resuming #[no_mangle] pub extern "C" fn resume(k: *mut Continuation, value: *mut ()) -> *mut () { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Check if continuation is linear and already used // - [ ] Restore execution state // - [ ] Jump to continuation point @@ -218,14 +218,14 @@ pub extern "C" fn resume(k: *mut Continuation, value: *mut ()) -> *mut () { /// * `value` - Value to return #[no_mangle] pub extern "C" fn abort_effect(evidence: *mut Evidence, value: *mut ()) -> ! { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Unwind to handler frame // - [ ] Call return clause loop {} } -// TODO: Phase 6 implementation +// TODO(#84): Phase 6 implementation // - [ ] Implement evidence passing transform in codegen // - [ ] Implement handler frame management // - [ ] Implement one-shot continuation optimization diff --git a/affinescript/runtime/src/ffi.rs b/affinescript/runtime/src/ffi.rs index c537917..a10e4f6 100644 --- a/affinescript/runtime/src/ffi.rs +++ b/affinescript/runtime/src/ffi.rs @@ -89,7 +89,7 @@ static mut HOST_REGISTRY: HostRegistry = HostRegistry { /// Initialize FFI layer pub fn init() { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Set up host function table // - [ ] Initialize string interop // - [ ] Register built-in imports @@ -205,14 +205,14 @@ mod wasi_ffi { /// Write to stdout #[no_mangle] pub extern "C" fn wasi_print(s: FfiString) { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Use fd_write to stdout } /// Read from stdin #[no_mangle] pub extern "C" fn wasi_read_line() -> FfiString { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Use fd_read from stdin FfiString::new(core::ptr::null(), 0) } @@ -220,7 +220,7 @@ mod wasi_ffi { /// Get environment variable #[no_mangle] pub extern "C" fn wasi_getenv(name: FfiString) -> FfiString { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Use environ_get FfiString::new(core::ptr::null(), 0) } @@ -228,7 +228,7 @@ mod wasi_ffi { /// Get command line arguments #[no_mangle] pub extern "C" fn wasi_args() -> FfiArray { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Use args_get FfiArray { ptr: core::ptr::null(), @@ -244,7 +244,7 @@ mod wasi_ffi { /// Convert AffineScript Int to host i64 #[no_mangle] pub extern "C" fn int_to_i64(value: *const ()) -> i64 { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // AffineScript Ints may be arbitrary precision 0 } @@ -252,25 +252,25 @@ pub extern "C" fn int_to_i64(value: *const ()) -> i64 { /// Convert host i64 to AffineScript Int #[no_mangle] pub extern "C" fn i64_to_int(value: i64) -> *mut () { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation core::ptr::null_mut() } /// Convert AffineScript Float to host f64 #[no_mangle] pub extern "C" fn float_to_f64(value: *const ()) -> f64 { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation 0.0 } /// Convert host f64 to AffineScript Float #[no_mangle] pub extern "C" fn f64_to_float(value: f64) -> *mut () { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation core::ptr::null_mut() } -// TODO: Phase 6 implementation +// TODO(#84): Phase 6 implementation // - [ ] Implement wasm-bindgen integration // - [ ] Add JSON serialization for complex types // - [ ] Implement async callback support diff --git a/affinescript/runtime/src/gc.rs b/affinescript/runtime/src/gc.rs index 43ec035..8a9a048 100644 --- a/affinescript/runtime/src/gc.rs +++ b/affinescript/runtime/src/gc.rs @@ -68,7 +68,7 @@ pub struct Gc { impl Gc { /// Allocate a new GC-managed value pub fn new(value: T) -> Self { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Allocate space for header + value // - [ ] Initialize header // - [ ] Register in allocation list @@ -128,7 +128,7 @@ static mut GC_STATE: GcState = GcState { /// Initialize the garbage collector pub fn init() { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Set up allocation list // - [ ] Initialize root set // - [ ] Set threshold based on available memory @@ -153,7 +153,7 @@ pub extern "C" fn collect() { /// Mark phase: trace from roots unsafe fn mark_from_roots() { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Mark all roots // - [ ] Recursively mark reachable objects // - [ ] Handle cycles (already marked = skip) @@ -161,7 +161,7 @@ unsafe fn mark_from_roots() { /// Sweep phase: free unmarked objects unsafe fn sweep() { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Walk allocation list // - [ ] Free unmarked objects // - [ ] Clear marks on surviving objects @@ -274,7 +274,7 @@ pub extern "C" fn gc_set_threshold(threshold: usize) { } } -// TODO: Phase 6 implementation +// TODO(#84): Phase 6 implementation // - [ ] Implement proper mark phase with type-based tracing // - [ ] Implement sweep with proper memory deallocation // - [ ] Add write barrier for generational GC (optional) diff --git a/affinescript/runtime/src/lib.rs b/affinescript/runtime/src/lib.rs index 4f7bca7..d740ac7 100644 --- a/affinescript/runtime/src/lib.rs +++ b/affinescript/runtime/src/lib.rs @@ -67,7 +67,7 @@ pub extern "C" fn __affinescript_cleanup() { gc::collect(); } -// TODO: Phase 6 implementation +// TODO(#84): Phase 6 implementation // - [ ] Memory allocator optimized for linear values // - [ ] Effect evidence passing runtime // - [ ] Handler frame management diff --git a/affinescript/runtime/src/panic.rs b/affinescript/runtime/src/panic.rs index a9575d1..1957a9a 100644 --- a/affinescript/runtime/src/panic.rs +++ b/affinescript/runtime/src/panic.rs @@ -78,7 +78,7 @@ pub enum ErrorCode { /// Initialize panic handling pub fn init() { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Set up default panic hook // - [ ] Register with host for error reporting // - [ ] Initialize stack canaries (if enabled) @@ -139,7 +139,7 @@ pub extern "C" fn panic( /// * `code` - Error code indicating the type of error #[no_mangle] pub extern "C" fn panic_code(code: ErrorCode) -> ! { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Convert code to message // - [ ] Call panic hook // - [ ] Trap with code @@ -214,7 +214,7 @@ pub extern "C" fn use_after_move( line: u32, column: u32, ) -> ! { - // TODO: Phase 6 implementation + // TODO(#84): Phase 6 implementation // - [ ] Format error message // - [ ] Include variable name // - [ ] Call panic @@ -235,7 +235,7 @@ pub extern "C" fn borrow_violation( panic(message, message_len, file, file_len, line, column) } -// TODO: Phase 6 implementation +// TODO(#84): Phase 6 implementation // - [ ] Implement WASI error output // - [ ] Add stack trace collection (if debug info available) // - [ ] Add error code documentation diff --git a/affinescript/stdlib/Option.affine b/affinescript/stdlib/Option.affine index b0e8076..5c4e36e 100644 --- a/affinescript/stdlib/Option.affine +++ b/affinescript/stdlib/Option.affine @@ -29,7 +29,7 @@ pub fn unwrap[T](own opt: Option[T]) -> T { return match opt { Some(v) => { return v; }, None => { - // TODO: panic + // TODO(#84): panic return 0; // Placeholder } }; diff --git a/affinescript/stdlib/Result.affine b/affinescript/stdlib/Result.affine index a313b95..442797e 100644 --- a/affinescript/stdlib/Result.affine +++ b/affinescript/stdlib/Result.affine @@ -29,7 +29,7 @@ pub fn unwrap[T, E](own r: Result[T, E]) -> T { return match r { Ok(v) => { return v; }, Err(_) => { - // TODO: panic with error message + // TODO(#84): panic with error message return 0; // Placeholder } }; @@ -47,7 +47,7 @@ pub fn unwrap_or[T, E](own r: Result[T, E], default: T) -> T { pub fn unwrap_err[T, E](own r: Result[T, E]) -> E { return match r { Ok(_) => { - // TODO: panic + // TODO(#84): panic return 0; // Placeholder }, Err(e) => { return e; } diff --git a/affinescript/stdlib/prelude.affine b/affinescript/stdlib/prelude.affine index 2283293..bd0706c 100644 --- a/affinescript/stdlib/prelude.affine +++ b/affinescript/stdlib/prelude.affine @@ -27,7 +27,7 @@ fn unwrap(opt: Option) -> T { Some(value) => value, None => { println("Called unwrap on None"); - // TODO: panic!() once implemented + // TODO(#84): panic!() once implemented } } } @@ -64,7 +64,7 @@ fn unwrap_result(res: Result) -> T { Ok(value) => value, Err(_) => { println("Called unwrap on Err"); - // TODO: panic!() once implemented + // TODO(#84): panic!() once implemented } } } diff --git a/affinescript/stdlib/result.affine b/affinescript/stdlib/result.affine index 56e17ca..6944ae8 100644 --- a/affinescript/stdlib/result.affine +++ b/affinescript/stdlib/result.affine @@ -219,7 +219,7 @@ fn result_or(a: Result, b: Result) -> Result { /// Try block emulation - execute function and catch panics as Err fn try(f: () -> T) -> Result { - // TODO: Requires exception handling support + // TODO(#84): Requires exception handling support try { Ok(f()) } catch { diff --git a/affinescript/test/test_main.ml b/affinescript/test/test_main.ml index 6286f93..75f4bb4 100644 --- a/affinescript/test/test_main.ml +++ b/affinescript/test/test_main.ml @@ -7,7 +7,7 @@ let () = Alcotest.run "AffineScript" ([ ("Lexer", Test_lexer.tests); - (* ("Parser", Test_parser.tests); *) (* TODO: Re-enable when test_parser is implemented *) + (* ("Parser", Test_parser.tests); *) (* TODO(#84): Re-enable when test_parser is implemented *) ("Golden", Test_golden.tests); ("Examples", Test_golden.example_tests); ] @ Test_e2e.tests) diff --git a/affinescript/tools/affine-doc/src/extract.rs b/affinescript/tools/affine-doc/src/extract.rs index ecdaa95..9d5fb1e 100644 --- a/affinescript/tools/affine-doc/src/extract.rs +++ b/affinescript/tools/affine-doc/src/extract.rs @@ -145,7 +145,7 @@ impl Extractor { pub fn extract_file(&self, path: impl AsRef) -> anyhow::Result { let _path = path.as_ref(); - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Parse source file // - [ ] Walk AST // - [ ] Extract doc comments @@ -163,7 +163,7 @@ impl Extractor { pub fn extract_dir(&self, path: impl AsRef) -> anyhow::Result> { let _path = path.as_ref(); - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Find all .afs files // - [ ] Extract each file // - [ ] Build module hierarchy @@ -257,7 +257,7 @@ impl Extractor { match section { "description" => *description = content.to_string(), "params" => { - // TODO: Parse parameter docs + // TODO(#84): Parse parameter docs } "returns" => *returns = Some(content.to_string()), "examples" => examples.push(content.to_string()), @@ -285,7 +285,7 @@ pub struct DocComment { pub safety: Option, } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Connect to AffineScript parser // - [ ] Handle attribute macros (#[doc], #[deprecated], etc.) // - [ ] Extract impl blocks diff --git a/affinescript/tools/affine-doc/src/html.rs b/affinescript/tools/affine-doc/src/html.rs index ab44ae8..98aabf6 100644 --- a/affinescript/tools/affine-doc/src/html.rs +++ b/affinescript/tools/affine-doc/src/html.rs @@ -250,7 +250,7 @@ impl HtmlGenerator { /// Generate search index fn generate_search_index(&self, _modules: &[ModuleDoc]) -> anyhow::Result<()> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Extract searchable content // - [ ] Build JSON index // - [ ] Or build Tantivy index @@ -259,7 +259,7 @@ impl HtmlGenerator { } } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Add navigation sidebar // - [ ] Add breadcrumbs // - [ ] Add source links diff --git a/affinescript/tools/affine-doc/src/index.rs b/affinescript/tools/affine-doc/src/index.rs index c860d0e..ad43eb1 100644 --- a/affinescript/tools/affine-doc/src/index.rs +++ b/affinescript/tools/affine-doc/src/index.rs @@ -211,7 +211,7 @@ fn first_line(text: &str) -> String { .to_string() } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Use Tantivy for full-text search // - [ ] Add fuzzy matching // - [ ] Add type signature search diff --git a/affinescript/tools/affine-doc/src/main.rs b/affinescript/tools/affine-doc/src/main.rs index 0b9f126..71bcbd9 100644 --- a/affinescript/tools/affine-doc/src/main.rs +++ b/affinescript/tools/affine-doc/src/main.rs @@ -93,7 +93,7 @@ fn main() -> anyhow::Result<()> { document_private, include_deps, } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Parse source files // - [ ] Extract documentation // - [ ] Generate HTML @@ -106,7 +106,7 @@ fn main() -> anyhow::Result<()> { #[cfg(feature = "serve")] Commands::Serve { dir, port } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Start HTTP server // - [ ] Serve static files // - [ ] Handle search API @@ -115,7 +115,7 @@ fn main() -> anyhow::Result<()> { } Commands::Index { dir } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Scan HTML files // - [ ] Extract content // - [ ] Build Tantivy index @@ -127,7 +127,7 @@ fn main() -> anyhow::Result<()> { Ok(()) } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Parse AffineScript source and extract types/functions // - [ ] Process doc comments (Markdown) // - [ ] Generate HTML with templates diff --git a/affinescript/tools/affine-doc/src/render.rs b/affinescript/tools/affine-doc/src/render.rs index e687510..ed6a01e 100644 --- a/affinescript/tools/affine-doc/src/render.rs +++ b/affinescript/tools/affine-doc/src/render.rs @@ -19,7 +19,7 @@ pub fn render_markdown(markdown: &str) -> String { /// Render code with syntax highlighting pub fn render_code(code: &str, language: Option<&str>) -> String { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Use syntect for highlighting // - [ ] Support AffineScript syntax // - [ ] Add line numbers option @@ -43,7 +43,7 @@ pub fn html_escape(s: &str) -> String { /// Render a type signature with links pub fn render_signature(signature: &str, _link_resolver: &dyn Fn(&str) -> Option) -> String { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Parse signature // - [ ] Identify type names // - [ ] Create links to type documentation @@ -113,7 +113,7 @@ pub enum Stability { Deprecated, } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Add syntax highlighting for AffineScript // - [ ] Implement cross-reference resolution // - [ ] Add heading anchor links diff --git a/affinescript/tools/affine-pkg/src/build.rs b/affinescript/tools/affine-pkg/src/build.rs index 6e44686..e7684a9 100644 --- a/affinescript/tools/affine-pkg/src/build.rs +++ b/affinescript/tools/affine-pkg/src/build.rs @@ -100,7 +100,7 @@ impl Builder { let _package_dir = package_dir.as_ref(); let start = std::time::Instant::now(); - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Load manifest // - [ ] Resolve dependencies // - [ ] Build dependencies first @@ -120,7 +120,7 @@ impl Builder { pub fn check(&self, package_dir: impl AsRef) -> anyhow::Result> { let _package_dir = package_dir.as_ref(); - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Load manifest // - [ ] Parse all source files // - [ ] Type check @@ -140,7 +140,7 @@ impl Builder { let _package_dir = package_dir.as_ref(); let _filter = filter; - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Find test functions (annotated with #[test]) // - [ ] Build test binary // - [ ] Run tests @@ -160,7 +160,7 @@ impl Builder { let package_dir = package_dir.as_ref(); let output_dir = self.config.target_dir.join("doc"); - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Parse source files // - [ ] Extract doc comments // - [ ] Generate HTML @@ -225,7 +225,7 @@ pub struct TestFailure { pub location: Option, } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Implement incremental compilation // - [ ] Add dependency tracking // - [ ] Add parallel compilation diff --git a/affinescript/tools/affine-pkg/src/config.rs b/affinescript/tools/affine-pkg/src/config.rs index 50142b3..cc26201 100644 --- a/affinescript/tools/affine-pkg/src/config.rs +++ b/affinescript/tools/affine-pkg/src/config.rs @@ -226,7 +226,7 @@ impl Credentials { } } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Add environment variable overrides // - [ ] Add configuration validation // - [ ] Add shell completion config diff --git a/affinescript/tools/affine-pkg/src/lockfile.rs b/affinescript/tools/affine-pkg/src/lockfile.rs index 31290fa..e238100 100644 --- a/affinescript/tools/affine-pkg/src/lockfile.rs +++ b/affinescript/tools/affine-pkg/src/lockfile.rs @@ -140,7 +140,7 @@ impl Default for Lockfile { } } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Add checksum verification // - [ ] Add lockfile merging (for conflicts) // - [ ] Add lockfile diffing diff --git a/affinescript/tools/affine-pkg/src/main.rs b/affinescript/tools/affine-pkg/src/main.rs index 7a0f3d6..30bf5cb 100644 --- a/affinescript/tools/affine-pkg/src/main.rs +++ b/affinescript/tools/affine-pkg/src/main.rs @@ -176,7 +176,7 @@ async fn main() -> anyhow::Result<()> { match cli.command { Commands::New { name, lib } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Create directory structure // - [ ] Generate affine.toml // - [ ] Create src/main.afs or src/lib.afs @@ -184,7 +184,7 @@ async fn main() -> anyhow::Result<()> { } Commands::Init { name, lib } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Generate affine.toml in current directory // - [ ] Create src/ directory let _ = (name, lib); @@ -192,7 +192,7 @@ async fn main() -> anyhow::Result<()> { } Commands::Build { release, package } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Load manifest // - [ ] Resolve dependencies // - [ ] Compile all packages @@ -201,14 +201,14 @@ async fn main() -> anyhow::Result<()> { } Commands::Check { package } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Type check without codegen let _ = package; println!("Checking..."); } Commands::Run { release, args } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Build if needed // - [ ] Run the binary let _ = (release, args); @@ -216,7 +216,7 @@ async fn main() -> anyhow::Result<()> { } Commands::Test { filter, release } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Find test functions // - [ ] Build test binary // - [ ] Run tests @@ -225,7 +225,7 @@ async fn main() -> anyhow::Result<()> { } Commands::Add { dependency, dev, build } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Parse dependency spec // - [ ] Resolve version // - [ ] Update manifest @@ -235,14 +235,14 @@ async fn main() -> anyhow::Result<()> { } Commands::Remove { dependency } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Remove from manifest // - [ ] Update lockfile println!("Removing dependency: {}", dependency); } Commands::Update { package } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Resolve latest compatible versions // - [ ] Update lockfile let _ = package; @@ -250,7 +250,7 @@ async fn main() -> anyhow::Result<()> { } Commands::Install => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Read lockfile // - [ ] Download missing packages // - [ ] Link to content store @@ -258,7 +258,7 @@ async fn main() -> anyhow::Result<()> { } Commands::Publish { dry_run } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Verify package // - [ ] Build tarball // - [ ] Upload to registry @@ -267,41 +267,41 @@ async fn main() -> anyhow::Result<()> { } Commands::Search { query } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Query registry API // - [ ] Display results println!("Searching for: {}", query); } Commands::Info { package } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Fetch package info // - [ ] Display metadata println!("Package info: {}", package); } Commands::Clean => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Remove target/ directory println!("Cleaning..."); } Commands::Fmt { check } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Run formatter let _ = check; println!("Formatting..."); } Commands::Lint { fix } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Run linter let _ = fix; println!("Linting..."); } Commands::Doc { open } => { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Generate docs // - [ ] Open in browser if requested let _ = open; @@ -312,7 +312,7 @@ async fn main() -> anyhow::Result<()> { Ok(()) } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Implement manifest parsing (affine.toml) // - [ ] Implement dependency resolution (SAT solver or PubGrub) // - [ ] Implement content-addressed storage diff --git a/affinescript/tools/affine-pkg/src/manifest.rs b/affinescript/tools/affine-pkg/src/manifest.rs index 58f4325..039a9b4 100644 --- a/affinescript/tools/affine-pkg/src/manifest.rs +++ b/affinescript/tools/affine-pkg/src/manifest.rs @@ -215,7 +215,7 @@ impl Manifest { } } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Add manifest validation // - [ ] Add version validation (semver) // - [ ] Add license validation (SPDX) diff --git a/affinescript/tools/affine-pkg/src/registry.rs b/affinescript/tools/affine-pkg/src/registry.rs index 4d793e2..093a779 100644 --- a/affinescript/tools/affine-pkg/src/registry.rs +++ b/affinescript/tools/affine-pkg/src/registry.rs @@ -152,7 +152,7 @@ impl RegistryClient { /// Search for packages pub async fn search(&self, query: &str, page: u32) -> Result { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // GET /api/v1/search?q={query}&page={page} let _ = (query, page); Ok(SearchResult { @@ -163,7 +163,7 @@ impl RegistryClient { /// Get package info pub async fn get_package(&self, name: &str) -> Result { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // GET /api/v1/packages/{name} let _ = name; Err(RegistryError::NotFound(name.to_string())) @@ -175,7 +175,7 @@ impl RegistryClient { name: &str, version: &Version, ) -> Result { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // GET /api/v1/packages/{name}/{version} let _ = (name, version); Err(RegistryError::NotFound(format!("{}@{}", name, version))) @@ -183,7 +183,7 @@ impl RegistryClient { /// Download package tarball pub async fn download(&self, url: &str) -> Result { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // GET {download_url} let _ = url; Ok(bytes::Bytes::new()) @@ -191,7 +191,7 @@ impl RegistryClient { /// Publish a package pub async fn publish(&self, request: PublishRequest) -> Result<(), RegistryError> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // PUT /api/v1/packages/{name} // Authorization: Bearer {token} let _ = request; @@ -205,7 +205,7 @@ impl RegistryClient { /// Yank a version pub async fn yank(&self, name: &str, version: &Version) -> Result<(), RegistryError> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // DELETE /api/v1/packages/{name}/{version} let _ = (name, version); @@ -218,7 +218,7 @@ impl RegistryClient { /// Unyank a version pub async fn unyank(&self, name: &str, version: &Version) -> Result<(), RegistryError> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // PUT /api/v1/packages/{name}/{version}/unyank let _ = (name, version); @@ -231,7 +231,7 @@ impl RegistryClient { /// Get owners of a package pub async fn get_owners(&self, name: &str) -> Result, RegistryError> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // GET /api/v1/packages/{name}/owners let _ = name; Ok(vec![]) @@ -239,7 +239,7 @@ impl RegistryClient { /// Add an owner pub async fn add_owner(&self, name: &str, user: &str) -> Result<(), RegistryError> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // PUT /api/v1/packages/{name}/owners let _ = (name, user); @@ -251,7 +251,7 @@ impl RegistryClient { } } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Implement actual HTTP requests // - [ ] Add retry logic with backoff // - [ ] Add caching with ETags diff --git a/affinescript/tools/affine-pkg/src/resolve.rs b/affinescript/tools/affine-pkg/src/resolve.rs index 268a8c1..f38cb37 100644 --- a/affinescript/tools/affine-pkg/src/resolve.rs +++ b/affinescript/tools/affine-pkg/src/resolve.rs @@ -117,7 +117,7 @@ impl Resolver { &mut self, _root_deps: &HashMap, ) -> Result { - // TODO: Phase 8 implementation using PubGrub algorithm + // TODO(#84): Phase 8 implementation using PubGrub algorithm // Reference: https://nex3.medium.com/pubgrub-2fb6470504f // // 1. Start with root package requirements @@ -144,7 +144,7 @@ impl Resolver { /// Get available versions for a package fn get_versions(&mut self, _name: &str) -> Result<&[Version], ResolveError> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Check cache // - [ ] Query registry // - [ ] Parse and cache versions @@ -154,7 +154,7 @@ impl Resolver { /// Get package metadata fn get_metadata(&mut self, _id: &PackageId) -> Result<&PackageMetadata, ResolveError> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Check cache // - [ ] Query registry // - [ ] Parse and cache metadata @@ -182,7 +182,7 @@ pub fn parse_requirement(s: &str) -> Result { VersionReq::parse(&normalized) } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Implement full PubGrub algorithm // - [ ] Add version preference (prefer newer, prefer locked) // - [ ] Add feature unification diff --git a/affinescript/tools/affine-pkg/src/storage.rs b/affinescript/tools/affine-pkg/src/storage.rs index f441c27..89e2bdd 100644 --- a/affinescript/tools/affine-pkg/src/storage.rs +++ b/affinescript/tools/affine-pkg/src/storage.rs @@ -84,7 +84,7 @@ impl PackageStore { std::fs::create_dir_all(&pkg_dir)?; // Extract tarball - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Extract tar.gz to pkg_dir // - [ ] Create integrity file @@ -98,7 +98,7 @@ impl PackageStore { _version: &str, _target: impl AsRef, ) -> std::io::Result<()> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Create symlink or copy on Windows // - [ ] Handle nested dependencies @@ -107,7 +107,7 @@ impl PackageStore { /// Garbage collect unused content pub fn gc(&self) -> std::io::Result { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Scan all projects for used packages // - [ ] Remove unreferenced content // - [ ] Return statistics @@ -120,7 +120,7 @@ impl PackageStore { /// Verify store integrity pub fn verify(&self) -> std::io::Result> { - // TODO: Phase 8 implementation + // TODO(#84): Phase 8 implementation // - [ ] Scan all content // - [ ] Verify hashes match // - [ ] Report errors @@ -188,7 +188,7 @@ pub struct VerifyError { pub actual: ContentHash, } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Add parallel extraction // - [ ] Add hardlink support for same-OS // - [ ] Add copy-on-write support (reflinks) diff --git a/affinescript/tools/affine-pkg/src/workspace.rs b/affinescript/tools/affine-pkg/src/workspace.rs index a4dbaf9..2dc80d0 100644 --- a/affinescript/tools/affine-pkg/src/workspace.rs +++ b/affinescript/tools/affine-pkg/src/workspace.rs @@ -156,7 +156,7 @@ impl Workspace { } } -// TODO: Phase 8 implementation +// TODO(#84): Phase 8 implementation // - [ ] Add workspace inheritance for dependencies // - [ ] Add workspace-level features // - [ ] Add parallel builds across workspace diff --git a/affinescript/tools/affinescript-lsp/src/main.rs b/affinescript/tools/affinescript-lsp/src/main.rs index 98e7e2c..714a84f 100644 --- a/affinescript/tools/affinescript-lsp/src/main.rs +++ b/affinescript/tools/affinescript-lsp/src/main.rs @@ -487,7 +487,7 @@ impl LanguageServer for Backend { } async fn code_action(&self, params: CodeActionParams) -> Result> { - // TODO: Phase D — requires structured fix suggestions in --json output + // TODO(#84): Phase D — requires structured fix suggestions in --json output let _ = params; Ok(None) } diff --git a/tests/e2e.sh b/tests/e2e.sh index a6bf954..d19a998 100755 --- a/tests/e2e.sh +++ b/tests/e2e.sh @@ -1,142 +1,12 @@ #!/usr/bin/env bash # SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# RSR Standard E2E Test Template -# -# End-to-end tests validate the full pipeline: build → run → verify output. -# Customise this file for your project. Delete the examples that don't apply. -# -# Usage: -# bash tests/e2e.sh -# just e2e -# -# Merge requirements (STANDING): All 6 test categories must pass before merge: -# P2P, E2E (this file), aspect, execution, lifecycle, benchmarks - +# Run the Burrower -> ECHIDNA -> Isabelle accepted/rejected goal contracts. +# This is a real prover integration check; missing prerequisites are failures. set -euo pipefail - -SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)" -PROJECT_DIR="$(cd "$SCRIPT_DIR/.." && pwd)" - -PASS=0 -FAIL=0 -SKIP=0 - -# ─── Colour helpers ────────────────────────────────────────────────── -green() { printf '\033[32m%s\033[0m\n' "$*"; } -red() { printf '\033[31m%s\033[0m\n' "$*"; } -yellow(){ printf '\033[33m%s\033[0m\n' "$*"; } -bold() { printf '\033[1m%s\033[0m\n' "$*"; } - -# ─── Assertion helpers ─────────────────────────────────────────────── - -# check