Skip to content

Commit 81da2cc

Browse files
arthurpaulinoarthurpaulino
authored
IOBuffer channels (#425)
* Add channel arg to IOBuffer ops for key disambiguation `IOBuffer` gains a per-channel dimension. Each of `io_get_info`, `io_set_info`, `io_read`, `io_write` takes a leading `channel : G`. The same key on different channels resolves to distinct `(idx, len)`, and each channel owns its own data arena. Data model: `data : HashMap G (Array G)` (per-channel arenas), `map : HashMap (G × Array G) IOKeyInfo` (channel-keyed info map). Idx in `IOKeyInfo` is an offset into the channel's arena. All four ops thread the channel through every IR stage (Source/Typed/Simple/Concrete/Bytecode), every pass (Check/Match/Simple/Concretize/Lower/Layout), every evaluator (BytecodeEval/SourceEval/Interpret), the parser (`Meta.lean`), and the Rust executor + FFI wire format. In-repo Aiur sources migrated to pass an explicit channel: existing IxVM kernel/blake3/sha256/ingress/claim code stays on channel 0; `ClaimHarness.addEntries` and `buildSerdeIOBuffer` seed channel-0 entries. The `read_write_io` test now exercises channel disambiguation across channels 0/1/2: reads identical key `[0]` on two channels with distinct arenas, writes the concatenation to a third. `lake test -- aiur-cross`, `lake test -- aiur`, and `lake test -- --ignored ixvm` all pass. `cargo clippy --all-targets` is clean. * Use channels to separate consts/blobs/hints in IxVM Replaces the suffix-byte hack (`addr ++ [0]` for blobs, `addr ++ [1]` for hints) with dedicated IOBuffer channels. The key is always the bare 32-G blake3 hash now. - channel 0: constants - channel 1: blobs - channel 2: reducibility hints `read_byte_stream` gains a leading `channel` argument so callers can read from the arena they queried with `io_get_info`. The blob-vs- constant detection in `load_with_deps` still relies on the empty marker on channel 0 for blob addrs (so a single channel-0 query distinguishes the two cases). Also drops the dead `len == 0` fallback in `load_constant_hint`: IOBuffer aborts on missing keys, so the harness must seed channel 2 for every defn — there is no absence-handling path to take.
1 parent 016c6c7 commit 81da2cc

35 files changed

Lines changed: 475 additions & 330 deletions

‎Benchmarks/Blake3.lean‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -44,10 +44,7 @@ def blake3Bench : IO $ Array BenchReport := do
4444
let data := Array.range dataSize |>.map
4545
-- Add `idx` so every preimage is different and avoids memoization.
4646
fun i => Aiur.G.ofUInt8 (i + idx).toUInt8
47-
let ioKeyInfo := ⟨ioBuffer.data.size, dataSize⟩
48-
{ ioBuffer with
49-
data := ioBuffer.data ++ data
50-
map := ioBuffer.map.insert #[.ofNat idx] ioKeyInfo }
47+
ioBuffer.extend 0 #[.ofNat idx] data
5148
throughput (.ElementsAndBytes numHashes.toUInt64 (dataSize * numHashes).toUInt64 "hashes")
5249
bench s!"dataSize={dataSize} numHashes={numHashes}"
5350
(aiurSystem.prove friParameters funIdx #[Aiur.G.ofNat numHashes]) ioBuffer

‎Benchmarks/Sha256.lean‎

Lines changed: 1 addition & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -44,10 +44,7 @@ def sha256Bench : IO $ Array BenchReport := do
4444
let data := Array.range dataSize |>.map
4545
-- Add `idx` so every preimage is different and avoids memoization.
4646
fun i => Aiur.G.ofUInt8 (i + idx).toUInt8
47-
let ioKeyInfo := ⟨ioBuffer.data.size, dataSize⟩
48-
{ ioBuffer with
49-
data := ioBuffer.data ++ data
50-
map := ioBuffer.map.insert #[.ofNat idx] ioKeyInfo }
47+
ioBuffer.extend 0 #[.ofNat idx] data
5148
throughput (.ElementsAndBytes numHashes.toUInt64 (dataSize * numHashes).toUInt64 "hashes")
5249
bench s!"dataSize={dataSize} numHashes={numHashes}"
5350
(aiurSystem.prove friParameters funIdx #[Aiur.G.ofNat numHashes]) ioBuffer

‎Ix/Aiur/Compiler/Check.lean‎

Lines changed: 21 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -793,33 +793,37 @@ def inferTerm (t : Term) : CheckM Typed.Term := match t with
793793
| .u8FromFieldUnsafe a => do
794794
let a' ← checkNoEscape a .field
795795
pure (Typed.Term.u8FromFieldUnsafe .u8 false a')
796-
| .ioGetInfo key => do
796+
| .ioGetInfo channel key => do
797+
let channel' ← checkNoEscape channel .field
797798
let key' ← inferNoEscape key
798799
match ← walkTyp key'.typ with
799800
| .array .. =>
800-
pure (Typed.Term.ioGetInfo (.tuple #[.field, .field]) false key')
801+
pure (Typed.Term.ioGetInfo (.tuple #[.field, .field]) false channel' key')
801802
| typ' => throw $ .notAnArray typ'
802-
| .ioSetInfo key idx len ret => do
803+
| .ioSetInfo channel key idx len ret => do
804+
let channel' ← checkNoEscape channel .field
803805
let key' ← inferNoEscape key
804806
match ← walkTyp key'.typ with
805807
| .array keyEltTyp _ =>
806808
unless ← unifyTyp keyEltTyp .field do throw $ .typeMismatch .field keyEltTyp
807809
let idx' ← checkNoEscape idx .field
808810
let len' ← checkNoEscape len .field
809811
let ret' ← inferTerm ret
810-
pure (Typed.Term.ioSetInfo ret'.typ ret'.escapes key' idx' len' ret')
812+
pure (Typed.Term.ioSetInfo ret'.typ ret'.escapes channel' key' idx' len' ret')
811813
| typ' => throw $ .notAnArray typ'
812-
| .ioRead idx len => do
814+
| .ioRead channel idx len => do
813815
if len = 0 then throw .emptyArray
816+
let channel' ← checkNoEscape channel .field
814817
let idx' ← checkNoEscape idx .field
815-
pure (Typed.Term.ioRead (.array .field len) false idx' len)
816-
| .ioWrite data ret => do
818+
pure (Typed.Term.ioRead (.array .field len) false channel' idx' len)
819+
| .ioWrite channel data ret => do
820+
let channel' ← checkNoEscape channel .field
817821
let data' ← inferNoEscape data
818822
match ← walkTyp data'.typ with
819823
| .array dataEltTyp _ =>
820824
unless ← unifyTyp dataEltTyp .field do throw $ .typeMismatch .field dataEltTyp
821825
let ret' ← inferTerm ret
822-
pure (Typed.Term.ioWrite ret'.typ ret'.escapes data' ret')
826+
pure (Typed.Term.ioWrite ret'.typ ret'.escapes channel' data' ret')
823827
| typ' => throw $ .notAnArray typ'
824828
| .assertEq a b ret => do
825829
let a' ← inferNoEscape a
@@ -934,12 +938,15 @@ def zonkTypedTerm (t : Typed.Term) : CheckM Typed.Term := match t with
934938
| .ptrVal τ e a => do pure (.ptrVal (← zonkTyp τ) e (← zonkTypedTerm a))
935939
| .assertEq τ e a b r => do
936940
pure (.assertEq (← zonkTyp τ) e (← zonkTypedTerm a) (← zonkTypedTerm b) (← zonkTypedTerm r))
937-
| .ioGetInfo τ e k => do pure (.ioGetInfo (← zonkTyp τ) e (← zonkTypedTerm k))
938-
| .ioSetInfo τ e k i l r => do
939-
pure (.ioSetInfo (← zonkTyp τ) e (← zonkTypedTerm k) (← zonkTypedTerm i)
940-
(← zonkTypedTerm l) (← zonkTypedTerm r))
941-
| .ioRead τ e i n => do pure (.ioRead (← zonkTyp τ) e (← zonkTypedTerm i) n)
942-
| .ioWrite τ e d r => do pure (.ioWrite (← zonkTyp τ) e (← zonkTypedTerm d) (← zonkTypedTerm r))
941+
| .ioGetInfo τ e c k => do
942+
pure (.ioGetInfo (← zonkTyp τ) e (← zonkTypedTerm c) (← zonkTypedTerm k))
943+
| .ioSetInfo τ e c k i l r => do
944+
pure (.ioSetInfo (← zonkTyp τ) e (← zonkTypedTerm c) (← zonkTypedTerm k)
945+
(← zonkTypedTerm i) (← zonkTypedTerm l) (← zonkTypedTerm r))
946+
| .ioRead τ e c i n => do
947+
pure (.ioRead (← zonkTyp τ) e (← zonkTypedTerm c) (← zonkTypedTerm i) n)
948+
| .ioWrite τ e c d r => do
949+
pure (.ioWrite (← zonkTyp τ) e (← zonkTypedTerm c) (← zonkTypedTerm d) (← zonkTypedTerm r))
943950
| .u8BitDecomposition τ e a => do
944951
pure (.u8BitDecomposition (← zonkTyp τ) e (← zonkTypedTerm a))
945952
| .u8ShiftLeft τ e a => do pure (.u8ShiftLeft (← zonkTyp τ) e (← zonkTypedTerm a))

‎Ix/Aiur/Compiler/Concretize.lean‎

Lines changed: 58 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -309,15 +309,21 @@ def termToConcrete
309309
| .assertEq τ e a b r => do
310310
pure (.assertEq (← typToConcrete mono τ) e
311311
(← termToConcrete mono a) (← termToConcrete mono b) (← termToConcrete mono r))
312-
| .ioGetInfo τ e k => do pure (.ioGetInfo (← typToConcrete mono τ) e (← termToConcrete mono k))
313-
| .ioSetInfo τ e k i l r => do
312+
| .ioGetInfo τ e c k => do
313+
pure (.ioGetInfo (← typToConcrete mono τ) e
314+
(← termToConcrete mono c) (← termToConcrete mono k))
315+
| .ioSetInfo τ e c k i l r => do
314316
pure (.ioSetInfo (← typToConcrete mono τ) e
315-
(← termToConcrete mono k) (← termToConcrete mono i)
317+
(← termToConcrete mono c) (← termToConcrete mono k)
318+
(← termToConcrete mono i)
316319
(← termToConcrete mono l) (← termToConcrete mono r))
317-
| .ioRead τ e i n => do pure (.ioRead (← typToConcrete mono τ) e (← termToConcrete mono i) n)
318-
| .ioWrite τ e d r => do
320+
| .ioRead τ e c i n => do
321+
pure (.ioRead (← typToConcrete mono τ) e
322+
(← termToConcrete mono c) (← termToConcrete mono i) n)
323+
| .ioWrite τ e c d r => do
319324
pure (.ioWrite (← typToConcrete mono τ) e
320-
(← termToConcrete mono d) (← termToConcrete mono r))
325+
(← termToConcrete mono c) (← termToConcrete mono d)
326+
(← termToConcrete mono r))
321327
| .u8BitDecomposition τ e a => do
322328
pure (.u8BitDecomposition (← typToConcrete mono τ) e (← termToConcrete mono a))
323329
| .u8ShiftLeft τ e a => do
@@ -521,16 +527,21 @@ def rewriteTypedTerm (decls : Typed.Decls)
521527
.assertEq (rewriteTyp subst mono τ) e
522528
(rewriteTypedTerm decls subst mono a) (rewriteTypedTerm decls subst mono b)
523529
(rewriteTypedTerm decls subst mono r)
524-
| .ioGetInfo τ e k =>
525-
.ioGetInfo (rewriteTyp subst mono τ) e (rewriteTypedTerm decls subst mono k)
526-
| .ioSetInfo τ e k i l r =>
530+
| .ioGetInfo τ e c k =>
531+
.ioGetInfo (rewriteTyp subst mono τ) e
532+
(rewriteTypedTerm decls subst mono c) (rewriteTypedTerm decls subst mono k)
533+
| .ioSetInfo τ e c k i l r =>
527534
.ioSetInfo (rewriteTyp subst mono τ) e
528-
(rewriteTypedTerm decls subst mono k) (rewriteTypedTerm decls subst mono i)
535+
(rewriteTypedTerm decls subst mono c) (rewriteTypedTerm decls subst mono k)
536+
(rewriteTypedTerm decls subst mono i)
529537
(rewriteTypedTerm decls subst mono l) (rewriteTypedTerm decls subst mono r)
530-
| .ioRead τ e i n => .ioRead (rewriteTyp subst mono τ) e (rewriteTypedTerm decls subst mono i) n
531-
| .ioWrite τ e d r =>
538+
| .ioRead τ e c i n =>
539+
.ioRead (rewriteTyp subst mono τ) e
540+
(rewriteTypedTerm decls subst mono c) (rewriteTypedTerm decls subst mono i) n
541+
| .ioWrite τ e c d r =>
532542
.ioWrite (rewriteTyp subst mono τ) e
533-
(rewriteTypedTerm decls subst mono d) (rewriteTypedTerm decls subst mono r)
543+
(rewriteTypedTerm decls subst mono c) (rewriteTypedTerm decls subst mono d)
544+
(rewriteTypedTerm decls subst mono r)
534545
| .u8BitDecomposition τ e a =>
535546
.u8BitDecomposition (rewriteTyp subst mono τ) e (rewriteTypedTerm decls subst mono a)
536547
| .u8ShiftLeft τ e a =>
@@ -636,20 +647,26 @@ def collectInTypedTerm (seen : Std.HashSet (Global × Array Typ)) :
636647
collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) b
637648
| .eqZero τ _ a | .store τ _ a | .load τ _ a | .ptrVal τ _ a | .toField τ _ a
638649
| .u8FromFieldUnsafe τ _ a
639-
| .u8BitDecomposition τ _ a | .u8ShiftLeft τ _ a | .u8ShiftRight τ _ a
640-
| .ioGetInfo τ _ a => collectInTypedTerm (collectInTyp seen τ) a
650+
| .u8BitDecomposition τ _ a | .u8ShiftLeft τ _ a | .u8ShiftRight τ _ a =>
651+
collectInTypedTerm (collectInTyp seen τ) a
652+
| .ioGetInfo τ _ c k =>
653+
collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) c) k
641654
| .proj τ _ a _ | .get τ _ a _ | .slice τ _ a _ _ =>
642655
collectInTypedTerm (collectInTyp seen τ) a
643656
| .set τ _ a _ v => collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) v
644657
| .assertEq τ _ a b r =>
645658
collectInTypedTerm
646659
(collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) a) b) r
647-
| .ioSetInfo τ _ k i l r =>
660+
| .ioSetInfo τ _ c k i l r =>
648661
collectInTypedTerm
649662
(collectInTypedTerm
650-
(collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) k) i) l) r
651-
| .ioRead τ _ i _ => collectInTypedTerm (collectInTyp seen τ) i
652-
| .ioWrite τ _ d r => collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) d) r
663+
(collectInTypedTerm
664+
(collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) c) k) i) l) r
665+
| .ioRead τ _ c i _ =>
666+
collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) c) i
667+
| .ioWrite τ _ c d r =>
668+
collectInTypedTerm
669+
(collectInTypedTerm (collectInTypedTerm (collectInTyp seen τ) c) d) r
653670
| .debug τ _ _ t r =>
654671
let seen := collectInTyp seen τ
655672
let seen := match t with | some t => collectInTypedTerm seen t | none => seen
@@ -700,17 +717,22 @@ def collectCalls (decls : Typed.Decls)
700717
collectCalls decls (collectCalls decls seen a) b
701718
| .eqZero _ _ a | .store _ _ a | .load _ _ a | .ptrVal _ _ a | .toField _ _ a
702719
| .u8FromFieldUnsafe _ _ a
703-
| .u8BitDecomposition _ _ a | .u8ShiftLeft _ _ a | .u8ShiftRight _ _ a
704-
| .ioGetInfo _ _ a => collectCalls decls seen a
720+
| .u8BitDecomposition _ _ a | .u8ShiftLeft _ _ a | .u8ShiftRight _ _ a =>
721+
collectCalls decls seen a
722+
| .ioGetInfo _ _ c k =>
723+
collectCalls decls (collectCalls decls seen c) k
705724
| .proj _ _ a _ | .get _ _ a _ | .slice _ _ a _ _ => collectCalls decls seen a
706725
| .set _ _ a _ v => collectCalls decls (collectCalls decls seen a) v
707726
| .assertEq _ _ a b r =>
708727
collectCalls decls (collectCalls decls (collectCalls decls seen a) b) r
709-
| .ioSetInfo _ _ k i l r =>
728+
| .ioSetInfo _ _ c k i l r =>
710729
collectCalls decls
711-
(collectCalls decls (collectCalls decls (collectCalls decls seen k) i) l) r
712-
| .ioRead _ _ i _ => collectCalls decls seen i
713-
| .ioWrite _ _ d r => collectCalls decls (collectCalls decls seen d) r
730+
(collectCalls decls
731+
(collectCalls decls
732+
(collectCalls decls (collectCalls decls seen c) k) i) l) r
733+
| .ioRead _ _ c i _ => collectCalls decls (collectCalls decls seen c) i
734+
| .ioWrite _ _ c d r =>
735+
collectCalls decls (collectCalls decls (collectCalls decls seen c) d) r
714736
| .debug _ _ _ t r =>
715737
let seen := match t with | some t => collectCalls decls seen t | none => seen
716738
collectCalls decls seen r
@@ -767,14 +789,19 @@ def substInTypedTerm (subst : Global → Option Typ) : Typed.Term → Typed.Term
767789
| .assertEq τ e a b r =>
768790
.assertEq (Typ.instantiate subst τ) e (substInTypedTerm subst a)
769791
(substInTypedTerm subst b) (substInTypedTerm subst r)
770-
| .ioGetInfo τ e k => .ioGetInfo (Typ.instantiate subst τ) e (substInTypedTerm subst k)
771-
| .ioSetInfo τ e k i l r =>
792+
| .ioGetInfo τ e c k =>
793+
.ioGetInfo (Typ.instantiate subst τ) e
794+
(substInTypedTerm subst c) (substInTypedTerm subst k)
795+
| .ioSetInfo τ e c k i l r =>
772796
.ioSetInfo (Typ.instantiate subst τ) e
773-
(substInTypedTerm subst k) (substInTypedTerm subst i)
797+
(substInTypedTerm subst c) (substInTypedTerm subst k)
798+
(substInTypedTerm subst i)
774799
(substInTypedTerm subst l) (substInTypedTerm subst r)
775-
| .ioRead τ e i n => .ioRead (Typ.instantiate subst τ) e (substInTypedTerm subst i) n
776-
| .ioWrite τ e d r => .ioWrite (Typ.instantiate subst τ) e
777-
(substInTypedTerm subst d) (substInTypedTerm subst r)
800+
| .ioRead τ e c i n =>
801+
.ioRead (Typ.instantiate subst τ) e
802+
(substInTypedTerm subst c) (substInTypedTerm subst i) n
803+
| .ioWrite τ e c d r => .ioWrite (Typ.instantiate subst τ) e
804+
(substInTypedTerm subst c) (substInTypedTerm subst d) (substInTypedTerm subst r)
778805
| .u8BitDecomposition τ e a =>
779806
.u8BitDecomposition (Typ.instantiate subst τ) e (substInTypedTerm subst a)
780807
| .u8ShiftLeft τ e a =>

