|
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 BQN array primitives accessible without learning APL syntax") |
| 13 | + (decision "Use manifest-driven code generation: user describes WHAT, tool detects patterns and generates BQN") |
| 14 | + (consequences "Users write zero BQN; all array optimisation complexity is in bqniser")) |
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") |
20 | | - (consequences "Compile-time correctness guarantees; zero runtime overhead from proofs")) |
| 18 | + (context "Need verified interop between Rust CLI, CBQN runtime, and user code") |
| 19 | + (decision "Idris2 ABI for formal proofs (BQN types, array layout, rewrite equivalence), Zig FFI for CBQN C-ABI bridge") |
| 20 | + (consequences "Compile-time correctness guarantees; every rewrite has a proof; zero runtime overhead from proofs")) |
21 | 21 |
|
22 | | - (adr "003-rsr-template" |
| 22 | + (adr "003-cbqn-runtime" |
| 23 | + (status "accepted") |
| 24 | + (context "Need a performant BQN execution engine with C FFI") |
| 25 | + (decision "Target CBQN (dzaima/CBQN) as the BQN runtime via its bqnffi.h C API") |
| 26 | + (consequences "In-process BQN evaluation; no serialisation overhead; vectorised SIMD execution")) |
| 27 | + |
| 28 | + (adr "004-pattern-conservative" |
| 29 | + (status "accepted") |
| 30 | + (context "Incorrect rewrites would produce wrong results silently") |
| 31 | + (decision "Only emit BQN rewrites when (a) pattern confidence is high AND (b) Idris2 equivalence proof exists") |
| 32 | + (consequences "False negatives preferred over false positives; users trust the output")) |
| 33 | + |
| 34 | + (adr "005-leading-axis-theory" |
| 35 | + (status "accepted") |
| 36 | + (context "BQN primitives generalise across array ranks via leading-axis theory") |
| 37 | + (decision "BQNiser leverages rank polymorphism: a single rewrite handles scalars, lists, tables, and higher-rank arrays") |
| 38 | + (consequences "Fewer pattern rules needed; rewrites are more general than dimension-specific alternatives")) |
| 39 | + |
| 40 | + (adr "006-rsr-template" |
23 | 41 | (status "accepted") |
24 | 42 | (context "Need consistent project structure across 29+ -iser repos") |
25 | 43 | (decision "All repos cloned from rsr-template-repo with full CI/CD and governance") |
26 | 44 | (consequences "17 workflows, SECURITY.md, CONTRIBUTING, bot directives from day one"))) |
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, manifest parsing, pattern detection, orchestration")) |
| 48 | + (language "BQN" (purpose "Target language for generated array expressions")) |
| 49 | + (language "Idris2" (purpose "ABI formal proofs: types, layout, equivalence")) |
| 50 | + (language "Zig" (purpose "FFI C-ABI bridge to CBQN runtime")) |
| 51 | + (build-tool "cargo" (purpose "Rust CLI")) |
| 52 | + (build-tool "zig build" (purpose "FFI bridge")) |
33 | 53 | (ci "GitHub Actions (17 workflows)")) |
34 | 54 |
|
35 | 55 | (design-rationale |
36 | 56 | (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")))) |
| 57 | + (explanation "User intent captured in bqniser.toml; pattern detection is automatic; generation is deterministic")) |
| 58 | + (principle "Formally verified rewrites" |
| 59 | + (explanation "Idris2 dependent types prove each BQN rewrite preserves input-output equivalence")) |
| 60 | + (principle "Rank-polymorphic by default" |
| 61 | + (explanation "BQN's leading-axis theory means primitives generalise across dimensions automatically")) |
| 62 | + (principle "Conservative rewriting" |
| 63 | + (explanation "Only rewrite when confidence is high and equivalence proof exists; never silently produce wrong results")) |
| 64 | + (principle "In-process execution" |
| 65 | + (explanation "CBQN runs in-process via Zig FFI; no IPC, no serialisation, no subprocess overhead")))) |
0 commit comments