valence-shell/0-AI-MANIFEST.a2ml at main · hyperpolymath/valence-shell · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
# SPDX-License-Identifier: MPL-2.0
# 0-AI-MANIFEST.a2ml — AI agent entry point for valence-shell
#
# Lexicographic-first machine-readable file so any agent that does a
# default-sorted directory walk discovers this first. Points at the
# canonical contractile family and the bot_directives/ tree.

[manifest]
project = "valence-shell"
version = "0.9.0"
status = "Advanced research prototype — NOT production-ready"
license = "MPL-2.0"
last-updated = "2026-07-01"

# What this project IS — one-line summary; for the full statement read
# .machine_readable/INTENT.contractile (the load-bearing artefact).
description = "Formally verified Unix-style shell with proven reversibility across 6 proof systems (Coq, Lean 4, Agda, Isabelle/HOL, Mizar, Z3). Implements the MAA (Mutually Assured Accountability) framework."

[entry-points]
# Read these in order at session start.
contractile-purpose       = ".machine_readable/INTENT.contractile"
contractile-must          = ".machine_readable/MUST.contractile"
contractile-trust         = ".machine_readable/TRUST.contractile"
contractile-adjust        = ".machine_readable/ADJUST.contractile"
methodology               = ".machine_readable/bot_directives/methodology.a2ml"
coverage                  = ".machine_readable/bot_directives/coverage.a2ml"
debt                      = ".machine_readable/bot_directives/debt.a2ml"
human-claude-handbook     = "CLAUDE.md"
human-readme              = "README.adoc"
human-explainme           = "EXPLAINME.adoc"
human-faq                 = "FAQ.adoc"

[honest-status]
# The single source of truth for proof debt is docs/PROOF_HOLES_AUDIT.md.
# If you see different numbers anywhere, file an issue.
proof-holes-doc      = "docs/PROOF_HOLES_AUDIT.md"
deep-audit-log-dir   = "docs/audits/"
latest-deep-audit    = "docs/audits/2026-06-01-deep-audit.adoc"

[counts-as-of-last-audit]
# Per docs/audits/2026-06-01-deep-audit.adoc + issue #42 + measured 2026-07-01.
theorem-candidates       = 478
proof-systems            = 6
coq-admits-remaining     = 3       # #56 + #57 + #58 (3 surfaced post-#55)
coq-axioms-justified     = 1       # is_empty_dir_dec
idris2-holes-remaining   = 0       # all closed 2026-07-01 (#152); builds under --total, 2 registered primitive-eq axioms
idris2-partial-markers   = 0       # cleared 2026-06-02
rust-source-files        = 33      # measured 2026-07-01 (impl/rust-cli/src)
rust-loc                 = 22574   # measured 2026-07-01 (impl/rust-cli/src)
tests-passing            = 766     # measured 2026-07-01 (impl/rust-cli); +24 in ffi/rust
tests-ignored            = 14
tests-failing            = 0
fuzz-targets             = 7

[boundary-convention]
# Per estate-standard feedback_estate_boundary_conventions:
in-process-ffi    = "Zig (impl/zig/)"
formal-abi        = "Idris2 (proofs/idris2/)"
beam-native       = "SNIFs — not currently wired"
compile-target    = "typed-wasm — not currently a target"
service-discovery = "Groove Protocol — not currently wired"

[delivery-promises]
# Every agent session must:
# 1. Read INTENT before changing scope.
# 2. Update docs/PROOF_HOLES_AUDIT.md the same commit that changes any proof.
# 3. Keep README/CLAUDE.md numbers in sync with reality (see docs/audits/).
# 4. Never collapse the 6-system polyglot stack (divergent invariant).
update-on-touch = [
  ".machine_readable/INTENT.contractile",
  ".machine_readable/MUST.contractile",
  ".machine_readable/TRUST.contractile",
  ".machine_readable/ADJUST.contractile",
  "docs/PROOF_HOLES_AUDIT.md",
  "docs/audits/",
  "CLAUDE.md",
  "README.adoc",
]