‎Ix/Aiur/Compiler/Layout.lean‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -178,9 +178,9 @@ def opLayout : Bytecode.Op → LayoutM Unit
178178
pushDegrees $ .replicate size 1
179179
bumpAuxiliaries size; bumpLookups; addMemSize size
180180
| .assertEq .. => pure ()
181-
| .ioGetInfo _ => do pushDegrees #[1, 1]; bumpAuxiliaries 2
181+
| .ioGetInfo _ _ => do pushDegrees #[1, 1]; bumpAuxiliaries 2
182182
| .ioSetInfo .. => pure ()
183-
| .ioRead _ len => do pushDegrees $ .replicate len 1; bumpAuxiliaries len
183+
| .ioRead _ _ len => do pushDegrees $ .replicate len 1; bumpAuxiliaries len
184184
| .ioWrite .. => pure ()
185185
| .u8BitDecomposition _ => do pushDegrees $ .replicate 8 1; bumpAuxiliaries 8; bumpLookups
186186
| .u8ShiftLeft _ | .u8ShiftRight _ | .u8Xor .. | .u8And .. | .u8Or .. => do

‎Ix/Aiur/Compiler/Lower.lean‎

Lines changed: 18 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -256,21 +256,25 @@ def toIndex
256256
let b ← toIndex layoutMap bindings b
257257
modify fun stt => { stt with ops := stt.ops.push (.assertEq a b) }
258258
toIndex layoutMap bindings ret
259-
| .ioGetInfo _ _ key => do
259+
| .ioGetInfo _ _ channel key => do
260+
let channel ← expectIdx layoutMap bindings channel
260261
let key ← toIndex layoutMap bindings key
261-
pushOp (.ioGetInfo key) 2
262-
| .ioSetInfo _ _ key idx len ret => do
262+
pushOp (.ioGetInfo channel key) 2
263+
| .ioSetInfo _ _ channel key idx len ret => do
264+
let channel ← expectIdx layoutMap bindings channel
263265
let key ← toIndex layoutMap bindings key
264266
let idx ← expectIdx layoutMap bindings idx
265267
let len ← expectIdx layoutMap bindings len
266-
modify fun stt => { stt with ops := stt.ops.push (.ioSetInfo key idx len) }
268+
modify fun stt => { stt with ops := stt.ops.push (.ioSetInfo channel key idx len) }
267269
toIndex layoutMap bindings ret
268-
| .ioRead _ _ idx len => do
270+
| .ioRead _ _ channel idx len => do
271+
let channel ← expectIdx layoutMap bindings channel
269272
let idx ← expectIdx layoutMap bindings idx
270-
pushOp (.ioRead idx len) len
271-
| .ioWrite _ _ data ret => do
273+
pushOp (.ioRead channel idx len) len
274+
| .ioWrite _ _ channel data ret => do
275+
let channel ← expectIdx layoutMap bindings channel
272276
let data ← toIndex layoutMap bindings data
273-
modify fun stt => { stt with ops := stt.ops.push (.ioWrite data) }
277+
modify fun stt => { stt with ops := stt.ops.push (.ioWrite channel data) }
274278
toIndex layoutMap bindings ret
275279
| .u8BitDecomposition _ _ byte => do
276280
let byte ← expectIdx layoutMap bindings byte
@@ -449,15 +453,17 @@ def Concrete.Term.compile
449453
let b ← toIndex layoutMap bindings b
450454
modify fun stt => { stt with ops := stt.ops.push (.assertEq a b) }
451455
ret.compile returnTyp layoutMap bindings yieldCtrl
452-
| .ioSetInfo _ _ key idx len ret => do
456+
| .ioSetInfo _ _ channel key idx len ret => do
457+
let channel ← toIndex layoutMap bindings channel
453458
let key ← toIndex layoutMap bindings key
454459
let idx ← toIndex layoutMap bindings idx
455460
let len ← toIndex layoutMap bindings len
456-
modify fun stt => { stt with ops := stt.ops.push (.ioSetInfo key idx[0]! len[0]!) }
461+
modify fun stt => { stt with ops := stt.ops.push (.ioSetInfo channel[0]! key idx[0]! len[0]!) }
457462
ret.compile returnTyp layoutMap bindings yieldCtrl
458-
| .ioWrite _ _ data ret => do
463+
| .ioWrite _ _ channel data ret => do
464+
let channel ← toIndex layoutMap bindings channel
459465
let data ← toIndex layoutMap bindings data
460-
modify fun stt => { stt with ops := stt.ops.push (.ioWrite data) }
466+
modify fun stt => { stt with ops := stt.ops.push (.ioWrite channel[0]! data) }
461467
ret.compile returnTyp layoutMap bindings yieldCtrl
462468
| .match _ _ scrut cases defaultOpt => do
463469
let idxs := bindings[scrut]?.getD #[0]

