|
4 | 4 |
|
5 | 5 | (meta |
6 | 6 | (version "0.1.0") |
7 | | - (last-updated "2026-03-20") |
| 7 | + (last-updated "2026-03-21") |
8 | 8 |
|
9 | 9 | (architecture-decisions |
10 | | - (adr "001-iser-pattern" |
| 10 | + (adr "001-idris2-as-sole-prover" |
11 | 11 | (status "accepted") |
12 | | - (context "Need to make powerful languages accessible without steep learning curves") |
13 | | - (decision "Use manifest-driven code generation: user describes WHAT, tool generates HOW") |
14 | | - (consequences "Users write zero target language code; all complexity in the -iser")) |
| 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 | 15 |
|
16 | | - (adr "002-abi-ffi-standard" |
| 16 | + (adr "002-meta-prover-architecture" |
17 | 17 | (status "accepted") |
18 | | - (context "Need verified interop between Rust CLI, target language, and user code") |
19 | | - (decision "Idris2 ABI for formal proofs, Zig FFI for C-ABI bridge") |
| 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") |
20 | 32 | (consequences "Compile-time correctness guarantees; zero runtime overhead from proofs")) |
21 | 33 |
|
22 | | - (adr "003-rsr-template" |
| 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" |
23 | 41 | (status "accepted") |
24 | | - (context "Need consistent project structure across 29+ -iser repos") |
25 | | - (decision "All repos cloned from rsr-template-repo with full CI/CD and governance") |
26 | | - (consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one"))) |
| 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"))) |
27 | 45 |
|
28 | 46 | (development-practices |
29 | | - (language "Rust" (purpose "CLI and orchestration")) |
30 | | - (language "Idris2" (purpose "ABI formal proofs")) |
31 | | - (language "Zig" (purpose "FFI C-ABI bridge")) |
32 | | - (build-tool "cargo") |
| 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")) |
33 | 53 | (ci "GitHub Actions (17 workflows)")) |
34 | 54 |
|
35 | 55 | (design-rationale |
36 | | - (principle "Manifest-driven" |
37 | | - (explanation "User intent captured in TOML; all generation is deterministic and reproducible")) |
38 | | - (principle "Formally verified bridges" |
39 | | - (explanation "Idris2 dependent types prove interface correctness at compile time")) |
40 | | - (principle "Zero target language exposure" |
41 | | - (explanation "Users never write Chapel/Julia/Futhark/etc. — the -iser handles everything")))) |
| 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")))) |
0 commit comments