logicaffeine_compile/spatial/
programs.rs

1//! `programs` — the LOGOS source of the reference programs the spatial lane is anchored on.
2//!
3//! ★ WHY A PROGRAM AND NOT A KERNEL. Everything else in `spatial/` describes computation as IR; these
4//! are the ORDINARY LOGOS programs the IR is built from, kept as source so the anchor is the language
5//! rather than any lowering of it. The GEMM oracle below is a scalar integer matmul: compiled to C it
6//! gives a card-free ground truth for every Tenstorrent number, and recognized by `tensor_recognize`
7//! it is the same program the spatial pipeline lowers — which is what makes "the accelerator agrees
8//! with the oracle" a statement about one program rather than two.
9//!
10//! Salvaged from `codegen_tt/matrix.rs` during the retirement; `codegen_tt` re-exports the name so callers
11//! are unmoved.
12
13pub const GEMM_ORACLE_LOGOS: &str = r#"## Main
14Let n be 16.
15Let mutable a be a new Seq of Int.
16Let mutable b be a new Seq of Int.
17Let mutable c be a new Seq of Int.
18Let mutable i be 0.
19While i is less than n:
20    Let mutable j be 0.
21    While j is less than n:
22        Push ((i * n + j) % 255) - 128 to a.
23        Push ((j * n + i) % 255) - 128 to b.
24        Push 0 to c.
25        Set j to j + 1.
26    Set i to i + 1.
27Set i to 0.
28While i is less than n:
29    Let mutable k be 0.
30    While k is less than n:
31        Let mutable j be 0.
32        While j is less than n:
33            Let idx be i * n + j + 1.
34            Set item idx of c to item idx of c + item (i * n + k + 1) of a * item (k * n + j + 1) of b.
35            Set j to j + 1.
36        Set k to k + 1.
37    Set i to i + 1.
38Let mutable checksum be 0.
39Set i to 1.
40While i is at most n * n:
41    Set checksum to checksum + item i of c.
42    Set i to i + 1.
43Show checksum.
44"#;
45
46/// The canonical LOGOS matmul the recognizer lifts: `C(m×n) = A(m×k)·B(k×n)` over `Seq of Int` with the
47/// deterministic fills `a[p] = (p % 7) - 3`, `b[p] = (p % 11) - 5`, and a `Show checksum` of `C` — the
48/// same program the spatial locks anchor on (`tests/common/spatial.rs`), here so a report generator can
49/// lower it without depending on a test tree.
50pub fn gemm_program(m: usize, n: usize, k: usize) -> String {
51    format!(
52        r#"## Main
53Let rows be {m}.
54Let cols be {n}.
55Let mid be {k}.
56Let mutable a be a new Seq of Int.
57Let mutable b be a new Seq of Int.
58Let mutable c be a new Seq of Int.
59Let mutable p be 0.
60While p is less than rows * mid:
61    Push (p % 7) - 3 to a.
62    Set p to p + 1.
63Set p to 0.
64While p is less than mid * cols:
65    Push (p % 11) - 5 to b.
66    Set p to p + 1.
67Set p to 0.
68While p is less than rows * cols:
69    Push 0 to c.
70    Set p to p + 1.
71Let mutable i be 0.
72While i is less than rows:
73    Let mutable k be 0.
74    While k is less than mid:
75        Let mutable j be 0.
76        While j is less than cols:
77            Let idx be i * cols + j + 1.
78            Set item idx of c to item idx of c + item (i * mid + k + 1) of a * item (k * cols + j + 1) of b.
79            Set j to j + 1.
80        Set k to k + 1.
81    Set i to i + 1.
82Let mutable checksum be 0.
83Let mutable q be 1.
84While q is at most rows * cols:
85    Set checksum to checksum + item q of c.
86    Set q to q + 1.
87Show checksum.
88"#
89    )
90}
logicaffeine_compile/spatial/programs.rs

logicaffeine_compile/spatial/
programs.rs