‎Ix/Aiur/Compiler/Match.lean‎

Lines changed: 6 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -370,11 +370,12 @@ def typedToSimple : Term → Simple.Term
370370
| .load τ e a => .load τ e (typedToSimple a)
371371
| .ptrVal τ e a => .ptrVal τ e (typedToSimple a)
372372
| .assertEq τ e a b r => .assertEq τ e (typedToSimple a) (typedToSimple b) (typedToSimple r)
373-
| .ioGetInfo τ e k => .ioGetInfo τ e (typedToSimple k)
374-
| .ioSetInfo τ e k i l r =>
375-
.ioSetInfo τ e (typedToSimple k) (typedToSimple i) (typedToSimple l) (typedToSimple r)
376-
| .ioRead τ e i n => .ioRead τ e (typedToSimple i) n
377-
| .ioWrite τ e d r => .ioWrite τ e (typedToSimple d) (typedToSimple r)
373+
| .ioGetInfo τ e c k => .ioGetInfo τ e (typedToSimple c) (typedToSimple k)
374+
| .ioSetInfo τ e c k i l r =>
375+
.ioSetInfo τ e (typedToSimple c) (typedToSimple k) (typedToSimple i)
376+
(typedToSimple l) (typedToSimple r)
377+
| .ioRead τ e c i n => .ioRead τ e (typedToSimple c) (typedToSimple i) n
378+
| .ioWrite τ e c d r => .ioWrite τ e (typedToSimple c) (typedToSimple d) (typedToSimple r)
378379
| .u8BitDecomposition τ e a => .u8BitDecomposition τ e (typedToSimple a)
379380
| .u8ShiftLeft τ e a => .u8ShiftLeft τ e (typedToSimple a)
380381
| .u8ShiftRight τ e a => .u8ShiftRight τ e (typedToSimple a)

