From bead2d4bfa07e70e2b3f79b796b8736f1ededabb Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 14 Aug 2025 08:57:54 +0100 Subject: [PATCH 01/11] chore: add example from circt --- .../handshake-to-dc-add.lean | 101 ++++++++++++++++++ 1 file changed, 101 insertions(+) create mode 100644 SSA/Projects/CIRCT/lowering-examples/handshake-to-dc-add.lean diff --git a/SSA/Projects/CIRCT/lowering-examples/handshake-to-dc-add.lean b/SSA/Projects/CIRCT/lowering-examples/handshake-to-dc-add.lean new file mode 100644 index 0000000000..6afaccfa4f --- /dev/null +++ b/SSA/Projects/CIRCT/lowering-examples/handshake-to-dc-add.lean @@ -0,0 +1,101 @@ +import SSA.Projects.CIRCT.DCxComb.DCxCombFunctor +import SSA.Projects.CIRCT.Stream.Stream +import SSA.Projects.CIRCT.Stream.WeakBisim +import SSA.Core.Tactic +import SSA.Core.ErasedContext +import SSA.Core.HVector +import SSA.Core.EffectKind +import SSA.Core.Util +import SSA.Projects.CIRCT.Handshake.Handshake +import SSA.Projects.CIRCT.HSxComb.HSxCombFunctor + + +namespace CIRCTStream + +open MLIR AST in + +instance : ToString DCOp.TokenStream where + toString s := toString (Stream.toList 10 s) + +instance [ToString w] : ToString (Option w) where + toString + | some x => s!"(some {toString x})" + | none => "(none)" + +instance [ToString w] : ToString (DCOp.ValueStream w) where + toString s := toString (Stream.toList 10 s) + +/-- +Initial handshake program: +handshake.func @add(%a : i32, %b : i32 ) -> i32{ + %add1 = comb.add %a, %a : i32 + %syncadd:2 = handshake.sync %add1, %b : i32, i32 + %add2 = comb.add %syncadd#1, %a : i32 + return %add2: i32 +} +-/ +def handshakeAdd := [HSxComb_com| { + ^entry(%a: !Stream_BitVec_32, %b: !Stream_BitVec_32): + %add1 = "HSxComb.add" (%a, %a) : (!Stream_BitVec_32, !Stream_BitVec_32) -> (!Stream_BitVec_32) + %syncAdd = "HSxComb.sync" (%add1, %b) : (!Stream_BitVec_32, !Stream_BitVec_32) -> (!Stream2_BitVec_32) + %syncAdd1 = "HSxComb.snd" (%syncAdd) : (!Stream2_BitVec_32) -> !Stream_BitVec_32 + %add2 = "HSxComb.add" (%syncAdd1, %a) : (!Stream_BitVec_32, !Stream_BitVec_32) -> (!Stream_BitVec_32) + "return" (%add2) : (!Stream_BitVec_32) -> () + }] + + +/-- +Lowered DC program (13d1f6860): +module { + hw.module @add(in %a : !dc.value, in %b : !dc.value, in %clk : !seq.clock {dc.clock}, in %rst : i1 {dc.reset}, out out0 : !dc.value) { + %token, %output = dc.unpack %a : !dc.value + %token_0, %output_1 = dc.unpack %a : !dc.value + %0 = dc.join %token, %token_0 + %1 = comb.add %output, %output_1 : i32 + %2 = dc.pack %0, %1 : i32 + %token_2, %output_3 = dc.unpack %2 : !dc.value + %token_4, %output_5 = dc.unpack %b : !dc.value + %3 = dc.join %token_2, %token_4 + %4 = dc.pack %3, %output_3 : i32 + %5 = dc.pack %3, %output_5 : i32 + %token_6, %output_7 = dc.unpack %5 : !dc.value + %token_8, %output_9 = dc.unpack %a : !dc.value + %6 = dc.join %token_6, %token_8 + %7 = comb.add %output_7, %output_9 : i32 + %8 = dc.pack %6, %7 : i32 + hw.output %8 : !dc.value + } +} +-/ +def dcAdd := [DCxComb_com| { + ^entry(%a: !ValueStream_32, %b: !ValueStream_32): + %unpacka = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) + -- opposit args order wrt. circt + %output = "DCxComb.fstVal" (%unpacka) : (!ValueTokenStream_32) -> (!ValueStream_32) + %token = "DCxComb.sndVal" (%unpacka) : (!ValueTokenStream_32) -> (!TokenStream) + %output1 = "DCxComb.fstVal" (%unpacka) : (!ValueTokenStream_32) -> (!ValueStream_32) + %token0 = "DCxComb.sndVal" (%unpacka) : (!ValueTokenStream_32) -> (!TokenStream) + %0 = "DCxComb.join" (%token, %token0) : (!TokenStream, !TokenStream) -> (!TokenStream) + %1 = "DCxComb.add" (%output, %output1) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) + -- opposite args order wrt. circt + %2 = "DCxComb.pack" (%1, %0) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) + %unpack2 = "DCxComb.unpack" (%2) : (!ValueStream_32) -> (!ValueTokenStream_32) + %output3 = "DCxComb.fstVal" (%unpack2) : (!ValueTokenStream_32) -> (!ValueStream_32) + %token2 = "DCxComb.sndVal" (%unpack2) : (!ValueTokenStream_32) -> (!TokenStream) + %unpackb = "DCxComb.unpack" (%b) : (!ValueStream_32) -> (!ValueTokenStream_32) + %output5 = "DCxComb.fstVal" (%unpackb) : (!ValueTokenStream_32) -> (!ValueStream_32) + %token4 = "DCxComb.sndVal" (%unpackb) : (!ValueTokenStream_32) -> (!TokenStream) + %3 = "DCxComb.join" (%token2, %token4) : (!TokenStream, !TokenStream) -> (!TokenStream) + %4 = "DCxComb.pack" (%output3, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) + %5 = "DCxComb.pack" (%output5, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) + %unpack5 = "DCxComb.unpack" (%5) : (!ValueStream_32) -> (!ValueTokenStream_32) + %output7 = "DCxComb.fstVal" (%unpack5) : (!ValueTokenStream_32) -> (!ValueStream_32) + %token6 = "DCxComb.sndVal" (%unpack5) : (!ValueTokenStream_32) -> (!TokenStream) + %unpackabis = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) + %output9 = "DCxComb.fstVal" (%unpackabis) : (!ValueTokenStream_32) -> (!ValueStream_32) + %token8 = "DCxComb.sndVal" (%unpackabis) : (!ValueTokenStream_32) -> (!TokenStream) + %6 = "DCxComb.join" (%token6, %token8) : (!TokenStream, !TokenStream) -> (!TokenStream) + %7 = "DCxComb.add" (%output7, %output9) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) + %8 = "DCxComb.pack" (%7, %6) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) + "return" (%8) : (!ValueStream_32) -> () + }] From acda52b18b03a4e10a6ba4fb47922126a291264c Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 4 Sep 2025 07:57:06 +0100 Subject: [PATCH 02/11] chore: rebase --- SSA/Projects/CIRCT/Handshake-to-DC/Add.lean | 2 - .../handshake-to-dc-add.lean | 101 ------------------ 2 files changed, 103 deletions(-) delete mode 100644 SSA/Projects/CIRCT/lowering-examples/handshake-to-dc-add.lean diff --git a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean index cf2ca3e2a9..0066f69028 100644 --- a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean +++ b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean @@ -179,8 +179,6 @@ def dcAdd2 := [DCxComb_com| { -- delay-insensitive, hence easier to prove. - - def dcAdd4 := [DCxComb_com| { ^entry(%a: !ValueStream_32, %b: !ValueStream_32): %unpacka = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) diff --git a/SSA/Projects/CIRCT/lowering-examples/handshake-to-dc-add.lean b/SSA/Projects/CIRCT/lowering-examples/handshake-to-dc-add.lean deleted file mode 100644 index 6afaccfa4f..0000000000 --- a/SSA/Projects/CIRCT/lowering-examples/handshake-to-dc-add.lean +++ /dev/null @@ -1,101 +0,0 @@ -import SSA.Projects.CIRCT.DCxComb.DCxCombFunctor -import SSA.Projects.CIRCT.Stream.Stream -import SSA.Projects.CIRCT.Stream.WeakBisim -import SSA.Core.Tactic -import SSA.Core.ErasedContext -import SSA.Core.HVector -import SSA.Core.EffectKind -import SSA.Core.Util -import SSA.Projects.CIRCT.Handshake.Handshake -import SSA.Projects.CIRCT.HSxComb.HSxCombFunctor - - -namespace CIRCTStream - -open MLIR AST in - -instance : ToString DCOp.TokenStream where - toString s := toString (Stream.toList 10 s) - -instance [ToString w] : ToString (Option w) where - toString - | some x => s!"(some {toString x})" - | none => "(none)" - -instance [ToString w] : ToString (DCOp.ValueStream w) where - toString s := toString (Stream.toList 10 s) - -/-- -Initial handshake program: -handshake.func @add(%a : i32, %b : i32 ) -> i32{ - %add1 = comb.add %a, %a : i32 - %syncadd:2 = handshake.sync %add1, %b : i32, i32 - %add2 = comb.add %syncadd#1, %a : i32 - return %add2: i32 -} --/ -def handshakeAdd := [HSxComb_com| { - ^entry(%a: !Stream_BitVec_32, %b: !Stream_BitVec_32): - %add1 = "HSxComb.add" (%a, %a) : (!Stream_BitVec_32, !Stream_BitVec_32) -> (!Stream_BitVec_32) - %syncAdd = "HSxComb.sync" (%add1, %b) : (!Stream_BitVec_32, !Stream_BitVec_32) -> (!Stream2_BitVec_32) - %syncAdd1 = "HSxComb.snd" (%syncAdd) : (!Stream2_BitVec_32) -> !Stream_BitVec_32 - %add2 = "HSxComb.add" (%syncAdd1, %a) : (!Stream_BitVec_32, !Stream_BitVec_32) -> (!Stream_BitVec_32) - "return" (%add2) : (!Stream_BitVec_32) -> () - }] - - -/-- -Lowered DC program (13d1f6860): -module { - hw.module @add(in %a : !dc.value, in %b : !dc.value, in %clk : !seq.clock {dc.clock}, in %rst : i1 {dc.reset}, out out0 : !dc.value) { - %token, %output = dc.unpack %a : !dc.value - %token_0, %output_1 = dc.unpack %a : !dc.value - %0 = dc.join %token, %token_0 - %1 = comb.add %output, %output_1 : i32 - %2 = dc.pack %0, %1 : i32 - %token_2, %output_3 = dc.unpack %2 : !dc.value - %token_4, %output_5 = dc.unpack %b : !dc.value - %3 = dc.join %token_2, %token_4 - %4 = dc.pack %3, %output_3 : i32 - %5 = dc.pack %3, %output_5 : i32 - %token_6, %output_7 = dc.unpack %5 : !dc.value - %token_8, %output_9 = dc.unpack %a : !dc.value - %6 = dc.join %token_6, %token_8 - %7 = comb.add %output_7, %output_9 : i32 - %8 = dc.pack %6, %7 : i32 - hw.output %8 : !dc.value - } -} --/ -def dcAdd := [DCxComb_com| { - ^entry(%a: !ValueStream_32, %b: !ValueStream_32): - %unpacka = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) - -- opposit args order wrt. circt - %output = "DCxComb.fstVal" (%unpacka) : (!ValueTokenStream_32) -> (!ValueStream_32) - %token = "DCxComb.sndVal" (%unpacka) : (!ValueTokenStream_32) -> (!TokenStream) - %output1 = "DCxComb.fstVal" (%unpacka) : (!ValueTokenStream_32) -> (!ValueStream_32) - %token0 = "DCxComb.sndVal" (%unpacka) : (!ValueTokenStream_32) -> (!TokenStream) - %0 = "DCxComb.join" (%token, %token0) : (!TokenStream, !TokenStream) -> (!TokenStream) - %1 = "DCxComb.add" (%output, %output1) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) - -- opposite args order wrt. circt - %2 = "DCxComb.pack" (%1, %0) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) - %unpack2 = "DCxComb.unpack" (%2) : (!ValueStream_32) -> (!ValueTokenStream_32) - %output3 = "DCxComb.fstVal" (%unpack2) : (!ValueTokenStream_32) -> (!ValueStream_32) - %token2 = "DCxComb.sndVal" (%unpack2) : (!ValueTokenStream_32) -> (!TokenStream) - %unpackb = "DCxComb.unpack" (%b) : (!ValueStream_32) -> (!ValueTokenStream_32) - %output5 = "DCxComb.fstVal" (%unpackb) : (!ValueTokenStream_32) -> (!ValueStream_32) - %token4 = "DCxComb.sndVal" (%unpackb) : (!ValueTokenStream_32) -> (!TokenStream) - %3 = "DCxComb.join" (%token2, %token4) : (!TokenStream, !TokenStream) -> (!TokenStream) - %4 = "DCxComb.pack" (%output3, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) - %5 = "DCxComb.pack" (%output5, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) - %unpack5 = "DCxComb.unpack" (%5) : (!ValueStream_32) -> (!ValueTokenStream_32) - %output7 = "DCxComb.fstVal" (%unpack5) : (!ValueTokenStream_32) -> (!ValueStream_32) - %token6 = "DCxComb.sndVal" (%unpack5) : (!ValueTokenStream_32) -> (!TokenStream) - %unpackabis = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) - %output9 = "DCxComb.fstVal" (%unpackabis) : (!ValueTokenStream_32) -> (!ValueStream_32) - %token8 = "DCxComb.sndVal" (%unpackabis) : (!ValueTokenStream_32) -> (!TokenStream) - %6 = "DCxComb.join" (%token6, %token8) : (!TokenStream, !TokenStream) -> (!TokenStream) - %7 = "DCxComb.add" (%output7, %output9) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) - %8 = "DCxComb.pack" (%7, %6) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) - "return" (%8) : (!ValueStream_32) -> () - }] From c981dbe8cbe4b428f403c2d5b162fd55e7c70edb Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 21 Aug 2025 10:01:18 +0100 Subject: [PATCH 03/11] chore: add --- SSA/Projects/CIRCT/Handshake-to-DC/Add.lean | 47 ++++++++++++++++++--- 1 file changed, 41 insertions(+), 6 deletions(-) diff --git a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean index 0066f69028..a62ec9f142 100644 --- a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean +++ b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean @@ -171,14 +171,13 @@ def dcAdd2 := [DCxComb_com| { %5 = "DCxComb.pack" (%4, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) "return" (%5) : (!ValueStream_32) -> () }] -#check dcAdd2 -#eval dcAdd2 -#reduce dcAdd2 -#check dcAdd2.denote -#print axioms dcAdd2 +#check dcAdd' +#eval dcAdd' +#reduce dcAdd' +#check dcAdd'.denote +#print axioms dcAdd' -- delay-insensitive, hence easier to prove. - def dcAdd4 := [DCxComb_com| { ^entry(%a: !ValueStream_32, %b: !ValueStream_32): %unpacka = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) @@ -248,6 +247,42 @@ theorem equiv_add (a : (BitVec 32)) : -- theorem equiv_add_dcxcomb (a : DCOp.ValueStream (BitVec 32)) : -- ((DCxCombFunctor.Op.comb add).denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) -- ((DCxCombFunctor.Op.comb shlPar 2).denote (Ctxt.Valuation.ofHVector (.cons a <| .nil))) := by sorry +#check dcAdd' +#eval dcAdd' +#reduce dcAdd' +#check dcAdd'.denote +#print axioms dcAdd' +-- delay-insensitive, hence easier to prove/reason about. + + + + + + + + + + + +-- def dcShl := [DCxComb_com| { +-- ^entry(%a: !ValueStream_32, %b: !ValueStream_32): +-- %unpacka = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) +-- -- opposit args order wrt. circt +-- %output = "DCxComb.fstVal" (%unpacka) : (!ValueTokenStream_32) -> (!ValueStream_32) +-- %token = "DCxComb.sndVal" (%unpacka) : (!ValueTokenStream_32) -> (!TokenStream) +-- -- %fork = "DCxComb.fork" (%token) : (!TokenStream) -> (!TokenStream2) keep this implicit +-- %2 = "DCxComb.shiftLeft" (%output, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) +-- %b2 = "DCxComb.add" (%2, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) +-- -- %c2 = "DCxComb.add" (%b2, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) +-- %unpackb = "DCxComb.unpack" (%b) : (!ValueStream_32) -> (!ValueTokenStream_32) +-- -- opposit args order wrt. circt +-- %output1 = "DCxComb.fstVal" (%unpackb) : (!ValueTokenStream_32) -> (!ValueStream_32) +-- %token0 = "DCxComb.sndVal" (%unpackb) : (!ValueTokenStream_32) -> (!TokenStream) +-- %3 = "DCxComb.join" (%token, %token0) : (!TokenStream, !TokenStream) -> (!TokenStream) +-- %4 = "DCxComb.add" (%b2, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) +-- %5 = "DCxComb.pack" (%4, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) +-- "return" (%5) : (!ValueStream_32) -> () +-- }] -- theorem dc_eq (a b: DCOp.ValueStream (BitVec 32)) : -- (dcAdd4.denote (Valuation.ofHVector (.cons a <| .cons b <| .nil))) = DCxComb.shiftLeft a >> 2 := by sorry From 235395260953e98da05eb966f6ac135985326574 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 21 Aug 2025 11:20:11 +0100 Subject: [PATCH 04/11] chore: make file compile --- SSA/Projects/CIRCT/Handshake-to-DC/Add.lean | 68 +++++++++++++-------- 1 file changed, 42 insertions(+), 26 deletions(-) diff --git a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean index a62ec9f142..a9e452c86a 100644 --- a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean +++ b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean @@ -171,13 +171,16 @@ def dcAdd2 := [DCxComb_com| { %5 = "DCxComb.pack" (%4, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) "return" (%5) : (!ValueStream_32) -> () }] -#check dcAdd' -#eval dcAdd' -#reduce dcAdd' -#check dcAdd'.denote -#print axioms dcAdd' +#check dcAdd2 +#eval dcAdd2 +#reduce dcAdd2 +#check dcAdd2.denote +#print axioms dcAdd2 -- delay-insensitive, hence easier to prove. + + + def dcAdd4 := [DCxComb_com| { ^entry(%a: !ValueStream_32, %b: !ValueStream_32): %unpacka = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) @@ -255,34 +258,47 @@ theorem equiv_add (a : (BitVec 32)) : -- delay-insensitive, hence easier to prove/reason about. +def dcShl := [DCxComb_com| { + ^entry(%a: !ValueStream_32, %b: !ValueStream_32): + %unpacka = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) + -- opposit args order wrt. circt + %output = "DCxComb.fstVal" (%unpacka) : (!ValueTokenStream_32) -> (!ValueStream_32) + %token = "DCxComb.sndVal" (%unpacka) : (!ValueTokenStream_32) -> (!TokenStream) + -- %fork = "DCxComb.fork" (%token) : (!TokenStream) -> (!TokenStream2) keep this implicit + %2 = "DCxComb.shlPar_1" (%output) : (!ValueStream_32) -> (!ValueStream_32) + %unpackb = "DCxComb.unpack" (%b) : (!ValueStream_32) -> (!ValueTokenStream_32) + -- opposit args order wrt. circt + %output1 = "DCxComb.fstVal" (%unpackb) : (!ValueTokenStream_32) -> (!ValueStream_32) + %token0 = "DCxComb.sndVal" (%unpackb) : (!ValueTokenStream_32) -> (!TokenStream) + %3 = "DCxComb.join" (%token, %token0) : (!TokenStream, !TokenStream) -> (!TokenStream) + %4 = "DCxComb.add" (%2, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) + %5 = "DCxComb.pack" (%4, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) + "return" (%5) : (!ValueStream_32) -> () +}] +def testDCAdd2 : DCOp.ValueStream (BitVec 32) := + dcAdd2.denote (Ctxt.Valuation.ofHVector (.cons a <| .cons b <| .nil)) +def testDCShl2 : DCOp.ValueStream (BitVec 32) := + dcShl.denote (Ctxt.Valuation.ofHVector (.cons a <| .cons b <| .nil)) +#eval testDCAdd2 +#eval testDCShl2 +theorem equiv_add_shl (a : DCOp.ValueStream (BitVec 32)) : + (dcAdd2.denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) = (dcShl.denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) := by + simp [dcAdd2, dcShl] + sorry +theorem equiv_add (a : (BitVec 32)) : + (CombOp.add [a, a]) = CombOp.shlPar a 1 := by + simp [CombOp.add, CombOp.shlPar] + bv_decide - - --- def dcShl := [DCxComb_com| { --- ^entry(%a: !ValueStream_32, %b: !ValueStream_32): --- %unpacka = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) --- -- opposit args order wrt. circt --- %output = "DCxComb.fstVal" (%unpacka) : (!ValueTokenStream_32) -> (!ValueStream_32) --- %token = "DCxComb.sndVal" (%unpacka) : (!ValueTokenStream_32) -> (!TokenStream) --- -- %fork = "DCxComb.fork" (%token) : (!TokenStream) -> (!TokenStream2) keep this implicit --- %2 = "DCxComb.shiftLeft" (%output, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) --- %b2 = "DCxComb.add" (%2, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) --- -- %c2 = "DCxComb.add" (%b2, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) --- %unpackb = "DCxComb.unpack" (%b) : (!ValueStream_32) -> (!ValueTokenStream_32) --- -- opposit args order wrt. circt --- %output1 = "DCxComb.fstVal" (%unpackb) : (!ValueTokenStream_32) -> (!ValueStream_32) --- %token0 = "DCxComb.sndVal" (%unpackb) : (!ValueTokenStream_32) -> (!TokenStream) --- %3 = "DCxComb.join" (%token, %token0) : (!TokenStream, !TokenStream) -> (!TokenStream) --- %4 = "DCxComb.add" (%b2, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) --- %5 = "DCxComb.pack" (%4, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) --- "return" (%5) : (!ValueStream_32) -> () --- }] +theorem equiv_add_dcxcomb (a : DCOp.ValueStream (BitVec 32)) : + ((DCxCombFunctor.Op.comb add).denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) + ((DCxCombFunctor.Op.comb shlPar 2).denote (Ctxt.Valuation.ofHVector (.cons a <| .nil))) := by sorry -- theorem dc_eq (a b: DCOp.ValueStream (BitVec 32)) : -- (dcAdd4.denote (Valuation.ofHVector (.cons a <| .cons b <| .nil))) = DCxComb.shiftLeft a >> 2 := by sorry From fb503e4ab689987ad347be14102912136e5d0fe5 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 21 Aug 2025 11:47:02 +0100 Subject: [PATCH 05/11] chore: progress for the meeting --- SSA/Projects/CIRCT/Handshake-to-DC/Add.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean index a9e452c86a..31c1c76166 100644 --- a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean +++ b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean @@ -296,9 +296,9 @@ theorem equiv_add (a : (BitVec 32)) : simp [CombOp.add, CombOp.shlPar] bv_decide -theorem equiv_add_dcxcomb (a : DCOp.ValueStream (BitVec 32)) : - ((DCxCombFunctor.Op.comb add).denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) - ((DCxCombFunctor.Op.comb shlPar 2).denote (Ctxt.Valuation.ofHVector (.cons a <| .nil))) := by sorry +-- theorem equiv_add_dcxcomb (a : DCOp.ValueStream (BitVec 32)) : +-- ((DCxCombFunctor.Op.comb add).denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) +-- ((DCxCombFunctor.Op.comb shlPar 2).denote (Ctxt.Valuation.ofHVector (.cons a <| .nil))) := by sorry -- theorem dc_eq (a b: DCOp.ValueStream (BitVec 32)) : -- (dcAdd4.denote (Valuation.ofHVector (.cons a <| .cons b <| .nil))) = DCxComb.shiftLeft a >> 2 := by sorry From 186d18dc6242e25e19576a6a45f8452fec5c1ecd Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 21 Aug 2025 17:08:11 +0100 Subject: [PATCH 06/11] chore: more dc things --- SSA/Projects/CIRCT/Stream/SyncMap.lean | 136 +++++++++++++++++++++++++ 1 file changed, 136 insertions(+) create mode 100644 SSA/Projects/CIRCT/Stream/SyncMap.lean diff --git a/SSA/Projects/CIRCT/Stream/SyncMap.lean b/SSA/Projects/CIRCT/Stream/SyncMap.lean new file mode 100644 index 0000000000..19cb58464d --- /dev/null +++ b/SSA/Projects/CIRCT/Stream/SyncMap.lean @@ -0,0 +1,136 @@ +import SSA.Projects.CIRCT.Stream.Stream +import SSA.Projects.CIRCT.Stream.WeakBisim + +namespace CIRCTStream + +#check Nat +-- def syncPrim (ls : List (Stream α)) : Stream (List α) := +def syncPrim1 (s : Stream α) : Stream α := s + +#check Stream.corec +-- the code below goes in the direction of having bv_automata deciding properties +-- about both synced streams (e.g. the ones in comb) and non-synced ones. +-- this makes it hard to express what's the actual benefit of using DC. + +-- σ is the state spaces +def syncMapAccum₂ (init : σ) (f : α → β → σ → γ × σ) (xs : Stream α) (ys : Stream β) : Stream γ := + Stream.corec (⟨xs, ys, init⟩ : _ × _ × _) fun ⟨xs, ys, s⟩ => + match xs 0, ys 0 with + | some x, some y => + let ⟨z, s'⟩ := f x y s + ⟨some z, xs.tail, ys.tail, s'⟩ + | _, _ => + let xs := if (xs 0).isNone then xs.tail else xs + let ys := if (ys 0).isNone then ys.tail else ys + ⟨none, xs, ys, s⟩ + +/-- recover the stateless function by setting σ to unit -/ +def syncMap₂ (f : α → β → γ) (xs : Stream α) (ys : Stream β) : Stream γ := + Stream.corec (xs, ys) fun ⟨xs, ys ⟩ => + match xs 0, ys 0 with + | some x, some y => ⟨some <| f x y, xs.tail, ys.tail⟩ + | _, _ => + let xs := if (xs 0).isNone then xs.tail else xs + let ys := if (ys 0).isNone then ys.tail else ys + ⟨none, xs, ys⟩ + +/-- f is bv-decidable and only operates on bitvecs (potentially), it is lifted to work on streams. -/ +def syncMap₃ (f : α → β → γ → δ) (xs : Stream α) (ys : Stream β) (zs : Stream γ): Stream δ := + Stream.corec (xs, ys, zs) fun ⟨xs, ys, zs⟩ => + match xs 0, ys 0, zs 0 with + | some x, some y, some z => ⟨some <| f x y z, xs.tail, ys.tail, zs.tail⟩ + | _, _, _ => + let xs := if (xs 0).isNone then xs.tail else xs + let ys := if (ys 0).isNone then ys.tail else ys + let zs := if (zs 0).isNone then zs.tail else zs + ⟨none, xs, ys, zs⟩ + +section SyncLemmas +open Stream.Bisim + +theorem syncMap₂_eq_syncMap₂ {f : α → β → γ} + (hxs : xs ~ xs') (hys : ys ~ ys') : + syncMap₂ f xs ys ~ syncMap₂ f xs' ys' := by + -- apply corec_eq_corec_of + sorry + + +theorem syncMap2_flip {f : α → β → γ} : + syncMap₂ f xs ys = syncMap₂ (fun y x => f x y) ys xs := by sorry + +theorem syncMap3_flip23 {f : α → β → γ → δ} : + syncMap₃ f xs ys zs = syncMap₃ (fun x z y => f x y z) xs zs ys := by sorry + + +theorem syncMap₃_eq_syncMap₃ + (hxs : xs ~ xs') (hys : ys ~ ys') (hzs : zs ~ zs') : + syncMap₃ f xs ys zs ~ syncMap₃ f xs' ys' zs' := by + -- apply corec_eq_corec_of + sorry + +@[simp] +theorem syncMap2_syncMap2_eq_syncMap3 (f : α → β → γ) (g : γ → ε → φ) + (as : Stream α) (bs : Stream β) (es : Stream ε) : + syncMap₂ g (syncMap₂ f as bs) es = syncMap₃ (fun a b e => g (f a b) e) as bs es := by + -- I believe this is equal, but it might only be bisim (~) + sorry + +-- theorem syncMap₃_eq_syncMap₃_iff {f g : α → β → γ} +-- (h : ∀ a b c, f a b c = g a b c) : +-- syncMap₂ f xs ys = syncMap₂ g xs ys := by +-- sorry + +end SyncLemmas + + +namespace Examples + +def add₂ : Stream (BitVec w) → Stream (BitVec w) → Stream (BitVec w) := + syncMap₂ (· + ·) + +def add₃ : Stream (BitVec w) → Stream (BitVec w) → Stream (BitVec w) → Stream (BitVec w) := + syncMap₃ (· + · + ·) + + +example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs ys) zs = add₃ xs ys zs := by + simp [add₂, add₃] + +/-- this is the shape of the decproc for comb parts -/ +example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys = add₃ xs ys zs := by + simp only [add₂, add₃] + simp only [syncMap2_syncMap2_eq_syncMap3] + rw [syncMap3_flip23] + congr + funext a b c + bv_decide + +/-- for things that are not synced, the above will do the above as a preproc anyways, +creating rather large areas of comb regions connected by other dc things. +to decide things that can't be synced there are multiple decproc we can write: +1. blackbox all synced stuff (values), just check the presence of things (just separates + data from control) +2. more complex decproc: there are multiple comb nodes, I create an automaton for each comb part + and the circuit will be the result of combining these automata. +-/ + + +example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys ~ add₃ xs ys zs := by sorry + +open Stream.Bisim + + + + + + + +example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys ~ add₃ xs ys zs := by + simp [add₂, add₃] + rw [syncMap₃_eq_syncMap₃ xs.removeNone_equiv _ _] + funext i + +--------------------- + + + +end Examples From 47e3c51817ca46d916e68d28d463ad6601367655 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 28 Aug 2025 08:20:33 +0100 Subject: [PATCH 07/11] chore: comments --- SSA/Projects/CIRCT/Stream/SyncMap.lean | 32 ++++++++++++-------------- 1 file changed, 15 insertions(+), 17 deletions(-) diff --git a/SSA/Projects/CIRCT/Stream/SyncMap.lean b/SSA/Projects/CIRCT/Stream/SyncMap.lean index 19cb58464d..dacfb4336a 100644 --- a/SSA/Projects/CIRCT/Stream/SyncMap.lean +++ b/SSA/Projects/CIRCT/Stream/SyncMap.lean @@ -3,14 +3,13 @@ import SSA.Projects.CIRCT.Stream.WeakBisim namespace CIRCTStream -#check Nat --- def syncPrim (ls : List (Stream α)) : Stream (List α) := +/-! + The code below goes in the direction of having `bv_automata` deciding properties + about both synced streams (e.g. the ones in comb) and non-synced ones. +-/ + def syncPrim1 (s : Stream α) : Stream α := s -#check Stream.corec --- the code below goes in the direction of having bv_automata deciding properties --- about both synced streams (e.g. the ones in comb) and non-synced ones. --- this makes it hard to express what's the actual benefit of using DC. -- σ is the state spaces def syncMapAccum₂ (init : σ) (f : α → β → σ → γ × σ) (xs : Stream α) (ys : Stream β) : Stream γ := @@ -45,6 +44,7 @@ def syncMap₃ (f : α → β → γ → δ) (xs : Stream α) (ys : Stream β) ( let zs := if (zs 0).isNone then zs.tail else zs ⟨none, xs, ys, zs⟩ + section SyncLemmas open Stream.Bisim @@ -104,17 +104,18 @@ example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys = add₃ xs ys funext a b c bv_decide -/-- for things that are not synced, the above will do the above as a preproc anyways, -creating rather large areas of comb regions connected by other dc things. -to decide things that can't be synced there are multiple decproc we can write: -1. blackbox all synced stuff (values), just check the presence of things (just separates - data from control) -2. more complex decproc: there are multiple comb nodes, I create an automaton for each comb part - and the circuit will be the result of combining these automata. +/-! + For streams that are not synced, the above will do the above as a preprocessing anyways, + creating rather large areas of comb regions connected by DC operations. + To decide properties that can't be synced there are multiple decproc we can write: + 1. blackbox all synced stuff (values), just check the presence of things (just separates + data from control) + 2. more complex decproc: there are multiple comb nodes, I create an automaton for each comb part + and the circuit will be the result of combining these automata. -/ -example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys ~ add₃ xs ys zs := by sorry +-- example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys ~ add₃ xs ys zs := by sorry open Stream.Bisim @@ -129,8 +130,5 @@ example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys ~ add₃ xs ys rw [syncMap₃_eq_syncMap₃ xs.removeNone_equiv _ _] funext i ---------------------- - - end Examples From 700a0f0166d68b94f58c3f704991fbcdbed120fd Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 4 Sep 2025 07:17:46 +0100 Subject: [PATCH 08/11] chore: semantics of DC with syncmap --- SSA/Projects/CIRCT/DC/DCSync.lean | 424 +++++++++++++++++++++++++ SSA/Projects/CIRCT/Stream/SyncMap.lean | 8 +- 2 files changed, 428 insertions(+), 4 deletions(-) create mode 100644 SSA/Projects/CIRCT/DC/DCSync.lean diff --git a/SSA/Projects/CIRCT/DC/DCSync.lean b/SSA/Projects/CIRCT/DC/DCSync.lean new file mode 100644 index 0000000000..e2f0682f63 --- /dev/null +++ b/SSA/Projects/CIRCT/DC/DCSync.lean @@ -0,0 +1,424 @@ +import SSA.Projects.CIRCT.Stream.Stream +import SSA.Projects.CIRCT.Stream.SyncMap +import SSA.Projects.CIRCT.Stream.WeakBisim +import SSA.Core.Framework +import SSA.Core.Framework.Macro +import SSA.Core.MLIRSyntax.GenericParser +import SSA.Core.MLIRSyntax.EDSL2 +import SSA.Core.Tactic.SimpSet + +namespace CIRCTStream +namespace DCOp + +def ValueStream := Stream + +def TokenStream := Stream Unit + +def VariadicValueStream (w : Nat) := CIRCTStream.Stream (List (BitVec w)) + +def unpack (x : ValueStream (BitVec w)) : ValueStream (BitVec w) × TokenStream := + Stream.corec₂ (β := Stream (BitVec w)) (x) + fun x => Id.run <| do + match x 0 with + | some _ => return (x 0, some (), x.tail) + | none => return (none, none, x.tail) + +def wrapReadyValue (value : α) (_ : Unit) := value +def sendReadySignal (_ : Unit) (tok : Unit) : Unit := tok + +def pack (x : Stream α) (y : Stream Unit) : Stream α := + syncMap₂ (xs := x) (ys := y) (f := wrapReadyValue) + +def branch (x : ValueStream (BitVec 1)): TokenStream × TokenStream := + Stream.corec₂ (β := ValueStream (BitVec 1)) x fun x => + Id.run <| do + match x 0 with + | none => (none, none, (x.tail)) + | some x₀ => + if x₀.msb then + (some (), none, (x.tail)) + else + (none, some (), (x.tail)) + +def fork (x : TokenStream) : TokenStream × TokenStream := + Stream.corec₂ (β := TokenStream) x + fun x => Id.run <| do + (x 0, x 0, x.tail) + +def join (x y : TokenStream) : TokenStream := + syncMap₂ (xs := x) (ys := y) (f := sendReadySignal) + +def sendReadyValue (_ : Unit) (_ : Unit) : BitVec 1 := 1 + +def merge (x y : TokenStream) : ValueStream (BitVec 1) := + syncMap₂ (xs := x) (ys := y) (f := sendReadyValue) + +/-- +An input token is selected based on the value of the incoming select signal, and propagated to the single output. Only the condition value, the selected input, and the output will be transacted. + + +Informally, the semantics are as follows: +- If there is no condition, then wait for a condition. +- If there is a condition, then try to produce output from the selected channel, leaving the other channel untouched. +- If the selected channel has a value, return it. +- If not, pull more from the selected channel, leaving the condition and the unselected channel unchanged. + +-/ +def select (x y : TokenStream) (c : ValueStream (BitVec 1)): TokenStream := + Stream.corec (β := TokenStream × TokenStream × Stream (BitVec 1)) (x, y, c) + fun ⟨x, y, c⟩ => + match (c 0) with + | none => (none, x, y, c.tail) -- wait on 'c'. + | some 1#1 => + match (x 0) with + | none => (none, x.tail, y, c) -- have 'c', wait on 'x'. + | some _ => (some (), x.tail, y, c.tail) -- consume 'c' and 'x'. + | some 0#1 => + match (y 0) with + | none => (none, x, y.tail, c) -- hace 'c', wait on 'y'. + | some _ => (some (), x, y.tail, c.tail) -- consume 'c' and 'y'. + +def sink (x : TokenStream) : TokenStream := + Stream.corec (β := TokenStream) x fun x => (none, x.tail) + +def source : TokenStream := + Stream.corec () fun () => (some (), ()) + +end DCOp + +end CIRCTStream + +namespace MLIR2DC + +section Dialect + + +inductive Ty +| tokenstream : Ty +| tokenstream2 : Ty +| valuestream (w : Nat) : Ty -- A stream of BitVec w +| valuestream2 (w : Nat) : Ty -- A stream of BitVec w +| valuetokenstream (w : Nat) : Ty -- A product of streams of BitVec wvariadicvaluevokenvstream +| variadicvaluetokenstream (w : Nat) : Ty -- variadicvaluevokenvstream +deriving Inhabited, DecidableEq, Repr, Lean.ToExpr + +instance : ToString Ty where + toString t := repr t |>.pretty + +inductive Op +| fst +| snd +| pair (w : Nat) +| fstVal (w : Nat) +| sndVal (w : Nat) +| fstVal' (w : Nat) +| sndVal' (w : Nat) +| tokVal' (w : Nat) +| merge +| branch +| fork +| join +| select +| sink +| source +| pack (w : Nat) +| pack2 (w : Nat) +| unpack (w : Nat) +| unpack2 (w : Nat) +deriving Inhabited, DecidableEq, Repr, Lean.ToExpr + +abbrev DC : Dialect where + Op := Op + Ty := Ty + +def_signature for DC where + | .fst => (Ty.tokenstream2) → (Ty.tokenstream) + | .fstVal t => (Ty.valuetokenstream t) → Ty.valuestream t + | .fstVal' t => (Ty.variadicvaluetokenstream t) → Ty.valuestream t + | .snd => (Ty.tokenstream2) → (Ty.tokenstream) + | .pair w => (Ty.valuestream w, Ty.valuestream w) → Ty.valuestream2 w + | .sndVal t => (Ty.valuetokenstream t) → Ty.tokenstream + | .sndVal' t => (Ty.variadicvaluetokenstream t) → Ty.valuestream t + | .tokVal' t => (Ty.variadicvaluetokenstream t) → Ty.tokenstream + | .merge => (Ty.tokenstream, Ty.tokenstream) → Ty.valuestream 1 + | .branch => (Ty.valuestream 1) → Ty.tokenstream2 + | .fork => (Ty.tokenstream) → Ty.tokenstream2 + | .join => (Ty.tokenstream, Ty.tokenstream) → Ty.tokenstream + | .select => (Ty.tokenstream, Ty.tokenstream, Ty.valuestream 1) → Ty.tokenstream + | .sink => (Ty.tokenstream) → Ty.tokenstream + | .source => () → Ty.tokenstream + | .pack t => (Ty.valuestream t, Ty.tokenstream) → Ty.valuestream t + | .pack2 t => (Ty.variadicvaluetokenstream t) → Ty.valuestream2 t + | .unpack t => (Ty.valuestream t) → Ty.valuetokenstream t + | .unpack2 t => (Ty.valuestream t, Ty.valuestream t) → Ty.variadicvaluetokenstream t + +instance instDCTyDenote : TyDenote Ty where +toType := fun +| Ty.tokenstream => CIRCTStream.DCOp.TokenStream +| Ty.tokenstream2 => CIRCTStream.DCOp.TokenStream × CIRCTStream.DCOp.TokenStream +| Ty.valuestream w => CIRCTStream.DCOp.ValueStream (BitVec w) +| Ty.valuestream2 w => CIRCTStream.DCOp.ValueStream (BitVec w) × CIRCTStream.DCOp.ValueStream (BitVec w) +| Ty.valuetokenstream w => CIRCTStream.DCOp.ValueStream (BitVec w) × CIRCTStream.DCOp.TokenStream +| Ty.variadicvaluetokenstream w => CIRCTStream.DCOp.VariadicValueStream w × CIRCTStream.DCOp.TokenStream + + +def_denote for DC where + | .fst => fun s => [s.fst]ₕ + | .fstVal _ => fun s => [s.fst]ₕ + | .fstVal' _ => fun s => [s.fst.mapOpt (·[0]?)]ₕ + | .snd => fun s => [s.snd]ₕ + | .pair _ => fun s₁ s₂ => [(s₁, s₂)]ₕ + | .sndVal _ => fun s => [s.snd]ₕ + | .sndVal' _ => fun s => [s.fst.mapOpt (·[0]?)]ₕ + | .tokVal' _ => fun s => [s.snd]ₕ + | .merge => fun s₁ s₂ => [CIRCTStream.DCOp.merge s₁ s₂]ₕ + | .branch => fun s => [CIRCTStream.DCOp.branch s]ₕ + | .fork => fun s => [CIRCTStream.DCOp.fork s]ₕ + | .join => fun s₁ s₂ => [CIRCTStream.DCOp.join s₁ s₂]ₕ + | .select => fun s₁ s₂ c => [CIRCTStream.DCOp.select s₁ s₂ c]ₕ + | .sink => fun s => [CIRCTStream.DCOp.sink s]ₕ + | .source => [CIRCTStream.DCOp.source]ₕ + | .pack _ => fun s₁ s₂ => [CIRCTStream.DCOp.pack s₁ s₂]ₕ + | .pack2 _ => fun s₁ => [CIRCTStream.DCOp.pack2 s₁]ₕ + | .unpack _ => fun s => [CIRCTStream.DCOp.unpack s]ₕ + | .unpack2 _ => fun s₁ s₂ => [CIRCTStream.DCOp.unpack2 s₁ s₂]ₕ + +end Dialect + +def mkTy : MLIR.AST.MLIRType φ → MLIR.AST.ExceptM DC DC.Ty + | MLIR.AST.MLIRType.undefined s => do + match s.splitOn "_" with + | ["TokenStream"] => + return .tokenstream + | ["TokenStream2"] => + return .tokenstream2 + | ["ValueStream", w] => + match w.toNat? with + | some w' => return .valuestream w' + | _ => throw .unsupportedType + | ["ValueStream2", w] => + match w.toNat? with + | some w' => return .valuestream2 w' + | _ => throw .unsupportedType + | ["ValueTokenStream", w] => + match w.toNat? with + | some w' => return .valuetokenstream w' + | _ => throw .unsupportedType + | ["VariadicValueTokenStream", w] => + match w.toNat? with + | some w' => return .variadicvaluetokenstream w' + | _ => throw .unsupportedType + | _ => throw .unsupportedType + | _ => throw .unsupportedType + +instance instTransformTy : MLIR.AST.TransformTy DC 0 where + mkTy := mkTy + +section Compat +open LeanMLIR.SingleReturnCompat (Expr) + +def source : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .source) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .nil) + (regArgs := .nil) + +def sink {Γ : Ctxt _} (a : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .sink) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def unpack {r} {Γ : Ctxt _} (a : Γ.Var (.valuestream r)) : Expr (DC) Γ .pure (.valuetokenstream r) := + Expr.mk + (op := .unpack r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def unpack2 {r} {Γ : Ctxt _} (a : Γ.Var (.valuestream r)) (b : Γ.Var (.valuestream r)) : Expr (DC) Γ .pure (.variadicvaluetokenstream r) := + Expr.mk + (op := .unpack2 r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def pack {r} {Γ : Ctxt _} (a : Γ.Var (.valuestream r)) (b : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.valuestream r) := + Expr.mk + (op := .pack r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def pack2 {r} {Γ : Ctxt _} (a : Γ.Var (.variadicvaluetokenstream r)) : Expr (DC) Γ .pure (.valuestream2 r) := + Expr.mk + (op := .pack2 r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def branch {Γ : Ctxt _} (a : Γ.Var (.valuestream 1)) : Expr (DC) Γ .pure (.tokenstream2) := + Expr.mk + (op := .branch) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def fork (a : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.tokenstream2) := + Expr.mk + (op := .fork) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def join {Γ : Ctxt _} (a b : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .join) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def merge {Γ : Ctxt _} (a b : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.valuestream 1) := + Expr.mk + (op := .merge) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def select {Γ : Ctxt _} (a b : Γ.Var (.tokenstream)) (c : Γ.Var (.valuestream 1)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .select) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .cons c <| .nil) + (regArgs := .nil) + +def fst {Γ : Ctxt _} (a : Γ.Var (.tokenstream2)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .fst) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def fstVal {r} {Γ : Ctxt _} (a : Γ.Var (.valuetokenstream r)) : Expr (DC) Γ .pure (.valuestream r) := + Expr.mk + (op := .fstVal r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def sndVal {r} {Γ : Ctxt _} (a : Γ.Var (.valuetokenstream r)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .sndVal r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def pair {r} {Γ : Ctxt _} (a b: Γ.Var (.valuestream r)) : Expr (DC) Γ .pure (.valuestream2 r) := + Expr.mk + (op := .pair r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def snd {Γ : Ctxt _} (a : Γ.Var (.tokenstream2)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .snd) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +end Compat + +def mkExpr (Γ : Ctxt _) (opStx : MLIR.AST.Op 0) : + MLIR.AST.ReaderM (DC) (Σ eff ty, Expr (DC) Γ eff ty) := do + match opStx.name with + | op@"DC.source" => + if opStx.args.length > 0 then + throw <| .generic s!"expected one operand for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" + else + return ⟨_, [.tokenstream], source⟩ + | op@"DC.sink" | op@"DC.unpack" | op@"DC.fork" | op@"DC.branch" | op@"DC.fst" | op@"DC.snd" | op@"DC.fstVal" | op@"DC.sndVal" => + match opStx.args with + | v₁Stx::[] => + let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx + match ty₁, op with + | .tokenstream2, "DC.fst" => return ⟨_, [.tokenstream], fst v₁⟩ + | .tokenstream2, "DC.snd" => return ⟨_, [.tokenstream], snd v₁⟩ + | .valuetokenstream r, "DC.fstVal" => return ⟨_, [.valuestream r], fstVal v₁⟩ + | .valuetokenstream _, "DC.sndVal" => return ⟨_, [.tokenstream], sndVal v₁⟩ + | .tokenstream, "DC.sink" => return ⟨_, [.tokenstream], sink v₁⟩ + | .valuestream r, "DC.unpack" => return ⟨_, [.valuetokenstream r], unpack v₁⟩ + | .tokenstream, "DC.fork" => return ⟨_, [.tokenstream2], fork v₁⟩ + | .valuestream 1, "DC.branch" => return ⟨_, [.tokenstream2], branch v₁⟩ + | _, _ => throw <| .generic s!"type mismatch" + | _ => throw <| .generic s!"expected one operand for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" + | op@"DC.merge" | op@"DC.join" | op@"DC.pack" | op@"DC.pair" => + match opStx.args with + | v₁Stx::v₂Stx::[] => + let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx + let ⟨ty₂, v₂⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₂Stx + match ty₁, ty₂, op with + | .tokenstream, .tokenstream, "DC.merge" => return ⟨_, [.valuestream 1], merge v₁ v₂⟩ + | .tokenstream, .tokenstream, "DC.join" => return ⟨_, [.tokenstream], join v₁ v₂⟩ + | .valuestream r, .tokenstream, "DC.pack" => return ⟨_, [.valuestream r], pack v₁ v₂⟩ + | .valuestream r₁, .valuestream r₂, "DC.pair" => + if h : r₁ = r₂ then + let v₂' : Γ.Var (Ty.valuestream r₁) := Eq.mp (by rw [h]) v₂ + return ⟨_, [.valuestream2 r₁], pair v₁ v₂'⟩ + else throw <| .generic s!"type mismatch, expected same width for pair, got {r₁} and {r₂}" + | _, _, _ => throw <| .generic s!"type mismatch" + | _ => throw <| .generic s!"expected two operands for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" + | op@"DC.select" => + match opStx.args with + | v₁Stx::v₂Stx::v₃Stx::[] => + let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx + let ⟨ty₂, v₂⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₂Stx + let ⟨ty₃, v₃⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₃Stx + match ty₁, ty₂, ty₃, op with + | .tokenstream, .tokenstream, .valuestream 1, "DC.select" => return ⟨_, [.tokenstream], select v₁ v₂ v₃⟩ + | _, _, _, _=> throw <| .generic s!"type mismatch" + | _ => throw <| .generic s!"expected three operands for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" + | _ => throw <| .unsupportedOp s!"unsupported operation {repr opStx}" + +instance : MLIR.AST.TransformExpr (DC) 0 where + mkExpr := mkExpr + +def mkReturn (Γ : Ctxt _) (opStx : MLIR.AST.Op 0) : MLIR.AST.ReaderM (DC) + (Σ eff ty, Com DC Γ eff ty) := + if opStx.name == "return" + then match opStx.args with + | vStx::[] => do + let ⟨ty, v⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ vStx + return ⟨.pure, [ty], Com.ret v⟩ + | _ => throw <| .generic s!"Ill-formed return statement (wrong arity, expected 1, got {opStx.args.length})" + else throw <| .generic s!"Tried to build return out of non-return statement {opStx.name}" + +instance : MLIR.AST.TransformReturn (DC) 0 where + mkReturn := mkReturn + +instance : DialectToExpr DC where + toExprM := .const ``Id [0] + toExprDialect := .const ``DC [] + +open Qq MLIR AST Lean Elab Term Meta in +elab "[DC_com| " reg:mlir_region "]" : term => do SSA.elabIntoCom' reg DC + +end MLIR2DC diff --git a/SSA/Projects/CIRCT/Stream/SyncMap.lean b/SSA/Projects/CIRCT/Stream/SyncMap.lean index dacfb4336a..dc128d6123 100644 --- a/SSA/Projects/CIRCT/Stream/SyncMap.lean +++ b/SSA/Projects/CIRCT/Stream/SyncMap.lean @@ -125,10 +125,10 @@ open Stream.Bisim -example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys ~ add₃ xs ys zs := by - simp [add₂, add₃] - rw [syncMap₃_eq_syncMap₃ xs.removeNone_equiv _ _] - funext i +-- example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys ~ add₃ xs ys zs := by +-- simp [add₂, add₃] +-- rw [syncMap₃_eq_syncMap₃ xs.removeNone_equiv _ _] +-- funext i end Examples From 505bb228dda6fb344898361d51f598d2fe84ce88 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 4 Sep 2025 07:19:01 +0100 Subject: [PATCH 09/11] chore: fix bugs in parser --- SSA/Projects/CIRCT/DC/DCSync.lean | 424 ------------------------- SSA/Projects/CIRCT/Stream/SyncMap.lean | 134 -------- 2 files changed, 558 deletions(-) delete mode 100644 SSA/Projects/CIRCT/DC/DCSync.lean delete mode 100644 SSA/Projects/CIRCT/Stream/SyncMap.lean diff --git a/SSA/Projects/CIRCT/DC/DCSync.lean b/SSA/Projects/CIRCT/DC/DCSync.lean deleted file mode 100644 index e2f0682f63..0000000000 --- a/SSA/Projects/CIRCT/DC/DCSync.lean +++ /dev/null @@ -1,424 +0,0 @@ -import SSA.Projects.CIRCT.Stream.Stream -import SSA.Projects.CIRCT.Stream.SyncMap -import SSA.Projects.CIRCT.Stream.WeakBisim -import SSA.Core.Framework -import SSA.Core.Framework.Macro -import SSA.Core.MLIRSyntax.GenericParser -import SSA.Core.MLIRSyntax.EDSL2 -import SSA.Core.Tactic.SimpSet - -namespace CIRCTStream -namespace DCOp - -def ValueStream := Stream - -def TokenStream := Stream Unit - -def VariadicValueStream (w : Nat) := CIRCTStream.Stream (List (BitVec w)) - -def unpack (x : ValueStream (BitVec w)) : ValueStream (BitVec w) × TokenStream := - Stream.corec₂ (β := Stream (BitVec w)) (x) - fun x => Id.run <| do - match x 0 with - | some _ => return (x 0, some (), x.tail) - | none => return (none, none, x.tail) - -def wrapReadyValue (value : α) (_ : Unit) := value -def sendReadySignal (_ : Unit) (tok : Unit) : Unit := tok - -def pack (x : Stream α) (y : Stream Unit) : Stream α := - syncMap₂ (xs := x) (ys := y) (f := wrapReadyValue) - -def branch (x : ValueStream (BitVec 1)): TokenStream × TokenStream := - Stream.corec₂ (β := ValueStream (BitVec 1)) x fun x => - Id.run <| do - match x 0 with - | none => (none, none, (x.tail)) - | some x₀ => - if x₀.msb then - (some (), none, (x.tail)) - else - (none, some (), (x.tail)) - -def fork (x : TokenStream) : TokenStream × TokenStream := - Stream.corec₂ (β := TokenStream) x - fun x => Id.run <| do - (x 0, x 0, x.tail) - -def join (x y : TokenStream) : TokenStream := - syncMap₂ (xs := x) (ys := y) (f := sendReadySignal) - -def sendReadyValue (_ : Unit) (_ : Unit) : BitVec 1 := 1 - -def merge (x y : TokenStream) : ValueStream (BitVec 1) := - syncMap₂ (xs := x) (ys := y) (f := sendReadyValue) - -/-- -An input token is selected based on the value of the incoming select signal, and propagated to the single output. Only the condition value, the selected input, and the output will be transacted. - - -Informally, the semantics are as follows: -- If there is no condition, then wait for a condition. -- If there is a condition, then try to produce output from the selected channel, leaving the other channel untouched. -- If the selected channel has a value, return it. -- If not, pull more from the selected channel, leaving the condition and the unselected channel unchanged. - --/ -def select (x y : TokenStream) (c : ValueStream (BitVec 1)): TokenStream := - Stream.corec (β := TokenStream × TokenStream × Stream (BitVec 1)) (x, y, c) - fun ⟨x, y, c⟩ => - match (c 0) with - | none => (none, x, y, c.tail) -- wait on 'c'. - | some 1#1 => - match (x 0) with - | none => (none, x.tail, y, c) -- have 'c', wait on 'x'. - | some _ => (some (), x.tail, y, c.tail) -- consume 'c' and 'x'. - | some 0#1 => - match (y 0) with - | none => (none, x, y.tail, c) -- hace 'c', wait on 'y'. - | some _ => (some (), x, y.tail, c.tail) -- consume 'c' and 'y'. - -def sink (x : TokenStream) : TokenStream := - Stream.corec (β := TokenStream) x fun x => (none, x.tail) - -def source : TokenStream := - Stream.corec () fun () => (some (), ()) - -end DCOp - -end CIRCTStream - -namespace MLIR2DC - -section Dialect - - -inductive Ty -| tokenstream : Ty -| tokenstream2 : Ty -| valuestream (w : Nat) : Ty -- A stream of BitVec w -| valuestream2 (w : Nat) : Ty -- A stream of BitVec w -| valuetokenstream (w : Nat) : Ty -- A product of streams of BitVec wvariadicvaluevokenvstream -| variadicvaluetokenstream (w : Nat) : Ty -- variadicvaluevokenvstream -deriving Inhabited, DecidableEq, Repr, Lean.ToExpr - -instance : ToString Ty where - toString t := repr t |>.pretty - -inductive Op -| fst -| snd -| pair (w : Nat) -| fstVal (w : Nat) -| sndVal (w : Nat) -| fstVal' (w : Nat) -| sndVal' (w : Nat) -| tokVal' (w : Nat) -| merge -| branch -| fork -| join -| select -| sink -| source -| pack (w : Nat) -| pack2 (w : Nat) -| unpack (w : Nat) -| unpack2 (w : Nat) -deriving Inhabited, DecidableEq, Repr, Lean.ToExpr - -abbrev DC : Dialect where - Op := Op - Ty := Ty - -def_signature for DC where - | .fst => (Ty.tokenstream2) → (Ty.tokenstream) - | .fstVal t => (Ty.valuetokenstream t) → Ty.valuestream t - | .fstVal' t => (Ty.variadicvaluetokenstream t) → Ty.valuestream t - | .snd => (Ty.tokenstream2) → (Ty.tokenstream) - | .pair w => (Ty.valuestream w, Ty.valuestream w) → Ty.valuestream2 w - | .sndVal t => (Ty.valuetokenstream t) → Ty.tokenstream - | .sndVal' t => (Ty.variadicvaluetokenstream t) → Ty.valuestream t - | .tokVal' t => (Ty.variadicvaluetokenstream t) → Ty.tokenstream - | .merge => (Ty.tokenstream, Ty.tokenstream) → Ty.valuestream 1 - | .branch => (Ty.valuestream 1) → Ty.tokenstream2 - | .fork => (Ty.tokenstream) → Ty.tokenstream2 - | .join => (Ty.tokenstream, Ty.tokenstream) → Ty.tokenstream - | .select => (Ty.tokenstream, Ty.tokenstream, Ty.valuestream 1) → Ty.tokenstream - | .sink => (Ty.tokenstream) → Ty.tokenstream - | .source => () → Ty.tokenstream - | .pack t => (Ty.valuestream t, Ty.tokenstream) → Ty.valuestream t - | .pack2 t => (Ty.variadicvaluetokenstream t) → Ty.valuestream2 t - | .unpack t => (Ty.valuestream t) → Ty.valuetokenstream t - | .unpack2 t => (Ty.valuestream t, Ty.valuestream t) → Ty.variadicvaluetokenstream t - -instance instDCTyDenote : TyDenote Ty where -toType := fun -| Ty.tokenstream => CIRCTStream.DCOp.TokenStream -| Ty.tokenstream2 => CIRCTStream.DCOp.TokenStream × CIRCTStream.DCOp.TokenStream -| Ty.valuestream w => CIRCTStream.DCOp.ValueStream (BitVec w) -| Ty.valuestream2 w => CIRCTStream.DCOp.ValueStream (BitVec w) × CIRCTStream.DCOp.ValueStream (BitVec w) -| Ty.valuetokenstream w => CIRCTStream.DCOp.ValueStream (BitVec w) × CIRCTStream.DCOp.TokenStream -| Ty.variadicvaluetokenstream w => CIRCTStream.DCOp.VariadicValueStream w × CIRCTStream.DCOp.TokenStream - - -def_denote for DC where - | .fst => fun s => [s.fst]ₕ - | .fstVal _ => fun s => [s.fst]ₕ - | .fstVal' _ => fun s => [s.fst.mapOpt (·[0]?)]ₕ - | .snd => fun s => [s.snd]ₕ - | .pair _ => fun s₁ s₂ => [(s₁, s₂)]ₕ - | .sndVal _ => fun s => [s.snd]ₕ - | .sndVal' _ => fun s => [s.fst.mapOpt (·[0]?)]ₕ - | .tokVal' _ => fun s => [s.snd]ₕ - | .merge => fun s₁ s₂ => [CIRCTStream.DCOp.merge s₁ s₂]ₕ - | .branch => fun s => [CIRCTStream.DCOp.branch s]ₕ - | .fork => fun s => [CIRCTStream.DCOp.fork s]ₕ - | .join => fun s₁ s₂ => [CIRCTStream.DCOp.join s₁ s₂]ₕ - | .select => fun s₁ s₂ c => [CIRCTStream.DCOp.select s₁ s₂ c]ₕ - | .sink => fun s => [CIRCTStream.DCOp.sink s]ₕ - | .source => [CIRCTStream.DCOp.source]ₕ - | .pack _ => fun s₁ s₂ => [CIRCTStream.DCOp.pack s₁ s₂]ₕ - | .pack2 _ => fun s₁ => [CIRCTStream.DCOp.pack2 s₁]ₕ - | .unpack _ => fun s => [CIRCTStream.DCOp.unpack s]ₕ - | .unpack2 _ => fun s₁ s₂ => [CIRCTStream.DCOp.unpack2 s₁ s₂]ₕ - -end Dialect - -def mkTy : MLIR.AST.MLIRType φ → MLIR.AST.ExceptM DC DC.Ty - | MLIR.AST.MLIRType.undefined s => do - match s.splitOn "_" with - | ["TokenStream"] => - return .tokenstream - | ["TokenStream2"] => - return .tokenstream2 - | ["ValueStream", w] => - match w.toNat? with - | some w' => return .valuestream w' - | _ => throw .unsupportedType - | ["ValueStream2", w] => - match w.toNat? with - | some w' => return .valuestream2 w' - | _ => throw .unsupportedType - | ["ValueTokenStream", w] => - match w.toNat? with - | some w' => return .valuetokenstream w' - | _ => throw .unsupportedType - | ["VariadicValueTokenStream", w] => - match w.toNat? with - | some w' => return .variadicvaluetokenstream w' - | _ => throw .unsupportedType - | _ => throw .unsupportedType - | _ => throw .unsupportedType - -instance instTransformTy : MLIR.AST.TransformTy DC 0 where - mkTy := mkTy - -section Compat -open LeanMLIR.SingleReturnCompat (Expr) - -def source : Expr (DC) Γ .pure (.tokenstream) := - Expr.mk - (op := .source) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .nil) - (regArgs := .nil) - -def sink {Γ : Ctxt _} (a : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.tokenstream) := - Expr.mk - (op := .sink) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .nil) - (regArgs := .nil) - -def unpack {r} {Γ : Ctxt _} (a : Γ.Var (.valuestream r)) : Expr (DC) Γ .pure (.valuetokenstream r) := - Expr.mk - (op := .unpack r) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .nil) - (regArgs := .nil) - -def unpack2 {r} {Γ : Ctxt _} (a : Γ.Var (.valuestream r)) (b : Γ.Var (.valuestream r)) : Expr (DC) Γ .pure (.variadicvaluetokenstream r) := - Expr.mk - (op := .unpack2 r) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .cons b <| .nil) - (regArgs := .nil) - -def pack {r} {Γ : Ctxt _} (a : Γ.Var (.valuestream r)) (b : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.valuestream r) := - Expr.mk - (op := .pack r) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .cons b <| .nil) - (regArgs := .nil) - -def pack2 {r} {Γ : Ctxt _} (a : Γ.Var (.variadicvaluetokenstream r)) : Expr (DC) Γ .pure (.valuestream2 r) := - Expr.mk - (op := .pack2 r) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .nil) - (regArgs := .nil) - -def branch {Γ : Ctxt _} (a : Γ.Var (.valuestream 1)) : Expr (DC) Γ .pure (.tokenstream2) := - Expr.mk - (op := .branch) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .nil) - (regArgs := .nil) - -def fork (a : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.tokenstream2) := - Expr.mk - (op := .fork) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .nil) - (regArgs := .nil) - -def join {Γ : Ctxt _} (a b : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.tokenstream) := - Expr.mk - (op := .join) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .cons b <| .nil) - (regArgs := .nil) - -def merge {Γ : Ctxt _} (a b : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.valuestream 1) := - Expr.mk - (op := .merge) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .cons b <| .nil) - (regArgs := .nil) - -def select {Γ : Ctxt _} (a b : Γ.Var (.tokenstream)) (c : Γ.Var (.valuestream 1)) : Expr (DC) Γ .pure (.tokenstream) := - Expr.mk - (op := .select) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .cons b <| .cons c <| .nil) - (regArgs := .nil) - -def fst {Γ : Ctxt _} (a : Γ.Var (.tokenstream2)) : Expr (DC) Γ .pure (.tokenstream) := - Expr.mk - (op := .fst) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .nil) - (regArgs := .nil) - -def fstVal {r} {Γ : Ctxt _} (a : Γ.Var (.valuetokenstream r)) : Expr (DC) Γ .pure (.valuestream r) := - Expr.mk - (op := .fstVal r) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .nil) - (regArgs := .nil) - -def sndVal {r} {Γ : Ctxt _} (a : Γ.Var (.valuetokenstream r)) : Expr (DC) Γ .pure (.tokenstream) := - Expr.mk - (op := .sndVal r) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .nil) - (regArgs := .nil) - -def pair {r} {Γ : Ctxt _} (a b: Γ.Var (.valuestream r)) : Expr (DC) Γ .pure (.valuestream2 r) := - Expr.mk - (op := .pair r) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .cons b <| .nil) - (regArgs := .nil) - -def snd {Γ : Ctxt _} (a : Γ.Var (.tokenstream2)) : Expr (DC) Γ .pure (.tokenstream) := - Expr.mk - (op := .snd) - (ty_eq := rfl) - (eff_le := by constructor) - (args := .cons a <| .nil) - (regArgs := .nil) - -end Compat - -def mkExpr (Γ : Ctxt _) (opStx : MLIR.AST.Op 0) : - MLIR.AST.ReaderM (DC) (Σ eff ty, Expr (DC) Γ eff ty) := do - match opStx.name with - | op@"DC.source" => - if opStx.args.length > 0 then - throw <| .generic s!"expected one operand for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" - else - return ⟨_, [.tokenstream], source⟩ - | op@"DC.sink" | op@"DC.unpack" | op@"DC.fork" | op@"DC.branch" | op@"DC.fst" | op@"DC.snd" | op@"DC.fstVal" | op@"DC.sndVal" => - match opStx.args with - | v₁Stx::[] => - let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx - match ty₁, op with - | .tokenstream2, "DC.fst" => return ⟨_, [.tokenstream], fst v₁⟩ - | .tokenstream2, "DC.snd" => return ⟨_, [.tokenstream], snd v₁⟩ - | .valuetokenstream r, "DC.fstVal" => return ⟨_, [.valuestream r], fstVal v₁⟩ - | .valuetokenstream _, "DC.sndVal" => return ⟨_, [.tokenstream], sndVal v₁⟩ - | .tokenstream, "DC.sink" => return ⟨_, [.tokenstream], sink v₁⟩ - | .valuestream r, "DC.unpack" => return ⟨_, [.valuetokenstream r], unpack v₁⟩ - | .tokenstream, "DC.fork" => return ⟨_, [.tokenstream2], fork v₁⟩ - | .valuestream 1, "DC.branch" => return ⟨_, [.tokenstream2], branch v₁⟩ - | _, _ => throw <| .generic s!"type mismatch" - | _ => throw <| .generic s!"expected one operand for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" - | op@"DC.merge" | op@"DC.join" | op@"DC.pack" | op@"DC.pair" => - match opStx.args with - | v₁Stx::v₂Stx::[] => - let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx - let ⟨ty₂, v₂⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₂Stx - match ty₁, ty₂, op with - | .tokenstream, .tokenstream, "DC.merge" => return ⟨_, [.valuestream 1], merge v₁ v₂⟩ - | .tokenstream, .tokenstream, "DC.join" => return ⟨_, [.tokenstream], join v₁ v₂⟩ - | .valuestream r, .tokenstream, "DC.pack" => return ⟨_, [.valuestream r], pack v₁ v₂⟩ - | .valuestream r₁, .valuestream r₂, "DC.pair" => - if h : r₁ = r₂ then - let v₂' : Γ.Var (Ty.valuestream r₁) := Eq.mp (by rw [h]) v₂ - return ⟨_, [.valuestream2 r₁], pair v₁ v₂'⟩ - else throw <| .generic s!"type mismatch, expected same width for pair, got {r₁} and {r₂}" - | _, _, _ => throw <| .generic s!"type mismatch" - | _ => throw <| .generic s!"expected two operands for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" - | op@"DC.select" => - match opStx.args with - | v₁Stx::v₂Stx::v₃Stx::[] => - let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx - let ⟨ty₂, v₂⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₂Stx - let ⟨ty₃, v₃⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₃Stx - match ty₁, ty₂, ty₃, op with - | .tokenstream, .tokenstream, .valuestream 1, "DC.select" => return ⟨_, [.tokenstream], select v₁ v₂ v₃⟩ - | _, _, _, _=> throw <| .generic s!"type mismatch" - | _ => throw <| .generic s!"expected three operands for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" - | _ => throw <| .unsupportedOp s!"unsupported operation {repr opStx}" - -instance : MLIR.AST.TransformExpr (DC) 0 where - mkExpr := mkExpr - -def mkReturn (Γ : Ctxt _) (opStx : MLIR.AST.Op 0) : MLIR.AST.ReaderM (DC) - (Σ eff ty, Com DC Γ eff ty) := - if opStx.name == "return" - then match opStx.args with - | vStx::[] => do - let ⟨ty, v⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ vStx - return ⟨.pure, [ty], Com.ret v⟩ - | _ => throw <| .generic s!"Ill-formed return statement (wrong arity, expected 1, got {opStx.args.length})" - else throw <| .generic s!"Tried to build return out of non-return statement {opStx.name}" - -instance : MLIR.AST.TransformReturn (DC) 0 where - mkReturn := mkReturn - -instance : DialectToExpr DC where - toExprM := .const ``Id [0] - toExprDialect := .const ``DC [] - -open Qq MLIR AST Lean Elab Term Meta in -elab "[DC_com| " reg:mlir_region "]" : term => do SSA.elabIntoCom' reg DC - -end MLIR2DC diff --git a/SSA/Projects/CIRCT/Stream/SyncMap.lean b/SSA/Projects/CIRCT/Stream/SyncMap.lean deleted file mode 100644 index dc128d6123..0000000000 --- a/SSA/Projects/CIRCT/Stream/SyncMap.lean +++ /dev/null @@ -1,134 +0,0 @@ -import SSA.Projects.CIRCT.Stream.Stream -import SSA.Projects.CIRCT.Stream.WeakBisim - -namespace CIRCTStream - -/-! - The code below goes in the direction of having `bv_automata` deciding properties - about both synced streams (e.g. the ones in comb) and non-synced ones. --/ - -def syncPrim1 (s : Stream α) : Stream α := s - - --- σ is the state spaces -def syncMapAccum₂ (init : σ) (f : α → β → σ → γ × σ) (xs : Stream α) (ys : Stream β) : Stream γ := - Stream.corec (⟨xs, ys, init⟩ : _ × _ × _) fun ⟨xs, ys, s⟩ => - match xs 0, ys 0 with - | some x, some y => - let ⟨z, s'⟩ := f x y s - ⟨some z, xs.tail, ys.tail, s'⟩ - | _, _ => - let xs := if (xs 0).isNone then xs.tail else xs - let ys := if (ys 0).isNone then ys.tail else ys - ⟨none, xs, ys, s⟩ - -/-- recover the stateless function by setting σ to unit -/ -def syncMap₂ (f : α → β → γ) (xs : Stream α) (ys : Stream β) : Stream γ := - Stream.corec (xs, ys) fun ⟨xs, ys ⟩ => - match xs 0, ys 0 with - | some x, some y => ⟨some <| f x y, xs.tail, ys.tail⟩ - | _, _ => - let xs := if (xs 0).isNone then xs.tail else xs - let ys := if (ys 0).isNone then ys.tail else ys - ⟨none, xs, ys⟩ - -/-- f is bv-decidable and only operates on bitvecs (potentially), it is lifted to work on streams. -/ -def syncMap₃ (f : α → β → γ → δ) (xs : Stream α) (ys : Stream β) (zs : Stream γ): Stream δ := - Stream.corec (xs, ys, zs) fun ⟨xs, ys, zs⟩ => - match xs 0, ys 0, zs 0 with - | some x, some y, some z => ⟨some <| f x y z, xs.tail, ys.tail, zs.tail⟩ - | _, _, _ => - let xs := if (xs 0).isNone then xs.tail else xs - let ys := if (ys 0).isNone then ys.tail else ys - let zs := if (zs 0).isNone then zs.tail else zs - ⟨none, xs, ys, zs⟩ - - -section SyncLemmas -open Stream.Bisim - -theorem syncMap₂_eq_syncMap₂ {f : α → β → γ} - (hxs : xs ~ xs') (hys : ys ~ ys') : - syncMap₂ f xs ys ~ syncMap₂ f xs' ys' := by - -- apply corec_eq_corec_of - sorry - - -theorem syncMap2_flip {f : α → β → γ} : - syncMap₂ f xs ys = syncMap₂ (fun y x => f x y) ys xs := by sorry - -theorem syncMap3_flip23 {f : α → β → γ → δ} : - syncMap₃ f xs ys zs = syncMap₃ (fun x z y => f x y z) xs zs ys := by sorry - - -theorem syncMap₃_eq_syncMap₃ - (hxs : xs ~ xs') (hys : ys ~ ys') (hzs : zs ~ zs') : - syncMap₃ f xs ys zs ~ syncMap₃ f xs' ys' zs' := by - -- apply corec_eq_corec_of - sorry - -@[simp] -theorem syncMap2_syncMap2_eq_syncMap3 (f : α → β → γ) (g : γ → ε → φ) - (as : Stream α) (bs : Stream β) (es : Stream ε) : - syncMap₂ g (syncMap₂ f as bs) es = syncMap₃ (fun a b e => g (f a b) e) as bs es := by - -- I believe this is equal, but it might only be bisim (~) - sorry - --- theorem syncMap₃_eq_syncMap₃_iff {f g : α → β → γ} --- (h : ∀ a b c, f a b c = g a b c) : --- syncMap₂ f xs ys = syncMap₂ g xs ys := by --- sorry - -end SyncLemmas - - -namespace Examples - -def add₂ : Stream (BitVec w) → Stream (BitVec w) → Stream (BitVec w) := - syncMap₂ (· + ·) - -def add₃ : Stream (BitVec w) → Stream (BitVec w) → Stream (BitVec w) → Stream (BitVec w) := - syncMap₃ (· + · + ·) - - -example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs ys) zs = add₃ xs ys zs := by - simp [add₂, add₃] - -/-- this is the shape of the decproc for comb parts -/ -example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys = add₃ xs ys zs := by - simp only [add₂, add₃] - simp only [syncMap2_syncMap2_eq_syncMap3] - rw [syncMap3_flip23] - congr - funext a b c - bv_decide - -/-! - For streams that are not synced, the above will do the above as a preprocessing anyways, - creating rather large areas of comb regions connected by DC operations. - To decide properties that can't be synced there are multiple decproc we can write: - 1. blackbox all synced stuff (values), just check the presence of things (just separates - data from control) - 2. more complex decproc: there are multiple comb nodes, I create an automaton for each comb part - and the circuit will be the result of combining these automata. --/ - - --- example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys ~ add₃ xs ys zs := by sorry - -open Stream.Bisim - - - - - - - --- example (xs ys zs : Stream (BitVec 8)) : add₂ (add₂ xs zs) ys ~ add₃ xs ys zs := by --- simp [add₂, add₃] --- rw [syncMap₃_eq_syncMap₃ xs.removeNone_equiv _ _] --- funext i - - -end Examples From a41055f8ae539bfca402eb530157dc7bbc1b6c62 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 4 Sep 2025 07:52:03 +0100 Subject: [PATCH 10/11] chore: auto sem --- SSA/Projects/CIRCT/DC/DC_auto.lean | 460 +++++++++++++++++++++++++++++ 1 file changed, 460 insertions(+) create mode 100644 SSA/Projects/CIRCT/DC/DC_auto.lean diff --git a/SSA/Projects/CIRCT/DC/DC_auto.lean b/SSA/Projects/CIRCT/DC/DC_auto.lean new file mode 100644 index 0000000000..f9f206aecf --- /dev/null +++ b/SSA/Projects/CIRCT/DC/DC_auto.lean @@ -0,0 +1,460 @@ +import SSA.Projects.CIRCT.Stream.Stream +import SSA.Projects.CIRCT.Stream.WeakBisim +import SSA.Core.Framework +import SSA.Core.Framework.Macro +import SSA.Core.MLIRSyntax.GenericParser +import SSA.Core.MLIRSyntax.EDSL2 +import SSA.Core.Tactic.SimpSet +import SSA.Experimental.Bits.Fast.FiniteStateMachine +namespace CIRCTStream +namespace DCOp + +def ValueStream := Stream + +def TokenStream := Stream Unit + +def TokenStreamFSM := FSM (arity := Bool) + +def VariadicValueStream (w : Nat) := CIRCTStream.Stream (List (BitVec w)) + +def unpack (x : ValueStream (BitVec w)) : ValueStream (BitVec w) × TokenStream := + Stream.corec₂ (β := Stream (BitVec w)) (x) + fun x => Id.run <| do + match x 0 with + | some _ => return (x 0, some (), x.tail) + | none => return (none, none, x.tail) + +-- ifeally we spit out a tuple of bitvec, but it's less usable +-- the output of this is synced +def unpack2 (x : ValueStream (BitVec w)) (y : ValueStream (BitVec w)) : VariadicValueStream w × TokenStream := + Stream.corec₂ (β := CIRCTStream.Stream (BitVec w) × CIRCTStream.Stream (BitVec w)) (x, y) + fun (x, y) => Id.run <| do + match x 0, y 0 with + | some x', some y' => return (some [x', y'], some .unit, (x.tail, y.tail)) + | some _, none => return (none, none, (x, y.tail)) + | none, some _ => return (none, none, (x.tail, y)) -- the mid return is the one that returns some if we have a sync + | none, none => return (none, none, (x.tail, y.tail)) + +def pack (x : ValueStream α) (y : TokenStream) : ValueStream α := + Stream.corec (β := ValueStream α × TokenStream) (x, y) fun ⟨x, y⟩ => + match x 0, y 0 with + | some x₀, some _ => (x₀, (x.tail, y.tail)) + | some _, none => (none, (x, y.tail)) -- wait to sync with the token stream + | none, some _ => (none, (x.tail, y)) -- wait to sync with the value stream + | none, none => (none, (x.tail, y.tail)) + +def pack2 (x : VariadicValueStream α × TokenStream) : (ValueStream (BitVec α)) × (ValueStream (BitVec α)) := + Stream.corec₂ (β := VariadicValueStream α × TokenStream) (x) fun ⟨x, y⟩ => + match x 0, y 0 with + | some x', some _ => (x'[0]?, x'[1]?, (x.tail, y.tail)) + | some _, none => (none, none, (x, y.tail)) + | none, some _ => (none, none, (x.tail, y)) -- wait to sync with the value stream + | none, none => (none, none, (x.tail, y.tail)) -- wait to sync with the value stream + +def branch (x : ValueStream (BitVec 1)): TokenStream × TokenStream := + Stream.corec₂ (β := ValueStream (BitVec 1)) x fun x => + Id.run <| do + match x 0 with + | none => (none, none, (x.tail)) + | some x₀ => + if x₀.msb then + (some (), none, (x.tail)) + else + (none, some (), (x.tail)) + + +def fork (x : TokenStream) : TokenStream × TokenStream := + Stream.corec₂ (β := TokenStream) x + fun x => Id.run <| do + (x 0, x 0, x.tail) + + +/-- Previous stream semantics: + def join (x y : TokenStream) : TokenStream := + Stream.corec (β := TokenStream × TokenStream) (x, y) fun ⟨x, y⟩ => + match x 0, y 0 with + | some _, some _ => (some (), (x.tail, y.tail)) + | some _, none => (none, (x, y.tail)) + | none, some _ => (none, (x.tail, y)) + | none, none => (none, (x.tail, y.tail)) + +-/ +def join : TokenStreamFSM := FSM.and + +def merge (x y : TokenStream) : ValueStream (BitVec 1) := + Stream.corec (β := TokenStream × TokenStream) (x, y) fun ⟨x, y⟩ => + match x 0, y 0 with + | some _, some _ => (some 1, (x.tail, y)) + | some _, none => (some 1, (x.tail, y.tail)) + | none, some _ => (some 0, (x.tail, y.tail)) + | none, none => (none, (x.tail, y.tail)) + +/-- +An input token is selected based on the value of the incoming select signal, and propagated to the single output. Only the condition value, the selected input, and the output will be transacted. + + +Informally, the semantics are as follows: +- If there is no condition, then wait for a condition. +- If there is a condition, then try to produce output from the selected channel, leaving the other channel untouched. +- If the selected channel has a value, return it. +- If not, pull more from the selected channel, leaving the condition and the unselected channel unchanged. + +-/ +def select (x y : TokenStream) (c : ValueStream (BitVec 1)): TokenStream := + Stream.corec (β := TokenStream × TokenStream × Stream (BitVec 1)) (x, y, c) + fun ⟨x, y, c⟩ => + match (c 0) with + | none => (none, x, y, c.tail) -- wait on 'c'. + | some 1#1 => + match (x 0) with + | none => (none, x.tail, y, c) -- have 'c', wait on 'x'. + | some _ => (some (), x.tail, y, c.tail) -- consume 'c' and 'x'. + | some 0#1 => + match (y 0) with + | none => (none, x, y.tail, c) -- hace 'c', wait on 'y'. + | some _ => (some (), x, y.tail, c.tail) -- consume 'c' and 'y'. + +def sink (x : TokenStream) : TokenStream := + Stream.corec (β := TokenStream) x fun x => (none, x.tail) + +def source : TokenStream := + Stream.corec () fun () => (some (), ()) + +end DCOp + +end CIRCTStream + +namespace MLIR2DC + +section Dialect + + +inductive Ty +| tokenstream : Ty +| tokenstream2 : Ty +| valuestream (w : Nat) : Ty -- A stream of BitVec w +| valuestream2 (w : Nat) : Ty -- A stream of BitVec w +| valuetokenstream (w : Nat) : Ty -- A product of streams of BitVec wvariadicvaluevokenvstream +| variadicvaluetokenstream (w : Nat) : Ty -- variadicvaluevokenvstream +deriving Inhabited, DecidableEq, Repr, Lean.ToExpr + +instance : ToString Ty where + toString t := repr t |>.pretty + +inductive Op +| fst +| snd +| pair (w : Nat) +| fstVal (w : Nat) +| sndVal (w : Nat) +| fstVal' (w : Nat) +| sndVal' (w : Nat) +| tokVal' (w : Nat) +| merge +| branch +| fork +| join +| select +| sink +| source +| pack (w : Nat) +| pack2 (w : Nat) +| unpack (w : Nat) +| unpack2 (w : Nat) +deriving Inhabited, DecidableEq, Repr, Lean.ToExpr + +abbrev DC : Dialect where + Op := Op + Ty := Ty + +def_signature for DC where + | .fst => (Ty.tokenstream2) → (Ty.tokenstream) + | .fstVal t => (Ty.valuetokenstream t) → Ty.valuestream t + | .fstVal' t => (Ty.variadicvaluetokenstream t) → Ty.valuestream t + | .snd => (Ty.tokenstream2) → (Ty.tokenstream) + | .pair w => (Ty.valuestream w, Ty.valuestream w) → Ty.valuestream2 w + | .sndVal t => (Ty.valuetokenstream t) → Ty.tokenstream + | .sndVal' t => (Ty.variadicvaluetokenstream t) → Ty.valuestream t + | .tokVal' t => (Ty.variadicvaluetokenstream t) → Ty.tokenstream + | .merge => (Ty.tokenstream, Ty.tokenstream) → Ty.valuestream 1 + | .branch => (Ty.valuestream 1) → Ty.tokenstream2 + | .fork => (Ty.tokenstream) → Ty.tokenstream2 + | .join => (Ty.tokenstream, Ty.tokenstream) → Ty.tokenstream + | .select => (Ty.tokenstream, Ty.tokenstream, Ty.valuestream 1) → Ty.tokenstream + | .sink => (Ty.tokenstream) → Ty.tokenstream + | .source => () → Ty.tokenstream + | .pack t => (Ty.valuestream t, Ty.tokenstream) → Ty.valuestream t + | .pack2 t => (Ty.variadicvaluetokenstream t) → Ty.valuestream2 t + | .unpack t => (Ty.valuestream t) → Ty.valuetokenstream t + | .unpack2 t => (Ty.valuestream t, Ty.valuestream t) → Ty.variadicvaluetokenstream t + +instance instDCTyDenote : TyDenote Ty where +toType := fun +| Ty.tokenstream => CIRCTStream.DCOp.TokenStream +| Ty.tokenstream2 => CIRCTStream.DCOp.TokenStream × CIRCTStream.DCOp.TokenStream +| Ty.valuestream w => CIRCTStream.DCOp.ValueStream (BitVec w) +| Ty.valuestream2 w => CIRCTStream.DCOp.ValueStream (BitVec w) × CIRCTStream.DCOp.ValueStream (BitVec w) +| Ty.valuetokenstream w => CIRCTStream.DCOp.ValueStream (BitVec w) × CIRCTStream.DCOp.TokenStream +| Ty.variadicvaluetokenstream w => CIRCTStream.DCOp.VariadicValueStream w × CIRCTStream.DCOp.TokenStream + + +def_denote for DC where + | .fst => fun s => [s.fst]ₕ + | .fstVal _ => fun s => [s.fst]ₕ + | .fstVal' _ => fun s => [s.fst.mapOpt (·[0]?)]ₕ + | .snd => fun s => [s.snd]ₕ + | .pair _ => fun s₁ s₂ => [(s₁, s₂)]ₕ + | .sndVal _ => fun s => [s.snd]ₕ + | .sndVal' _ => fun s => [s.fst.mapOpt (·[0]?)]ₕ + | .tokVal' _ => fun s => [s.snd]ₕ + | .merge => fun s₁ s₂ => [CIRCTStream.DCOp.merge s₁ s₂]ₕ + | .branch => fun s => [CIRCTStream.DCOp.branch s]ₕ + | .fork => fun s => [CIRCTStream.DCOp.fork s]ₕ + | .join => fun s₁ s₂ => [CIRCTStream.DCOp.join s₁ s₂]ₕ + | .select => fun s₁ s₂ c => [CIRCTStream.DCOp.select s₁ s₂ c]ₕ + | .sink => fun s => [CIRCTStream.DCOp.sink s]ₕ + | .source => [CIRCTStream.DCOp.source]ₕ + | .pack _ => fun s₁ s₂ => [CIRCTStream.DCOp.pack s₁ s₂]ₕ + | .pack2 _ => fun s₁ => [CIRCTStream.DCOp.pack2 s₁]ₕ + | .unpack _ => fun s => [CIRCTStream.DCOp.unpack s]ₕ + | .unpack2 _ => fun s₁ s₂ => [CIRCTStream.DCOp.unpack2 s₁ s₂]ₕ + +end Dialect + +def mkTy : MLIR.AST.MLIRType φ → MLIR.AST.ExceptM DC DC.Ty + | MLIR.AST.MLIRType.undefined s => do + match s.splitOn "_" with + | ["TokenStream"] => + return .tokenstream + | ["TokenStream2"] => + return .tokenstream2 + | ["ValueStream", w] => + match w.toNat? with + | some w' => return .valuestream w' + | _ => throw .unsupportedType + | ["ValueStream2", w] => + match w.toNat? with + | some w' => return .valuestream2 w' + | _ => throw .unsupportedType + | ["ValueTokenStream", w] => + match w.toNat? with + | some w' => return .valuetokenstream w' + | _ => throw .unsupportedType + | ["VariadicValueTokenStream", w] => + match w.toNat? with + | some w' => return .variadicvaluetokenstream w' + | _ => throw .unsupportedType + | _ => throw .unsupportedType + | _ => throw .unsupportedType + +instance instTransformTy : MLIR.AST.TransformTy DC 0 where + mkTy := mkTy + +section Compat +open LeanMLIR.SingleReturnCompat (Expr) + +def source : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .source) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .nil) + (regArgs := .nil) + +def sink {Γ : Ctxt _} (a : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .sink) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def unpack {r} {Γ : Ctxt _} (a : Γ.Var (.valuestream r)) : Expr (DC) Γ .pure (.valuetokenstream r) := + Expr.mk + (op := .unpack r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def unpack2 {r} {Γ : Ctxt _} (a : Γ.Var (.valuestream r)) (b : Γ.Var (.valuestream r)) : Expr (DC) Γ .pure (.variadicvaluetokenstream r) := + Expr.mk + (op := .unpack2 r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def pack {r} {Γ : Ctxt _} (a : Γ.Var (.valuestream r)) (b : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.valuestream r) := + Expr.mk + (op := .pack r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def pack2 {r} {Γ : Ctxt _} (a : Γ.Var (.variadicvaluetokenstream r)) : Expr (DC) Γ .pure (.valuestream2 r) := + Expr.mk + (op := .pack2 r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def branch {Γ : Ctxt _} (a : Γ.Var (.valuestream 1)) : Expr (DC) Γ .pure (.tokenstream2) := + Expr.mk + (op := .branch) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def fork (a : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.tokenstream2) := + Expr.mk + (op := .fork) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def join {Γ : Ctxt _} (a b : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .join) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def merge {Γ : Ctxt _} (a b : Γ.Var (.tokenstream)) : Expr (DC) Γ .pure (.valuestream 1) := + Expr.mk + (op := .merge) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def select {Γ : Ctxt _} (a b : Γ.Var (.tokenstream)) (c : Γ.Var (.valuestream 1)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .select) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .cons c <| .nil) + (regArgs := .nil) + +def fst {Γ : Ctxt _} (a : Γ.Var (.tokenstream2)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .fst) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def fstVal {r} {Γ : Ctxt _} (a : Γ.Var (.valuetokenstream r)) : Expr (DC) Γ .pure (.valuestream r) := + Expr.mk + (op := .fstVal r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def sndVal {r} {Γ : Ctxt _} (a : Γ.Var (.valuetokenstream r)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .sndVal r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +def pair {r} {Γ : Ctxt _} (a b: Γ.Var (.valuestream r)) : Expr (DC) Γ .pure (.valuestream2 r) := + Expr.mk + (op := .pair r) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .cons b <| .nil) + (regArgs := .nil) + +def snd {Γ : Ctxt _} (a : Γ.Var (.tokenstream2)) : Expr (DC) Γ .pure (.tokenstream) := + Expr.mk + (op := .snd) + (ty_eq := rfl) + (eff_le := by constructor) + (args := .cons a <| .nil) + (regArgs := .nil) + +end Compat + +def mkExpr (Γ : Ctxt _) (opStx : MLIR.AST.Op 0) : + MLIR.AST.ReaderM (DC) (Σ eff ty, Expr (DC) Γ eff ty) := do + match opStx.name with + | op@"DC.source" => + if opStx.args.length > 0 then + throw <| .generic s!"expected one operand for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" + else + return ⟨_, [.tokenstream], source⟩ + | op@"DC.sink" | op@"DC.unpack" | op@"DC.fork" | op@"DC.branch" | op@"DC.fst" | op@"DC.snd" | op@"DC.fstVal" | op@"DC.sndVal" => + match opStx.args with + | v₁Stx::[] => + let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx + match ty₁, op with + | .tokenstream2, "DC.fst" => return ⟨_, [.tokenstream], fst v₁⟩ + | .tokenstream2, "DC.snd" => return ⟨_, [.tokenstream], snd v₁⟩ + | .valuetokenstream r, "DC.fstVal" => return ⟨_, [.valuestream r], fstVal v₁⟩ + | .valuetokenstream _, "DC.sndVal" => return ⟨_, [.tokenstream], sndVal v₁⟩ + | .tokenstream, "DC.sink" => return ⟨_, [.tokenstream], sink v₁⟩ + | .valuestream r, "DC.unpack" => return ⟨_, [.valuetokenstream r], unpack v₁⟩ + | .tokenstream, "DC.fork" => return ⟨_, [.tokenstream2], fork v₁⟩ + | .valuestream 1, "DC.branch" => return ⟨_, [.tokenstream2], branch v₁⟩ + | _, _ => throw <| .generic s!"type mismatch" + | _ => throw <| .generic s!"expected one operand for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" + | op@"DC.merge" | op@"DC.join" | op@"DC.pack" | op@"DC.pair" => + match opStx.args with + | v₁Stx::v₂Stx::[] => + let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx + let ⟨ty₂, v₂⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₂Stx + match ty₁, ty₂, op with + | .tokenstream, .tokenstream, "DC.merge" => return ⟨_, [.valuestream 1], merge v₁ v₂⟩ + | .tokenstream, .tokenstream, "DC.join" => return ⟨_, [.tokenstream], join v₁ v₂⟩ + | .valuestream r, .tokenstream, "DC.pack" => return ⟨_, [.valuestream r], pack v₁ v₂⟩ + | .valuestream r₁, .valuestream r₂, "DC.pair" => + if h : r₁ = r₂ then + let v₂' : Γ.Var (Ty.valuestream r₁) := Eq.mp (by rw [h]) v₂ + return ⟨_, [.valuestream2 r₁], pair v₁ v₂'⟩ + else throw <| .generic s!"type mismatch, expected same width for pair, got {r₁} and {r₂}" + | _, _, _ => throw <| .generic s!"type mismatch" + | _ => throw <| .generic s!"expected two operands for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" + | op@"DC.select" => + match opStx.args with + | v₁Stx::v₂Stx::v₃Stx::[] => + let ⟨ty₁, v₁⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₁Stx + let ⟨ty₂, v₂⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₂Stx + let ⟨ty₃, v₃⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ v₃Stx + match ty₁, ty₂, ty₃, op with + | .tokenstream, .tokenstream, .valuestream 1, "DC.select" => return ⟨_, [.tokenstream], select v₁ v₂ v₃⟩ + | _, _, _, _=> throw <| .generic s!"type mismatch" + | _ => throw <| .generic s!"expected three operands for `monomial`, found #'{opStx.args.length}' in '{repr opStx.args}'" + | _ => throw <| .unsupportedOp s!"unsupported operation {repr opStx}" + +instance : MLIR.AST.TransformExpr (DC) 0 where + mkExpr := mkExpr + +def mkReturn (Γ : Ctxt _) (opStx : MLIR.AST.Op 0) : MLIR.AST.ReaderM (DC) + (Σ eff ty, Com DC Γ eff ty) := + if opStx.name == "return" + then match opStx.args with + | vStx::[] => do + let ⟨ty, v⟩ ← MLIR.AST.TypedSSAVal.mkVal Γ vStx + return ⟨.pure, [ty], Com.ret v⟩ + | _ => throw <| .generic s!"Ill-formed return statement (wrong arity, expected 1, got {opStx.args.length})" + else throw <| .generic s!"Tried to build return out of non-return statement {opStx.name}" + +instance : MLIR.AST.TransformReturn (DC) 0 where + mkReturn := mkReturn + +instance : DialectToExpr DC where + toExprM := .const ``Id [0] + toExprDialect := .const ``DC [] + +open Qq MLIR AST Lean Elab Term Meta in +elab "[DC_com| " reg:mlir_region "]" : term => do SSA.elabIntoCom' reg DC + +end MLIR2DC From 98059a8d2479e21bbf9c7d0fbf731943366e3466 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 4 Sep 2025 08:00:06 +0100 Subject: [PATCH 11/11] chore: reset add --- SSA/Projects/CIRCT/Handshake-to-DC/Add.lean | 49 --------------------- 1 file changed, 49 deletions(-) diff --git a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean index 31c1c76166..cf2ca3e2a9 100644 --- a/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean +++ b/SSA/Projects/CIRCT/Handshake-to-DC/Add.lean @@ -247,55 +247,6 @@ theorem equiv_add (a : (BitVec 32)) : simp [CombOp.add, CombOp.shlPar] bv_decide --- theorem equiv_add_dcxcomb (a : DCOp.ValueStream (BitVec 32)) : --- ((DCxCombFunctor.Op.comb add).denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) --- ((DCxCombFunctor.Op.comb shlPar 2).denote (Ctxt.Valuation.ofHVector (.cons a <| .nil))) := by sorry -#check dcAdd' -#eval dcAdd' -#reduce dcAdd' -#check dcAdd'.denote -#print axioms dcAdd' --- delay-insensitive, hence easier to prove/reason about. - - -def dcShl := [DCxComb_com| { - ^entry(%a: !ValueStream_32, %b: !ValueStream_32): - %unpacka = "DCxComb.unpack" (%a) : (!ValueStream_32) -> (!ValueTokenStream_32) - -- opposit args order wrt. circt - %output = "DCxComb.fstVal" (%unpacka) : (!ValueTokenStream_32) -> (!ValueStream_32) - %token = "DCxComb.sndVal" (%unpacka) : (!ValueTokenStream_32) -> (!TokenStream) - -- %fork = "DCxComb.fork" (%token) : (!TokenStream) -> (!TokenStream2) keep this implicit - %2 = "DCxComb.shlPar_1" (%output) : (!ValueStream_32) -> (!ValueStream_32) - %unpackb = "DCxComb.unpack" (%b) : (!ValueStream_32) -> (!ValueTokenStream_32) - -- opposit args order wrt. circt - %output1 = "DCxComb.fstVal" (%unpackb) : (!ValueTokenStream_32) -> (!ValueStream_32) - %token0 = "DCxComb.sndVal" (%unpackb) : (!ValueTokenStream_32) -> (!TokenStream) - %3 = "DCxComb.join" (%token, %token0) : (!TokenStream, !TokenStream) -> (!TokenStream) - %4 = "DCxComb.add" (%2, %output) : (!ValueStream_32, !ValueStream_32) -> (!ValueStream_32) - %5 = "DCxComb.pack" (%4, %3) : (!ValueStream_32, !TokenStream) -> (!ValueStream_32) - "return" (%5) : (!ValueStream_32) -> () -}] - -def testDCAdd2 : DCOp.ValueStream (BitVec 32) := - dcAdd2.denote (Ctxt.Valuation.ofHVector (.cons a <| .cons b <| .nil)) - -def testDCShl2 : DCOp.ValueStream (BitVec 32) := - dcShl.denote (Ctxt.Valuation.ofHVector (.cons a <| .cons b <| .nil)) - -#eval testDCAdd2 -#eval testDCShl2 - -theorem equiv_add_shl (a : DCOp.ValueStream (BitVec 32)) : - (dcAdd2.denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) = (dcShl.denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) := by - simp [dcAdd2, dcShl] - - sorry - -theorem equiv_add (a : (BitVec 32)) : - (CombOp.add [a, a]) = CombOp.shlPar a 1 := by - simp [CombOp.add, CombOp.shlPar] - bv_decide - -- theorem equiv_add_dcxcomb (a : DCOp.ValueStream (BitVec 32)) : -- ((DCxCombFunctor.Op.comb add).denote (Ctxt.Valuation.ofHVector (.cons a <| .cons a <| .nil))) -- ((DCxCombFunctor.Op.comb shlPar 2).denote (Ctxt.Valuation.ofHVector (.cons a <| .nil))) := by sorry