logicaffeine_compile/vm/
isa.rs

1//! R6 — the Tier-5 **Silicon ISA emitter**. The register-VM opcode set becomes the native ISA; each
2//! stencil family maps to a functional unit. This lowers a
3//! [`CompiledProgram`] to LOGOS Silicon ISA assembly — the SAME opcodes the interpreter/VM/JIT/AOT
4//! run, now as the chip's instruction set.
5//!
6//! Every emitted instruction carries its [`RevClass`] — the adiabatic datapath contract:
7//!   • `Bijection` instructions run backward with ZERO garbage (the charge-recovery core);
8//!   • `Journaled` instructions push a minimal Bennett delta;
9//!   • `Effectful` instructions hit the effect log / a named irreversibility barrier;
10//!   • `Control` instructions reverse on the recorded trace.
11//!
12//! Because the classifier [`reversibility`] is TOTAL over the ISA (no `NonReversible`, enforced by
13//! `reverse_op_lock`), the emitter can never lower an unclassified — hence non-reversible-by-omission —
14//! instruction. The `isa_aot_lock` test pins that: every op emits, and every emission is classified.
15
16use crate::vm::instruction::{CompiledProgram, Op};
17use crate::vm::reverse::{reversibility, EffectKind, InverseSpec, JournalKind, RevClass};
18
19/// The reversibility-contract tag for one ISA instruction — the adiabatic annotation the Silicon
20/// backend reads to decide whether an instruction charge-recovers (Bijection) or needs a history cell.
21pub fn rev_tag(op: &Op) -> String {
22    match reversibility(op) {
23        RevClass::Bijection(spec) => {
24            let inv = match spec {
25                InverseSpec::Involution => "self".to_string(),
26                InverseSpec::SelfFamily => "self-family".to_string(),
27                InverseSpec::NamedOp(n) => n.to_string(),
28            };
29            format!("REV   zero-garbage, inverse={inv}  (adiabatic charge-recovery)")
30        }
31        RevClass::Journaled(k) => {
32            let kind = match k {
33                JournalKind::Overwrite => "overwrite",
34                JournalKind::Collection => "collection",
35                JournalKind::InPlace => "in-place",
36                JournalKind::CrdtSnapshot => "crdt-snapshot",
37            };
38            format!("JRNL  Bennett delta ({kind})")
39        }
40        RevClass::Effectful(e) => {
41            let kind = match e {
42                EffectKind::Output => "output-buffer",
43                EffectKind::Clock => "clock-capture",
44                EffectKind::Timer => "virtual-time",
45                EffectKind::Concurrency => "sched-trace",
46                EffectKind::Network => "IRREVERSIBLE-BARRIER (network)",
47            };
48            format!("EFF   {kind}")
49        }
50        RevClass::Control => "CTRL  reverse on trace".to_string(),
51        RevClass::NonReversible(why) => format!("!!!!  UNCLASSIFIED: {why}"),
52    }
53}
54
55/// The mnemonic + operands for one instruction. The reversible-core ops surface their group operands
56/// (place / delta) since those ARE the adiabatic datapath; the rest carry their opcode name.
57fn mnemonic(op: &Op) -> String {
58    match op {
59        Op::RevAdd { place, delta } => format!("REVADD  r{place}, r{delta}"),
60        Op::RevSub { place, delta } => format!("REVSUB  r{place}, r{delta}"),
61        Op::RevXor { place, delta } => format!("REVXOR  r{place}, r{delta}"),
62        Op::RevNeg { place } => format!("REVNEG  r{place}"),
63        Op::RevSwap { a, b } => format!("REVSWAP r{a}, r{b}"),
64        Op::LoadConst { dst, idx } => format!("LOADK   r{dst}, k{idx}"),
65        Op::Move { dst, src } => format!("MOV     r{dst}, r{src}"),
66        Op::Show { .. } => "SHOW".to_string(),
67        Op::Jump { target } => format!("JMP     L{target}"),
68        Op::Halt => "HALT".to_string(),
69        other => other.name().to_uppercase(),
70    }
71}
72
73/// Emit `prog` as LOGOS Silicon ISA assembly text, every instruction annotated with its reversibility
74/// class. Totality is guaranteed by the classifier: an unclassified op cannot compile the crate.
75pub fn emit_isa(prog: &CompiledProgram) -> String {
76    let mut s = String::new();
77    s.push_str("; ============================================================================\n");
78    s.push_str(";  LOGOS Silicon ISA — Tier 5  (register-VM opcode set = native chip ISA)\n");
79    s.push_str(
80        ";  MAKE_A_CHIP §10.1 — each instruction annotated with its reversibility contract.\n",
81    );
82    s.push_str(
83        "; ============================================================================\n\n",
84    );
85
86    // A reversibility budget summary: how much of the program is zero-garbage (adiabatic) vs journaled.
87    let (mut bij, mut jrnl, mut eff, mut ctrl) = (0usize, 0usize, 0usize, 0usize);
88    for op in &prog.code {
89        match reversibility(op) {
90            RevClass::Bijection(_) => bij += 1,
91            RevClass::Journaled(_) => jrnl += 1,
92            RevClass::Effectful(_) => eff += 1,
93            RevClass::Control => ctrl += 1,
94            RevClass::NonReversible(_) => {}
95        }
96    }
97    s.push_str(&format!(
98        ";  reversibility budget: {bij} zero-garbage / {jrnl} journaled / {eff} effect / {ctrl} control\n\n"
99    ));
100
101    s.push_str(".text\n");
102    for (i, op) in prog.code.iter().enumerate() {
103        s.push_str(&format!(
104            "  L{i:<4} {:<24} ; {}\n",
105            mnemonic(op),
106            rev_tag(op)
107        ));
108    }
109
110    if !prog.functions.is_empty() {
111        s.push_str("\n.functions\n");
112        for (fi, f) in prog.functions.iter().enumerate() {
113            s.push_str(&format!(
114                "  fn{fi}: entry=L{}  params={}  regs={}\n",
115                f.entry_pc, f.param_count, f.register_count
116            ));
117        }
118    }
119
120    // The machine-checkable adiabatic contract: what fraction of the datapath charge-recovers.
121    let sched = adiabatic_schedule(prog);
122    s.push_str(&format!(
123        "\n.adiabatic\n  charge-recovery cells: {} ({:.0}%)  |  ancilla (history) cells: {}  |  effect: {}  |  control: {}\n",
124        sched.charge_recovery,
125        sched.charge_recovery_fraction() * 100.0,
126        sched.ancilla,
127        sched.effect,
128        sched.control,
129    ));
130    s
131}
132
133/// The physical cell a Silicon-ISA instruction maps to — the structured (machine-checkable) form of
134/// the `rev_tag` annotation, one per [`RevClass`]. This is the datapath's adiabatic contract:
135/// `ChargeRecovery` cells recycle their charge (zero erased bits); `AncillaWrite` cells write a
136/// Bennett history bit (the only genuine erased-bit source); the rest carry no erased data.
137#[derive(Clone, Copy, PartialEq, Eq, Debug)]
138pub enum CellClass {
139    /// A `Bijection` op — a reversible (adiabatic charge-recovery) functional unit, ZERO erased bits.
140    ChargeRecovery,
141    /// A `Journaled` op — a Bennett history (ancilla) cell; the only cell that can erase information.
142    AncillaWrite,
143    /// An `Effectful` op — an effect-log cell (or, for network, a named irreversibility barrier).
144    EffectLog,
145    /// A `Control` op — reverses on the recorded trace; no datapath cell, no erased data.
146    ControlTrace,
147}
148
149/// The cell an op maps to — derived from the TOTAL [`reversibility`] classifier, so it is exhaustive
150/// by construction (the census `NonReversible` is provably empty, mapped conservatively to an ancilla
151/// cell). Keep in lockstep with [`rev_tag`].
152pub fn cell_class(op: &Op) -> CellClass {
153    match reversibility(op) {
154        RevClass::Bijection(_) => CellClass::ChargeRecovery,
155        RevClass::Journaled(_) => CellClass::AncillaWrite,
156        RevClass::Effectful(_) => CellClass::EffectLog,
157        RevClass::Control => CellClass::ControlTrace,
158        // The census is empty (locked); a hypothetical unclassified op is worst-cased as erasing.
159        RevClass::NonReversible(_) => CellClass::AncillaWrite,
160    }
161}
162
163/// The adiabatic cell budget of a program — the count of each [`CellClass`] its Silicon datapath needs.
164/// The `charge_recovery` fraction is the adiabatic (zero-erasure) share; a program with no ancilla or
165/// effect cells is FULLY ADIABATIC — its Landauer floor is 0, since no cell can erase a bit.
166#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
167pub struct AdiabaticSchedule {
168    pub charge_recovery: usize,
169    pub ancilla: usize,
170    pub effect: usize,
171    pub control: usize,
172}
173
174impl AdiabaticSchedule {
175    /// FULLY ADIABATIC iff the datapath needs no history (ancilla) cell and hits no effect — every
176    /// instruction charge-recovers or reverses on the trace, so nothing can erase a bit. A *sufficient*
177    /// static condition for a Landauer-0 run (the dynamic floor is [`crate::vm::journal::HistoryTape::landauer_bytes`]).
178    pub fn is_fully_adiabatic(&self) -> bool {
179        self.ancilla == 0 && self.effect == 0
180    }
181
182    /// The fraction of instructions on the zero-erasure charge-recovery datapath (`1.0` for empty).
183    pub fn charge_recovery_fraction(&self) -> f64 {
184        let total = self.charge_recovery + self.ancilla + self.effect + self.control;
185        if total == 0 {
186            1.0
187        } else {
188            self.charge_recovery as f64 / total as f64
189        }
190    }
191}
192
193/// Compute the [`AdiabaticSchedule`] — the per-[`CellClass`] cell budget — for a program.
194pub fn adiabatic_schedule(prog: &CompiledProgram) -> AdiabaticSchedule {
195    let mut s = AdiabaticSchedule::default();
196    for op in &prog.code {
197        match cell_class(op) {
198            CellClass::ChargeRecovery => s.charge_recovery += 1,
199            CellClass::AncillaWrite => s.ancilla += 1,
200            CellClass::EffectLog => s.effect += 1,
201            CellClass::ControlTrace => s.control += 1,
202        }
203    }
204    s
205}
206
207/// Where each ISA op lives in silicon — the FULL-SURFACE map. Every op has a home, so the WHOLE
208/// language is silicon-implementable: the realized reversible datapath, the ALU/value datapath (the
209/// build frontier), the instruction sequencer, the load/store + structured-memory unit, or an
210/// off-core coprocessor (runtime services). This is an EXHAUSTIVE match with no wildcard — a new `Op`
211/// cannot compile until it declares its silicon home, so the chip can never silently fail to cover a
212/// language feature. `CoreDatapath` is a monotone floor that RISES as datapath ops are realized in
213/// RTL and proven ≡ VM by our certified SAT (the `silicon_op_support_ratchet` lock).
214#[derive(Clone, Copy, PartialEq, Eq, Debug)]
215pub enum SiliconStatus {
216    /// Realized TODAY in `rev_alu_core.v` — the abelian charge-recovery reversible datapath (wire opcodes 0..4).
217    CoreDatapath,
218    /// A register/value ALU op (arithmetic, bitwise, comparison, moves, constants) — belongs on the core
219    /// datapath; the frontier being grown from `CoreDatapath` op-by-op.
220    Datapath,
221    /// The instruction sequencer — branch / call / return / halt / closure-make; the fetch-decode-PC front-end.
222    Sequencer,
223    /// The load/store + structured-memory unit — collections, structs, enums, tuples, indexing, slicing, iteration, globals.
224    LoadStore,
225    /// An off-core COPROCESSOR / runtime service — I/O, time, policy, CRDTs, concurrency, networking, kernel builtins.
226    Coprocessor,
227}
228
229/// Whether an op is REALIZED in synthesizable silicon TODAY — it has emitted RTL AND its operation is
230/// proven correct by our own certified SAT (not merely classified). This is the ratchet's PROGRESS
231/// metric; it grows as `Datapath` ops are turned into verified hardware. Two realized units:
232/// the reversible charge-recovery core (`rev_alu_core.v`; each op proven a bijection/injective) and
233/// the general integer ALU (`codegen_sva::rtl::emit_alu_datapath_verilog`; arithmetic/bitwise/signed-
234/// comparison ops proven correct by the our-SAT identity battery `the_general_alu_datapath_is_proven
235/// _correct_by_our_sat`). RAISE `SILICON_REALIZED_FLOOR` as ops graduate — never lower it.
236pub fn silicon_realized(op: &Op) -> bool {
237    matches!(
238        op,
239        // reversible charge-recovery core (wire opcodes 0..4) — proven injective by our SAT
240        Op::RevAdd { .. }
241            | Op::RevSub { .. }
242            | Op::RevXor { .. }
243            | Op::RevNeg { .. }
244            | Op::RevSwap { .. }
245            // general integer ALU — combinational; proven correct by the our-SAT identity battery
246            | Op::Add { .. }
247            | Op::AddAssign { .. }
248            | Op::Sub { .. }
249            | Op::Mul { .. }
250            | Op::Pow { .. }
251            | Op::Div { .. }
252            | Op::ExactDiv { .. }
253            | Op::Mod { .. }
254            | Op::FloorDiv { .. }
255            | Op::DivPow2 { .. }
256            | Op::MagicDivU { .. }
257            | Op::BitXor { .. }
258            | Op::BitAnd { .. }
259            | Op::BitOr { .. }
260            | Op::Not { .. }
261            | Op::Shl { .. }
262            | Op::Shr { .. }
263            | Op::Lt { .. }
264            | Op::Gt { .. }
265            | Op::LtEq { .. }
266            | Op::GtEq { .. }
267            | Op::Eq { .. }
268            | Op::ApproxEq { .. }
269            | Op::NotEq { .. }
270            | Op::EnsureOwned { .. }
271            // sequencer + movement ops realized in the soft-core CPU (`soft_core.v`) — see `soft_core_executes`
272            | Op::Move { .. }
273            | Op::LoadConst { .. }
274            | Op::Jump { .. }
275            | Op::JumpIfFalse { .. }
276            | Op::JumpIfTrue { .. }
277            | Op::Halt
278            | Op::Show { .. }
279            | Op::Call { .. }
280            | Op::CallValue { .. }
281            | Op::MakeClosure { .. }
282            | Op::Return { .. }
283            | Op::ReturnNothing
284            | Op::FailWith { .. }
285            // load-store unit (the heap in `soft_core.v` + the ≡VM differential) — see `load_store_realized`
286            | Op::NewList { .. }
287            | Op::NewEmptyList { .. }
288            | Op::NewEmptyListFixed { .. }
289            | Op::NewEmptyListI32 { .. }
290            | Op::NewEmptyMap { .. }
291            | Op::ListPush { .. }
292            | Op::Index { .. }
293            | Op::IndexUnchecked { .. }
294            | Op::Length { .. }
295            | Op::FormatValue { .. }
296            | Op::NewTuple { .. }
297            | Op::ListPop { .. }
298            | Op::Contains { .. }
299            | Op::DestructureTuple { .. }
300            | Op::NewStruct { .. }
301            | Op::StructInsert { .. }
302            | Op::GetField { .. }
303            | Op::SetIndex { .. }
304            | Op::SetIndexUnchecked { .. }
305            | Op::SeqConcat { .. }
306            | Op::Concat { .. }
307            | Op::DeepClone { .. }
308            | Op::IterPrepare { .. }
309            | Op::IterNext { .. }
310            | Op::IterPop
311            | Op::RegionBoundsGuard { .. }
312            | Op::NewInductive { .. }
313            | Op::TestArm { .. }
314            | Op::BindArm { .. }
315            | Op::NewEmptySet { .. }
316            | Op::SetAdd { .. }
317            | Op::NewRange { .. }
318            | Op::UnionOp { .. }
319            | Op::IntersectOp { .. }
320            | Op::RemoveFrom { .. }
321            | Op::SliceOp { .. }
322            | Op::ListPushField { .. }
323            | Op::GlobalGet { .. }
324            | Op::GlobalSet { .. }
325            | Op::Args { .. }
326            // concurrency coprocessor (the FIFO-channel NoC in `soft_core.v`) — see `coprocessor_realized`
327            | Op::ChanNew { .. }
328            | Op::ChanSend { .. }
329            | Op::ChanRecv { .. }
330            | Op::Spawn { .. }
331            | Op::CrdtBump { .. }
332            | Op::CrdtMerge { .. }
333            | Op::CrdtJoin { .. }
334            | Op::BigIntWide { .. }
335            | Op::NewCrdt { .. }
336            | Op::CrdtAppend { .. }
337            | Op::CrdtResolve { .. }
338            | Op::SelectArmRecv { .. }
339            | Op::SelectArmTimeout { .. }
340            | Op::SelectWait { .. }
341            | Op::ChanTrySend { .. }
342            | Op::ChanTryRecv { .. }
343            | Op::Sleep { .. }
344            | Op::LoadToday { .. }
345            | Op::LoadNow { .. }
346            | Op::Obs { .. }
347            | Op::SpawnHandle { .. }
348            | Op::TaskAbort { .. }
349            | Op::TaskAwait { .. }
350            | Op::ChanClose { .. }
351            | Op::CallBuiltin { .. }
352            | Op::CheckPolicy { .. }
353            // offline networking coprocessor (single-node no-ops in `soft_core.v`) — see `coprocessor_realized`
354            | Op::NetConnect { .. }
355            | Op::NetListen { .. }
356            | Op::NetSend { .. }
357            | Op::NetStream { .. }
358            | Op::NetAwait { .. }
359            | Op::NetMakePeer { .. }
360            | Op::NetSync { .. }
361    )
362}
363
364/// The concurrency/coprocessor ops realized as on-core services in `soft_core.v`: the FIFO-channel NoC
365/// (a fixed ring buffer on the heap), proven by the ≡VM differential (buffered send/receive is byte-identical
366/// to the VM's deterministic pipe) + iverilog, decoded at their `binisa` wire opcodes.
367pub fn coprocessor_realized(op: &Op) -> bool {
368    matches!(
369        op,
370        Op::ChanNew { .. }
371            | Op::ChanSend { .. }
372            | Op::ChanRecv { .. }
373            | Op::Spawn { .. }
374            | Op::CrdtBump { .. }
375            | Op::CrdtMerge { .. }
376            | Op::CrdtJoin { .. }
377            | Op::BigIntWide { .. }
378            | Op::NewCrdt { .. }
379            | Op::CrdtAppend { .. }
380            | Op::CrdtResolve { .. }
381            | Op::SelectArmRecv { .. }
382            | Op::SelectArmTimeout { .. }
383            | Op::SelectWait { .. }
384            | Op::ChanTrySend { .. }
385            | Op::ChanTryRecv { .. }
386            | Op::Sleep { .. }
387            | Op::LoadToday { .. }
388            | Op::LoadNow { .. }
389            | Op::Obs { .. }
390            | Op::SpawnHandle { .. }
391            | Op::TaskAbort { .. }
392            | Op::TaskAwait { .. }
393            | Op::ChanClose { .. }
394            | Op::CallBuiltin { .. }
395            | Op::CheckPolicy { .. }
396            | Op::NetConnect { .. }
397            | Op::NetListen { .. }
398            | Op::NetSend { .. }
399            | Op::NetStream { .. }
400            | Op::NetAwait { .. }
401            | Op::NetMakePeer { .. }
402            | Op::NetSync { .. }
403    )
404}
405
406/// The ops the fetch-decode-execute soft-core (`benchmarks/silicon/soft_core.v`) itself decodes and
407/// executes — the movement + control-flow + output ops (as opposed to the value-transform ALU ops
408/// proven by our-SAT identities). Realized by the CPU running real bytecode (iverilog-proven) and by
409/// the `soft_core_decodes_the_wire_opcodes` lock tying its decode to `binisa::opcode`.
410pub fn soft_core_executes(op: &Op) -> bool {
411    matches!(
412        op,
413        Op::Move { .. }
414            | Op::LoadConst { .. }
415            | Op::Jump { .. }
416            | Op::JumpIfFalse { .. }
417            | Op::JumpIfTrue { .. }
418            | Op::Halt
419            | Op::Show { .. }
420            | Op::Call { .. }
421            | Op::CallValue { .. }
422            | Op::MakeClosure { .. }
423            | Op::Return { .. }
424            | Op::ReturnNothing
425            | Op::FailWith { .. }
426    )
427}
428
429/// The load-store ops realized in the soft-core's heap unit (`soft_core.v`'s `dmem`/`hp` + the
430/// `run_soft_core` model): sequence construction, push, indexed read, and length. Proven by the
431/// `the_soft_core_runs_logos_programs_identically_to_the_vm` differential (heap ≡ VM `RuntimeValue::List`)
432/// and decoded at their `binisa` wire opcodes by the `soft_core_decodes_the_wire_opcodes` lock.
433pub fn load_store_realized(op: &Op) -> bool {
434    matches!(
435        op,
436        Op::NewList { .. }
437            | Op::NewEmptyList { .. }
438            | Op::NewEmptyListFixed { .. }
439            | Op::NewEmptyListI32 { .. }
440            | Op::NewEmptyMap { .. }
441            | Op::ListPush { .. }
442            | Op::Index { .. }
443            | Op::IndexUnchecked { .. }
444            | Op::Length { .. }
445            | Op::FormatValue { .. }
446            | Op::NewTuple { .. }
447            | Op::ListPop { .. }
448            | Op::Contains { .. }
449            | Op::DestructureTuple { .. }
450            | Op::NewStruct { .. }
451            | Op::StructInsert { .. }
452            | Op::GetField { .. }
453            | Op::SetIndex { .. }
454            | Op::SetIndexUnchecked { .. }
455            | Op::SeqConcat { .. }
456            | Op::Concat { .. }
457            | Op::DeepClone { .. }
458            | Op::IterPrepare { .. }
459            | Op::IterNext { .. }
460            | Op::IterPop
461            | Op::RegionBoundsGuard { .. }
462            | Op::NewInductive { .. }
463            | Op::TestArm { .. }
464            | Op::BindArm { .. }
465            | Op::NewEmptySet { .. }
466            | Op::SetAdd { .. }
467            | Op::NewRange { .. }
468            | Op::UnionOp { .. }
469            | Op::IntersectOp { .. }
470            | Op::RemoveFrom { .. }
471            | Op::SliceOp { .. }
472            | Op::ListPushField { .. }
473            | Op::GlobalGet { .. }
474            | Op::GlobalSet { .. }
475            | Op::Args { .. }
476    )
477}
478
479/// The silicon home of an op — EXHAUSTIVE (no wildcard), so the full ISA is provably mapped to
480/// hardware and a new op must declare its home. Keep the `CoreDatapath` arm in lockstep with the
481/// realized `rev_alu_core.v` datapath (`binisa` opcodes 0..4).
482pub fn silicon_status(op: &Op) -> SiliconStatus {
483    use SiliconStatus::*;
484    match op {
485        Op::RevAdd { .. }
486        | Op::RevSub { .. }
487        | Op::RevXor { .. }
488        | Op::RevNeg { .. }
489        | Op::RevSwap { .. } => CoreDatapath,
490
491        Op::LoadConst { .. }
492        | Op::Move { .. }
493        | Op::EnsureOwned { .. }
494        | Op::Add { .. }
495        | Op::AddAssign { .. }
496        | Op::Sub { .. }
497        | Op::Mul { .. }
498        | Op::Div { .. }
499        | Op::ExactDiv { .. }
500        | Op::FloorDiv { .. }
501        | Op::Mod { .. }
502        | Op::DivPow2 { .. }
503        | Op::MagicDivU { .. }
504        | Op::Pow { .. }
505        | Op::BitXor { .. }
506        | Op::BitAnd { .. }
507        | Op::BitOr { .. }
508        | Op::Shl { .. }
509        | Op::Shr { .. }
510        | Op::Not { .. }
511        | Op::Lt { .. }
512        | Op::Gt { .. }
513        | Op::LtEq { .. }
514        | Op::GtEq { .. }
515        | Op::Eq { .. }
516        | Op::ApproxEq { .. }
517        | Op::NotEq { .. }
518        | Op::Concat { .. }
519        | Op::SeqConcat { .. } => Datapath,
520
521        Op::Jump { .. }
522        | Op::JumpIfFalse { .. }
523        | Op::JumpIfTrue { .. }
524        | Op::Call { .. }
525        | Op::CallValue { .. }
526        | Op::MakeClosure { .. }
527        | Op::Return { .. }
528        | Op::ReturnNothing
529        | Op::Halt => Sequencer,
530
531        Op::GlobalGet { .. }
532        | Op::GlobalSet { .. }
533        | Op::ListPushField { .. }
534        | Op::NewList { .. }
535        | Op::NewEmptyList { .. }
536        | Op::NewEmptyListFixed { .. }
537        | Op::NewEmptyListI32 { .. }
538        | Op::NewEmptySet { .. }
539        | Op::NewEmptyMap { .. }
540        | Op::NewRange { .. }
541        | Op::ListPush { .. }
542        | Op::SetAdd { .. }
543        | Op::RemoveFrom { .. }
544        | Op::SetIndex { .. }
545        | Op::SetIndexUnchecked { .. }
546        | Op::Index { .. }
547        | Op::IndexUnchecked { .. }
548        | Op::RegionBoundsGuard { .. }
549        | Op::Length { .. }
550        | Op::Contains { .. }
551        | Op::FormatValue { .. }
552        | Op::SliceOp { .. }
553        | Op::DeepClone { .. }
554        | Op::NewTuple { .. }
555        | Op::UnionOp { .. }
556        | Op::IntersectOp { .. }
557        | Op::ListPop { .. }
558        | Op::DestructureTuple { .. }
559        | Op::NewStruct { .. }
560        | Op::StructInsert { .. }
561        | Op::GetField { .. }
562        | Op::NewInductive { .. }
563        | Op::TestArm { .. }
564        | Op::BindArm { .. }
565        | Op::IterPrepare { .. }
566        | Op::IterNext { .. }
567        | Op::IterPop => LoadStore,
568
569        Op::CallBuiltin { .. }
570        | Op::CheckPolicy { .. }
571        | Op::NewEmptyListWithCapacity { .. }
572        | Op::NewEmptyMapWithCapacity { .. }
573        | Op::CrdtBump { .. }
574        | Op::CrdtMerge { .. }
575        | Op::CrdtJoin { .. }
576        | Op::BigIntWide { .. }
577        | Op::NewCrdt { .. }
578        | Op::CrdtAppend { .. }
579        | Op::CrdtResolve { .. }
580        | Op::LoadToday { .. }
581        | Op::LoadNow { .. }
582        | Op::Sleep { .. }
583        | Op::Show { .. }
584        | Op::Obs { .. }
585        | Op::Args { .. }
586        | Op::FailWith { .. }
587        | Op::ChanNew { .. }
588        | Op::ChanSend { .. }
589        | Op::ChanRecv { .. }
590        | Op::ChanTrySend { .. }
591        | Op::ChanTryRecv { .. }
592        | Op::ChanClose { .. }
593        | Op::Spawn { .. }
594        | Op::SpawnHandle { .. }
595        | Op::TaskAwait { .. }
596        | Op::TaskAbort { .. }
597        | Op::SelectArmRecv { .. }
598        | Op::SelectArmTimeout { .. }
599        | Op::SelectWait { .. }
600        | Op::NetConnect { .. }
601        | Op::NetListen { .. }
602        | Op::NetSend { .. }
603        | Op::NetStream { .. }
604        | Op::NetAwait { .. }
605        | Op::NetMakePeer { .. }
606        | Op::NetSync { .. }
607        | Op::Tcp { .. }
608        | Op::Serve { .. } => Coprocessor,
609    }
610}
611
612#[cfg(test)]
613#[path = "../../../logicaffeine_tests/unit/logicaffeine_compile/vm/isa/tests.rs"]
614mod tests;
logicaffeine_compile/vm/isa.rs

logicaffeine_compile/vm/
isa.rs
