|
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 | 10 | (adr "001-iser-pattern" |
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 to make K9 contract generation accessible without deep knowledge of contract internals") |
| 13 | + (decision "Use manifest-driven code generation: user points at configs, k9iser generates contracts") |
| 14 | + (consequences "Users write zero K9 contract code by hand; all complexity in k9iser")) |
15 | 15 |
|
16 | 16 | (adr "002-abi-ffi-standard" |
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 "Need verified interop between Rust CLI, validation engine, and K9 contract model") |
| 19 | + (decision "Idris2 ABI for formal proofs of constraint soundness, Zig FFI for C-ABI bridge") |
20 | 20 | (consequences "Compile-time correctness guarantees; zero runtime overhead from proofs")) |
21 | 21 |
|
22 | 22 | (adr "003-rsr-template" |
23 | 23 | (status "accepted") |
24 | 24 | (context "Need consistent project structure across 29+ -iser repos") |
25 | 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"))) |
| 26 | + (consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one")) |
| 27 | + |
| 28 | + (adr "004-four-pillars" |
| 29 | + (status "accepted") |
| 30 | + (context "K9 contracts need a clear structure that maps to the contractile CLI validators") |
| 31 | + (decision "Every K9 contract contains four pillars: must, trust, dust, intend") |
| 32 | + (consequences "Generated contracts are directly consumable by contractile must/trust/dust/intend validators")) |
| 33 | + |
| 34 | + (adr "005-safety-tiers" |
| 35 | + (status "accepted") |
| 36 | + (context "Different configs have different risk profiles — deployment configs vs. logging configs") |
| 37 | + (decision "Three safety tiers: Kennel (read-only), Yard (write files), Hunt (mutate live)") |
| 38 | + (consequences "Users can gate dangerous operations; CI/CD can enforce tier limits")) |
| 39 | + |
| 40 | + (adr "006-multi-format" |
| 41 | + (status "accepted") |
| 42 | + (context "Real-world projects use a mix of TOML, YAML, JSON, and Nickel configs") |
| 43 | + (decision "Support all four formats via a unified config AST") |
| 44 | + (consequences "One constraint inference engine works across all formats; no format lock-in"))) |
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")) |
| 47 | + (language "Rust" (purpose "CLI, orchestration, config parsing, constraint inference, codegen")) |
| 48 | + (language "Idris2" (purpose "ABI formal proofs — constraint soundness, layout correctness")) |
| 49 | + (language "Zig" (purpose "FFI C-ABI bridge — validation engine hot path")) |
| 50 | + (language "Nickel" (purpose "K9 contract output format (.k9.ncl)")) |
32 | 51 | (build-tool "cargo") |
33 | 52 | (ci "GitHub Actions (17 workflows)")) |
34 | 53 |
|
35 | 54 | (design-rationale |
36 | | - (principle "Manifest-driven" |
37 | | - (explanation "User intent captured in TOML; all generation is deterministic and reproducible")) |
| 55 | + (principle "Implicit-to-explicit" |
| 56 | + (explanation "Turn implicit config assumptions into explicit, machine-checked K9 contracts")) |
| 57 | + (principle "Four pillars" |
| 58 | + (explanation "must/trust/dust/intend gives complete coverage of constraint, provenance, hygiene, and intent")) |
38 | 59 | (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")))) |
| 60 | + (explanation "Idris2 dependent types prove constraint completeness and soundness at compile time")) |
| 61 | + (principle "Contractile compatibility" |
| 62 | + (explanation "Generated contracts are first-class inputs to the contractile CLI validator chain")))) |
0 commit comments