feat: borrow agent-language ideas — contracts-in-evidence, boruna_symbols, agent corpus, quickfix gate

[escapeboy]

Borrows the strongest ideas from the other projects catalogued at agentlanguages.dev, each mapped onto Boruna's determinism + evidence moat. Four disjoint slices, built in parallel and integrated behind full-workspace gates.

What's in it

1. Contract checks → sealed evidence (the differentiator)

requires/ensures were already enforced as runtime guards, but a passing contract left no trace. Now every contract check emits a ContractCheck { function, kind, index, passed } event (both pass and fail) into the hash-chained EventLog, so an evidence bundle now proves every precondition/postcondition held on a run — a compliance artifact none of the verification-camp peers (Vera, Aver) produce.

• New Event::ContractCheck; EVENT_LOG_VERSION 1→2 (backward-read preserved).
• Op::Assert extended to carry kind + clause index; VM records both outcomes then still traps on violation.
• End-to-end test: a ContractCheck survives into a sealed + verify_bundle-passing evidence bundle, and tampering the sealed log fails verification.

2. boruna_symbols MCP tool (zero-training-data mitigation)

13th MCP tool: .ax source → exact typed signatures (fns/records/enums), capabilities, and requires/ensures arity — so coding agents ground on real APIs instead of hallucinating them.

3. Agent-facing corpus (zero-training-data mitigation)

llms.txt + llms-full.txt (.ax teaching primer) + docs/agent/portal.json (machine-readable manifest: caps, 13 libs, 5 templates, 13 tools).

4. Quickfix-coverage CI gate (X07 discipline)

tooling/tests/quickfix_coverage.rs partitions the diagnostic-code registry: every fixable code must ship a repair (proven by a behavioral fixture that emits + applies a real edit) or be allowlisted with a reason. Plus a node-addressed-patch design note.

5. Doc-drift fix (surfaced by the work)

docs/reference/ax-language.md showed syntax that does not compile (record keyword, struct-style enum variants, Enum::Variant match paths). Corrected to the real grammar (type, single-payload variants, bare match patterns), each form verified with boruna lang check.

Verification

Full-workspace gates on the integrated branch: cargo fmt --check clean · cargo clippy --workspace -D warnings zero warnings · cargo test --workspace = 1402 passed / 0 failed (+14 new tests).

Deferred (need a design pass first)

Behavioral certificates (Lean), conformal-confidence gating, type-guided token sampling, M-EVAL benchmark harness.

https://claude.ai/code/session_01BEk2VHyMr1MrSPitnhox5o

[github-actions]

Bench compare

Threshold for regression: ≥ 10% slower mean.

Benchmark	Mean change	99% CI
compile_crud_admin_template	+29.98%	[+24.79%, +34.94%]
compile_medium_program	+4.92%	[+1.88%, +8.56%]
compile_small_program	-1.96%	[-3.47%, -0.71%]
evidence_build_5_steps	-17.90%	[-30.86%, -7.23%]
evidence_build_empty	-8.84%	[-13.50%, -3.86%]
evidence_verify_10_steps	-31.77%	[-41.86%, -18.58%]
evidence_verify_5_steps	+52.01%	[+27.86%, +79.76%]
vm_call_dispatch_loop/iters=1000	-6.45%	[-9.99%, -3.02%]
vm_call_dispatch_loop/iters=10000	-3.19%	[-5.41%, -1.08%]
vm_pure_loop/iters=1000	-2.74%	[-5.00%, -0.85%]
vm_pure_loop/iters=10000	-8.73%	[-12.48%, -5.40%]
vm_pure_loop/iters=100000	-28.76%	[-31.78%, -25.46%]
vm_record_loop/iters=1000	-28.68%	[-32.82%, -24.15%]
vm_record_loop/iters=10000	-21.03%	[-24.86%, -16.85%]

⚠️ 2 benchmark(s) regressed past threshold:

• compile_crud_admin_template
• evidence_verify_5_steps