‎Ix/Aiur/Compiler/Simple.lean‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -90,16 +90,18 @@ def simplifyTypedTerm (decls : Source.Decls) : Term → Except CheckError Term
9090
let b' ← simplifyTypedTerm decls b
9191
let r' ← simplifyTypedTerm decls r
9292
pure (.assertEq τ e a' b' r')
93-
| .ioSetInfo τ e k i l r => do
93+
| .ioSetInfo τ e c k i l r => do
94+
let c' ← simplifyTypedTerm decls c
9495
let k' ← simplifyTypedTerm decls k
9596
let i' ← simplifyTypedTerm decls i
9697
let l' ← simplifyTypedTerm decls l
9798
let r' ← simplifyTypedTerm decls r
98-
pure (.ioSetInfo τ e k' i' l' r')
99-
| .ioWrite τ e d r => do
99+
pure (.ioSetInfo τ e c' k' i' l' r')
100+
| .ioWrite τ e c d r => do
101+
let c' ← simplifyTypedTerm decls c
100102
let d' ← simplifyTypedTerm decls d
101103
let r' ← simplifyTypedTerm decls r
102-
pure (.ioWrite τ e d' r')
104+
pure (.ioWrite τ e c' d' r')
103105
| .u8LessThan τ e a b => do
104106
let a' ← simplifyTypedTerm decls a
105107
let b' ← simplifyTypedTerm decls b

0 commit comments

Comments
 (0)