logicaffeine_compile/spatial/lower/
rdu.rs

1//! The SambaNova RDU slot: the placed+scheduled IR as a certified neutral placement — the
2//! `logos.spatial.neutral` v2 envelope — honestly SDK-gated for the RDA config bytes.
3//!
4//! ONE envelope serves both RDU lanes. The spatial lane ([`RduSpatialBackend`]) carries the whole IR
5//! under `program` beside its recomputed choreography certificate; the placed-grid lane
6//! (`codegen_sva::backend::RduBackend`) carries its deterministic dump under `grid`. Both name the lane,
7//! both derive the `target` block from the same [`RduChipFacts`] — the chip, its published numbers, the
8//! unit model with every value's provenance, which precisions are witnessed and which are chip-supported
9//! but witness-pending, what is modeled — and both are gated by the ONE sentence [`GATED_REASON`].
10//!
11//! `sections`, `state`, `gathers` and `ii_report` are present and empty: the composed (multi-section,
12//! stateful) form of a program fills them; a reader written today already sees their keys.
13
14use serde::Serialize;
15use serde_json::Value;
16
17use super::{
18    require_verified, Census, NeutralArtifact, SpatialArtifact, SpatialBackend, SpatialLowerError,
19};
20use crate::codegen_sva::fabric_target::{MemHierarchy, Precision, SiliconSpec};
21use crate::spatial::certificate::{certify_choreography, CertifyFault, ChoreographyCertificate};
22use crate::spatial::eval::ChoreoFault;
23use crate::spatial::ir::*;
24use crate::spatial::rdu_chip::{Fact, RduChip, RduChipFacts, RduUnitModel, ScaleUp};
25use crate::spatial::target::{MeshShape, SpatialTarget};
26
27pub const NEUTRAL_SCHEMA: &str = "logos.spatial.neutral";
28pub const NEUTRAL_VERSION: u32 = 2;
29/// The versions [`parse_neutral`] reads: v1 (target block + program + certificate, already shipped) and v2.
30pub const NEUTRAL_VERSIONS_READ: &[u32] = &[1, 2];
31
32/// The one sentence both RDU lanes gate on. Written here once; `RduBackend::GATED_REASON` and
33/// [`RduSpatialBackend::GATED_REASON`] re-export it.
34pub const GATED_REASON: &str = "RDA/SambaFlow config emission is gated on the vendor SDK; the certified placement and schedule are ready to bridge";
35
36pub struct RduSpatialBackend {
37    pub target: SpatialTarget,
38    pub facts: RduChipFacts,
39}
40
41impl RduSpatialBackend {
42    /// The SN40L lane.
43    pub fn new() -> Self {
44        Self::for_chip(RduChip::Sn40l)
45    }
46    /// The lane for one RDU generation, its target derived from that chip's facts.
47    pub fn for_chip(chip: RduChip) -> Self {
48        Self::with_facts(chip.facts())
49    }
50    /// The lane for facts with numbers dropped in (an SDK reading, a probe).
51    pub fn with_facts(facts: RduChipFacts) -> Self {
52        RduSpatialBackend {
53            target: facts.spatial_target(),
54            facts,
55        }
56    }
57    pub const GATED_REASON: &'static str = GATED_REASON;
58}
59
60impl Default for RduSpatialBackend {
61    fn default() -> Self {
62        Self::new()
63    }
64}
65
66impl SpatialBackend for RduSpatialBackend {
67    fn name(&self) -> &str {
68        self.target.name
69    }
70    fn target(&self) -> &SpatialTarget {
71        &self.target
72    }
73    fn lower(&self, p: &SpatialProgram) -> Result<SpatialArtifact, SpatialLowerError> {
74        require_verified(p)?;
75        self.target
76            .scalar_target()
77            .ok_or(SpatialLowerError::Unsupported(
78                "an RDU target without its scalar descriptor",
79            ))?;
80        // A lowering ships only what it proved itself, never a certificate on the program's word: the one the program
81        // carries RECHECKED — every obligation re-derived from the program and held to what the certificate states —
82        // or, when it carries none that rechecks, one derived here.
83        let (certificate, rechecked) = match p.certificate.as_ref().filter(|c| c.recheck(p)) {
84            Some(c) => (c.clone(), true),
85            None => {
86                let mut fresh = p.clone();
87                fresh.certificate = None;
88                (
89                    certify_choreography(&fresh)
90                        .map_err(|f| SpatialLowerError::Uncertified(certify_fault_as_choreo(f)))?,
91                    false,
92                )
93            }
94        };
95        let json = neutral_envelope(
96            &self.target,
97            &self.facts,
98            NeutralBody::Program(p),
99            Some(&certificate),
100        );
101        Ok(SpatialArtifact::SdkGated(NeutralArtifact {
102            json,
103            pretty: pretty_neutral(p),
104            reason: GATED_REASON,
105            certificate,
106            rechecked,
107            census: Census::of(p),
108        }))
109    }
110}
111
112fn certify_fault_as_choreo(f: CertifyFault) -> ChoreoFault {
113    match f {
114        CertifyFault::Eval(e) => e,
115        other => ChoreoFault::Unsupported(format!("certificate: {other:?}")),
116    }
117}
118
119// ── The envelope ─────────────────────────────────────────────────────────────────────────────────
120
121/// Which RDU lane produced an artifact.
122#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize)]
123#[serde(rename_all = "lowercase")]
124pub enum NeutralLane {
125    /// The whole spatial IR: stages, buffers, semaphores, edges, placement, schedule.
126    Spatial,
127    /// A placed scalar grid (`codegen_sva::fabric_grid::Grid`), as its deterministic dump.
128    Grid,
129}
130
131impl NeutralLane {
132    pub fn as_str(self) -> &'static str {
133        match self {
134            NeutralLane::Spatial => "spatial",
135            NeutralLane::Grid => "grid",
136        }
137    }
138}
139
140/// The grid lane's body: the deterministic dump(s) of the placed grid(s).
141#[derive(Clone, Debug, PartialEq, Eq, Serialize)]
142pub struct GridBody {
143    pub name: String,
144    /// The dump — one grid, or every grid of a reconfigurable array joined by `---\n`.
145    pub pretty: String,
146    /// One dump per grid.
147    pub grids: Vec<String>,
148    /// The configuration-select width of a reconfigurable array; `None` for a single grid.
149    pub cfg_width: Option<u32>,
150}
151
152/// What an envelope carries under its lane.
153pub enum NeutralBody<'a> {
154    Program(&'a SpatialProgram),
155    Grid(GridBody),
156}
157
158impl NeutralBody<'_> {
159    pub fn lane(&self) -> NeutralLane {
160        match self {
161            NeutralBody::Program(_) => NeutralLane::Spatial,
162            NeutralBody::Grid(_) => NeutralLane::Grid,
163        }
164    }
165}
166
167/// The precisions block: what the descriptors advertise, what the chip supports that no witness has shipped
168/// for, and the integer every index in the program rides — with its provenance, since a vendor engineer
169/// reading the artifact must see whether that width is published for this part or inherited.
170#[derive(Clone, Debug, PartialEq, Eq, Serialize)]
171pub struct NeutralPrecisions {
172    pub witnessed: Vec<Precision>,
173    pub chip_supported_witness_pending: Vec<Precision>,
174    pub index: Fact<Precision>,
175}
176
177/// The target block: the mesh and the published numbers, the unit model with every value's provenance,
178/// and the modeled ledgers — the descriptor's and the facts'.
179#[derive(Clone, Debug, PartialEq, Serialize)]
180pub struct NeutralTarget {
181    pub name: &'static str,
182    pub chip: RduChip,
183    pub part: &'static str,
184    pub sites: MeshShape,
185    pub silicon: Option<SiliconSpec>,
186    pub mem: MemHierarchy,
187    /// The descriptor's modeled fields.
188    pub modeled: &'static [&'static str],
189    /// The facts' modeled values, by dotted path.
190    pub facts_modeled: Vec<String>,
191    pub unit_model: RduUnitModel,
192    pub precisions: NeutralPrecisions,
193    pub peak_bf16_tflops: u32,
194    pub peak_fp8_tflops: Option<u32>,
195    pub node_nm: u32,
196    pub dies: u32,
197    pub chips_per_node: usize,
198    pub scale_up: Option<ScaleUp>,
199    pub cites: &'static [&'static str],
200}
201
202impl NeutralTarget {
203    pub fn of(target: &SpatialTarget, facts: &RduChipFacts) -> NeutralTarget {
204        NeutralTarget {
205            name: target.name,
206            chip: facts.chip,
207            part: facts.part,
208            sites: target.sites,
209            silicon: target.scalar_target().and_then(|s| s.silicon),
210            mem: target.dram,
211            modeled: target.modeled,
212            facts_modeled: facts.modeled_fields(),
213            unit_model: facts.unit_model,
214            precisions: NeutralPrecisions {
215                witnessed: facts.witnessed.to_vec(),
216                chip_supported_witness_pending: facts.witness_pending.to_vec(),
217                index: facts.index_datatype,
218            },
219            peak_bf16_tflops: facts.peak_bf16_tflops.value,
220            peak_fp8_tflops: facts.peak_fp8_tflops.map(|f| f.value),
221            node_nm: facts.node_nm.value,
222            dies: facts.dies.value,
223            chips_per_node: facts.chips_per_node.value,
224            scale_up: facts.scale_up.map(|f| f.value),
225            cites: facts.cites,
226        }
227    }
228}
229
230#[derive(Serialize)]
231struct NeutralEnvelope<'a> {
232    schema: &'static str,
233    version: u32,
234    lane: NeutralLane,
235    target: NeutralTarget,
236    sections: Vec<Value>,
237    state: Vec<Value>,
238    gathers: Vec<Value>,
239    ii_report: serde_json::Map<String, Value>,
240    #[serde(skip_serializing_if = "Option::is_none")]
241    program: Option<&'a SpatialProgram>,
242    #[serde(skip_serializing_if = "Option::is_none")]
243    grid: Option<GridBody>,
244    certificate: Option<Value>,
245}
246
247/// The certificate summary a reader checks before opening the program: the digest that binds it, the
248/// marked graph's size, the liveness witness, every buffer balance, every semaphore count, every compute
249/// certificate kind, and the numerics claim.
250pub fn certificate_summary(cert: &ChoreographyCertificate) -> Value {
251    let mut v = serde_json::json!({
252        "schedule_digest": cert.schedule_digest,
253        "places": cert.places(),
254        "transitions": cert.transitions(),
255        "liveness_witness": cert.proof.witnesses().first().map(|w| w.topo_order.clone()).unwrap_or_default(),
256        "balances": cert.balances.iter().map(|b| serde_json::json!({
257            "buffer": b.buf.idx(), "depth_pages": b.depth_pages, "reserved": b.reserved, "pushed": b.pushed, "popped": b.popped, "high_water": b.high_water,
258        })).collect::<Vec<_>>(),
259        "sem_counts": cert.sem_counts.iter().map(|(s, n, w)| serde_json::json!([s.idx(), n, w])).collect::<Vec<_>>(),
260        "compute": cert.compute.iter().map(|(s, c)| serde_json::json!([s.idx(), format!("{c:?}")])).collect::<Vec<_>>(),
261        "numerics": cert.numerics,
262    });
263    // A per-section proof carries one order per section over that section's OWN numbering, so the flat
264    // array above is only readable with the cuts beside it. The whole form has no cuts and no key.
265    // The per-section form carries a TABLE of distinct witnesses and, per section, which one it uses.
266    // `liveness_witness` stays the whole form's single order, so a single-section artifact is unchanged.
267    if let (Some(uses), Some(obj)) = (cert.proof.witness_of_section(), v.as_object_mut()) {
268        let table: Vec<&Vec<usize>> = cert
269            .proof
270            .witnesses()
271            .iter()
272            .map(|w| &w.topo_order)
273            .collect();
274        obj.remove("liveness_witness");
275        obj.insert("liveness_witnesses".into(), serde_json::json!(table));
276        obj.insert("liveness_sections".into(), serde_json::json!(uses));
277    }
278    v
279}
280
281/// `logos.spatial.neutral` v2: the lane, the target block derived from the facts, the empty composed-form
282/// sections, the lane's body (the IR itself, every field declaration-ordered — the certificate travels
283/// beside it, never inside — or the grid dump), and the certificate summary when the lane proved one.
284pub fn neutral_envelope(
285    target: &SpatialTarget,
286    facts: &RduChipFacts,
287    body: NeutralBody<'_>,
288    certificate: Option<&ChoreographyCertificate>,
289) -> String {
290    let lane = body.lane();
291    let (program, grid) = match body {
292        NeutralBody::Program(p) => (Some(p), None),
293        NeutralBody::Grid(g) => (None, Some(g)),
294    };
295    let doc = NeutralEnvelope {
296        schema: NEUTRAL_SCHEMA,
297        version: NEUTRAL_VERSION,
298        lane,
299        target: NeutralTarget::of(target, facts),
300        sections: Vec::new(),
301        state: Vec::new(),
302        gathers: Vec::new(),
303        ii_report: serde_json::Map::new(),
304        program,
305        grid,
306        certificate: certificate.map(certificate_summary),
307    };
308    serde_json::to_string(&doc).expect("the envelope serializes")
309}
310
311/// One line per object, in id order: what a vendor engineer reads before opening the JSON.
312pub fn pretty_neutral(p: &SpatialProgram) -> String {
313    let mut out = String::new();
314    let line = |out: &mut String, s: String| {
315        out.push_str(&s);
316        out.push('\n');
317    };
318    line(
319        &mut out,
320        format!(
321            "program {} tile {}x{} phase {:?}",
322            p.name,
323            p.tile.rows,
324            p.tile.cols,
325            p.phase()
326        ),
327    );
328    for t in &p.tensors {
329        line(
330            &mut out,
331            format!(
332                "tensor {} {:?} {}x{} {:?} tiles {}x{}",
333                t.name, t.role, t.elems.rows, t.elems.cols, t.dtype, t.tiles.rows_t, t.tiles.cols_t
334            ),
335        );
336    }
337    let pl = p.placement.as_ref();
338    for s in &p.stages {
339        let site = pl
340            .map(|pl| pl.site_of[s.id.idx()])
341            .map(|si| format!("({},{})", si.x, si.y))
342            .unwrap_or_else(|| "-".into());
343        let engine = pl
344            .map(|pl| format!("{:?}", pl.engine_of[s.id.idx()].engine))
345            .unwrap_or_else(|| "-".into());
346        // The placed name carries an `@x,y` suffix that the `site` column on this very line already
347        // states. A vendor engineer reads this dump to see WHICH STAGE ran WHERE, so print the stage's
348        // own name once and let `site` say where — the suffix was the same fact spelled twice.
349        let stage_name = s
350            .name
351            .split_once('@')
352            .map(|(base, _)| base)
353            .unwrap_or(&s.name);
354        line(
355            &mut out,
356            format!(
357                "stage {} {:?} site {site} engine {engine} ins {:?} outs {:?}",
358                stage_name,
359                s.role,
360                s.ins.iter().map(|b| b.idx()).collect::<Vec<_>>(),
361                s.outs.iter().map(|b| b.idx()).collect::<Vec<_>>()
362            ),
363        );
364    }
365    for b in &p.buffers {
366        line(
367            &mut out,
368            format!(
369                "buffer {} {:?} {:?} site {:?}",
370                b.name,
371                b.kind,
372                b.dtype,
373                b.site.map(|s| (s.x, s.y))
374            ),
375        );
376    }
377    for s in &p.semaphores {
378        line(
379            &mut out,
380            format!(
381                "semaphore {} init {} {:?} operand {:?} sites {}",
382                s.id.idx(),
383                s.init,
384                s.role,
385                s.operand,
386                s.sites.len()
387            ),
388        );
389    }
390    for e in &p.edges {
391        line(
392            &mut out,
393            format!(
394                "edge stage {} -> {:?} via buffer {} {:?}",
395                e.from.idx(),
396                e.to.iter().map(|t| t.idx()).collect::<Vec<_>>(),
397                e.buffer.idx(),
398                e.handshake.kind()
399            ),
400        );
401    }
402    if let Some(pl) = pl {
403        for g in &pl.groups {
404            line(
405                &mut out,
406                format!(
407                    "group {} {:?} {:?} sender ({},{}) rect ({},{})-({},{}) noc {:?}",
408                    g.id.idx(),
409                    g.operand,
410                    g.direction,
411                    g.sender.x,
412                    g.sender.y,
413                    g.rect.x0,
414                    g.rect.y0,
415                    g.rect.x1,
416                    g.rect.y1,
417                    g.noc
418                ),
419            );
420        }
421        for (site, items) in &pl.items_of_site {
422            line(
423                &mut out,
424                format!(
425                    "site ({},{}) items {:?}",
426                    site.x,
427                    site.y,
428                    items.iter().map(|i| i.idx()).collect::<Vec<_>>()
429                ),
430            );
431        }
432    }
433    if let Some(sch) = &p.schedule {
434        for prog in &sch.programs {
435            line(
436                &mut out,
437                format!(
438                    "engine site ({},{}) {:?} ops {}",
439                    prog.site.x,
440                    prog.site.y,
441                    prog.engine,
442                    prog.ops.len()
443                ),
444            );
445        }
446    }
447    out
448}
449
450/// Parse a `logos.spatial.neutral` artifact (v1 or v2, spatial lane) back into the program it describes.
451pub fn parse_neutral(json: &str) -> Result<SpatialProgram, String> {
452    let v: Value = serde_json::from_str(json).map_err(|e| e.to_string())?;
453    let schema = v.get("schema").and_then(Value::as_str).ok_or("no schema")?;
454    if schema != NEUTRAL_SCHEMA {
455        return Err(format!("schema `{schema}` is not `{NEUTRAL_SCHEMA}`"));
456    }
457    let version = v
458        .get("version")
459        .and_then(Value::as_u64)
460        .ok_or("no version")?;
461    if !NEUTRAL_VERSIONS_READ
462        .iter()
463        .any(|k| u64::from(*k) == version)
464    {
465        return Err(format!("{NEUTRAL_SCHEMA} version {version} is not one this reader knows ({NEUTRAL_VERSIONS_READ:?})"));
466    }
467    if version >= 2 {
468        let lane = v
469            .get("lane")
470            .and_then(Value::as_str)
471            .ok_or("a v2 artifact names its lane")?;
472        if lane != NeutralLane::Spatial.as_str() {
473            return Err(format!(
474                "a `{lane}`-lane artifact carries no spatial program (its body is `{lane}`)"
475            ));
476        }
477    }
478    let program = v.get("program").ok_or("no program")?;
479    serde_json::from_value(program.clone()).map_err(|e| e.to_string())
480}
logicaffeine_compile/spatial/lower/rdu.rs

logicaffeine_compile/spatial/lower/
rdu.rs
