|
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 | | -;; META.a2ml — Meta-level information for idrisiser |
4 | | - |
5 | | -(meta |
6 | | - (version "0.1.0") |
7 | | - (last-updated "2026-03-21") |
8 | | - |
9 | | - (architecture-decisions |
10 | | - (adr "001-idris2-as-sole-prover" |
11 | | - (status "accepted") |
12 | | - (context "Need a formal verification language for the hyperpolymath ecosystem; candidates were ATS2, Coq, Lean, Agda, and Idris2") |
13 | | - (decision "Idris2 is the sole formal verification language — dependent types, totality checking, elaborator reflection, and quantitative type theory") |
14 | | - (consequences "Single prover simplifies tooling; idrisiser is the universal proof generation frontend")) |
15 | | - |
16 | | - (adr "002-meta-prover-architecture" |
17 | | - (status "accepted") |
18 | | - (context "Developers should not need to learn Idris2 to get formal guarantees") |
19 | | - (decision "Idrisiser parses interface definitions and generates Idris2 proofs automatically — users write manifests, not proof terms") |
20 | | - (consequences "Proof generation is deterministic and reproducible; users get compile-time guarantees without type theory expertise")) |
21 | | - |
22 | | - (adr "003-multi-format-interface-parsing" |
23 | | - (status "accepted") |
24 | | - (context "Interfaces come in many formats: REST APIs, C headers, protobuf, type signatures") |
25 | | - (decision "Pluggable parser architecture with bridge adapters per format, all producing a common IR") |
26 | | - (consequences "New interface formats can be added without changing the proof engine")) |
27 | | - |
28 | | - (adr "004-abi-ffi-standard" |
29 | | - (status "accepted") |
30 | | - (context "Need verified interop between Idris2 proof engine and native output") |
31 | | - (decision "Idris2 ABI for formal proofs, Zig FFI for C-ABI bridge — per hyperpolymath universal standard") |
32 | | - (consequences "Compile-time correctness guarantees; zero runtime overhead from proofs")) |
33 | | - |
34 | | - (adr "005-proof-erasure" |
35 | | - (status "accepted") |
36 | | - (context "Proofs must not impose runtime cost on generated wrappers") |
37 | | - (decision "All proof witnesses are erased during Idris2 compilation (QTT 0-usage)") |
38 | | - (consequences "Native wrapper is as fast as hand-written C; proofs exist only at compile time")) |
39 | | - |
40 | | - (adr "006-no-unsafe-patterns" |
41 | | - (status "accepted") |
42 | | - (context "Generated Idris2 code must be trustworthy") |
43 | | - (decision "Never use believe_me, assert_total, sorry, unsafeCoerce, or any escape hatch in generated code") |
44 | | - (consequences "If a proof cannot be discharged, idrisiser reports a clear error rather than silently unsound output"))) |
45 | | - |
46 | | - (development-practices |
47 | | - (language "Rust" (purpose "CLI orchestrator — parses manifest, invokes parsers and codegen")) |
48 | | - (language "Idris2" (purpose "ABI layer — formal proofs of interface correctness")) |
49 | | - (language "Zig" (purpose "FFI layer — C-ABI bridge implementing proof engine operations")) |
50 | | - (build-tool "cargo" (purpose "Rust CLI build")) |
51 | | - (build-tool "zig build" (purpose "FFI shared/static library build")) |
52 | | - (build-tool "idris2" (purpose "Proof compilation and totality checking")) |
53 | | - (ci "GitHub Actions (17 workflows)")) |
54 | | - |
55 | | - (design-rationale |
56 | | - (principle "Interface-first" |
57 | | - (explanation "The parsed interface is the single source of truth; all proofs, FFI, and native output derive from it")) |
58 | | - (principle "Proof obligations, not proof terms" |
59 | | - (explanation "Idrisiser derives WHAT must be proven from the interface; Idris2 elaborator reflection builds HOW")) |
60 | | - (principle "Deterministic generation" |
61 | | - (explanation "Same manifest + same interface = same output, always; no randomness, no heuristics")) |
62 | | - (principle "Fail loudly on unproven obligations" |
63 | | - (explanation "A proof that cannot be discharged halts generation with a clear diagnostic; never emit unsound code")))) |
| 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 | +# META.a2ml — Idrisiser meta-level information |
| 5 | +[metadata] |
| 6 | +version = "0.1.0" |
| 7 | +last-updated = "2026-03-21" |
| 8 | + |
| 9 | +[project-info] |
| 10 | +license = "PMPL-1.0-or-later" |
| 11 | +author = "Jonathan D.A. Jewell (hyperpolymath)" |
| 12 | + |
| 13 | +[architecture-decisions] |
| 14 | +decisions = [ |
| 15 | + # No ADRs recorded |
| 16 | +] |
| 17 | + |
| 18 | +[development-practices] |
| 19 | +versioning = "SemVer" |
| 20 | +documentation = "AsciiDoc" |
| 21 | +build-tool = "just" |
| 22 | + |
| 23 | +[maintenance-axes] |
| 24 | +scoping-first = true |
| 25 | +axis-1 = "must > intend > like" |
| 26 | +axis-2 = "corrective > adaptive > perfective" |
| 27 | +axis-3 = "systems > compliance > effects" |
0 commit comments