|
1 | | -;; SPDX-License-Identifier: PMPL-1.0-or-later |
2 | | -;; STATE.scm - Project state for absolute-zero |
3 | | -;; Media-Type: application/vnd.state+scm |
| 1 | +# SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +# |
| 4 | +# STATE.a2ml — Absolute Zero project state |
| 5 | +[metadata] |
| 6 | +project = "absolute-zero" |
| 7 | +version = "1.0.0-alpha" |
| 8 | +last-updated = "2026-02-05" |
| 9 | +status = "active" |
| 10 | +session = "converted from scheme — 2026-04-11" |
4 | 11 |
|
5 | | -(state |
6 | | - (metadata |
7 | | - (version "1.0.0-alpha") |
8 | | - (schema-version "1.0") |
9 | | - (created "2026-01-03") |
10 | | - (updated "2026-02-05") |
11 | | - (project "absolute-zero") |
12 | | - (repo "github.com/hyperpolymath/absolute-zero")) |
| 12 | +[project-context] |
| 13 | +name = "Absolute Zero" |
| 14 | +purpose = """Formal Verification of Certified Null Operations""" |
| 15 | +completion-percentage = 65 |
13 | 16 |
|
14 | | - (project-context |
15 | | - (name "Absolute Zero") |
16 | | - (tagline "Formal Verification of Certified Null Operations") |
17 | | - (tech-stack ("Coq" "Lean 4" "Z3" "Agda" "Isabelle" "ReScript" "Rust"))) |
| 17 | +[position] |
| 18 | +phase = "proof-completion" # design | implementation | testing | maintenance | archived |
| 19 | +maturity = "experimental" # experimental | alpha | beta | production | lts |
18 | 20 |
|
19 | | - (current-position |
20 | | - (phase "proof-completion") |
21 | | - (overall-completion 65) |
22 | | - (components |
23 | | - (("coq-proofs" 81 "81 Qed, 19 Admitted, 6 Defined, 63 Axioms") |
24 | | - ("lean4-proofs" 70 "syntax-complete, needs verification") |
25 | | - ("z3-proofs" 90 "10 theorems encoded, needs z3 runtime") |
26 | | - ("agda-proofs" 40 "phase 1 complete") |
27 | | - ("isabelle-proofs" 40 "phase 1 complete") |
28 | | - ("mizar-proofs" 10 "stub, needs installation"))) |
29 | | - (working-features |
30 | | - ("Core CNO theory fully proven" |
31 | | - "Category theory fully proven" |
32 | | - "Statistical mechanics fully proven" |
33 | | - "Lambda calculus 90% proven" |
34 | | - "Quantum computing 70% proven" |
35 | | - "Filesystem 57% proven"))) |
| 21 | +[route-to-mvp] |
| 22 | +milestones = [ |
| 23 | + # No milestones recorded |
| 24 | +] |
36 | 25 |
|
37 | | - (route-to-mvp |
38 | | - (milestones |
39 | | - (("v0.8" "Compliance sprint" "in-progress" 40) |
40 | | - ("v0.9" "Container verification" "not-started" 0) |
41 | | - ("v1.0" "Publication release" "not-started" 0)))) |
| 26 | +[blockers-and-issues] |
| 27 | +issues = [ |
| 28 | + # No blockers recorded |
| 29 | +] |
42 | 30 |
|
43 | | - (blockers-and-issues |
44 | | - (critical) |
45 | | - (high |
46 | | - ("19 Admitted proofs in Coq" |
47 | | - "Python interpreters violate RSR" |
48 | | - "No local coqc for compilation")) |
49 | | - (medium |
50 | | - ("QuantumCNO.v Cexp real-vs-phase bug" |
51 | | - "LandauerDerivation.v needs measure theory")) |
52 | | - (low |
53 | | - ("y_not_cno non-termination proof"))) |
| 31 | +[critical-next-actions] |
| 32 | +actions = [ |
| 33 | + "Complete QuantumCNO.v proofs", |
| 34 | + "Classify FilesystemCNO.v proofs", |
| 35 | + "Classify MalbolgeCore.v proof", |
| 36 | + "Target 12-15 of 19 Admitted proofs", |
| 37 | + "Migrate Python to Rust", |
| 38 | + "Container pipeline", |
| 39 | + "Paper draft", |
| 40 | +] |
54 | 41 |
|
55 | | - (critical-next-actions |
56 | | - (immediate |
57 | | - ("Complete QuantumCNO.v proofs" |
58 | | - "Classify FilesystemCNO.v proofs" |
59 | | - "Classify MalbolgeCore.v proof")) |
60 | | - (this-week |
61 | | - ("Target 12-15 of 19 Admitted proofs" |
62 | | - "Migrate Python to Rust")) |
63 | | - (this-month |
64 | | - ("Container pipeline" |
65 | | - "Paper draft"))) |
66 | | - |
67 | | - (session-history |
68 | | - (("2026-02-05" "opus" "Completed 8 proofs, created PROOF-INSIGHTS.md") |
69 | | - ("2026-02-04" "opus" "Completed cno_logically_reversible, added axioms")))) |
| 42 | +[maintenance-status] |
| 43 | +last-run-utc = "2026-02-05T00:00:00Z" |
| 44 | +last-result = "unknown" # unknown | pass | warn | fail |
0 commit comments