From d84f54d71a10b1b200c0f0174918c4b846aea4df Mon Sep 17 00:00:00 2001
From: luisacicolini <luisacicolini@gmail.com>
Date: Tue, 9 Dec 2025 10:31:28 +0000
Subject: [PATCH 1/9] chore: proof statement

---
 SSA/Projects/CIRCT/Register/Basic.lean | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/SSA/Projects/CIRCT/Register/Basic.lean b/SSA/Projects/CIRCT/Register/Basic.lean
index 2466dcf913..b486879bde 100644
--- a/SSA/Projects/CIRCT/Register/Basic.lean
+++ b/SSA/Projects/CIRCT/Register/Basic.lean
@@ -1,9 +1,20 @@
 import SSA.Projects.CIRCT.Stream.Basic
 import SSA.Projects.CIRCT.Stream.Lemmas
 
+<<<<<<< HEAD:SSA/Projects/CIRCT/Register/Basic.lean
 /-! We model a register storing a value for one cycle -/
 
 namespace HandshakeStream
+=======
+namespace CIRCTStream
+
+/-!
+Trace monoidal categories:
+we model a feedback loop as a function with a-many inputs and x-many inputs, producing b-many outputs
+and x-many outputs that are re-fed as inputs to the function (inputs, inputs from feedback, outputs,
+outputs to be fed-back)
+-/
+>>>>>>> 6701d2b8a (chore: proof statement):SSA/Projects/CIRCT/Handshake-to-HW/fork.lean
 
 /--
   The sequential logics defining the behaviour of a register, assuming it operates on a stream
@@ -103,6 +114,10 @@ def iso_unary (a : Stream' (BitVec 1)) : Stream' (Vector (BitVec 1) 1) :=
     fun n =>
       {toArray := [a n].toArray, size_toArray := by simp}
 
+/-- Convert a `Stream'` to `Stream` -/
+def iso_unary' (a : Stream' (BitVec 1)) : Stream (BitVec 1) :=
+    fun i => a.get i
+
 /--
   We define an isomorphism from two streams `a`, `b` to a stream of their product BitVec 1 × BitVec 1.
   With this isomorphism we map the single streams that define the inputs of the hardware module to

From 8c0ac4356adeaa028269d4114d8c7d78209d8576 Mon Sep 17 00:00:00 2001
From: luisacicolini <luisacicolini@gmail.com>
Date: Tue, 9 Dec 2025 14:01:23 +0000
Subject: [PATCH 2/9] chore: proof of fork statement

---
 SSA/Projects/CIRCT/Register/Basic.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/SSA/Projects/CIRCT/Register/Basic.lean b/SSA/Projects/CIRCT/Register/Basic.lean
index b486879bde..7577d38426 100644
--- a/SSA/Projects/CIRCT/Register/Basic.lean
+++ b/SSA/Projects/CIRCT/Register/Basic.lean
@@ -128,16 +128,16 @@ def iso_binary (a b : Stream' (BitVec 1)) : Stream' (Vector (BitVec 1) 2) :=
       {toArray := [a n, b n].toArray, size_toArray := by simp}
 
 /--
-  Map the `i`-th element of stream `s` in `xv` to the output vector.
+  Map the `i`-th element of stream `s` in `xv` to the output vector, using `Stream'`.
 -/
-def streams_to_vec {α : Type u} {n : Nat} (xv : Vector (Stream' α) n) : Stream' (Vector α n) :=
+def streams_to_vec' {α : Type u} {n : Nat} (xv : Vector (Stream' α) n) : Stream' (Vector α n) :=
   /- `map` applies `fun (s : Stream' α) => s i` to every element in `xv` -/
   fun (i : Nat) => xv.map (fun (s : Stream' α) => s i)
 
 /--
-  Map each element at the `k`-th position of `xv` to the `k`-th stream of the output.
+  Map each element at the `k`-th position of `xv` to the `k`-th stream of the output, using `Stream'`.
 -/
-def vec_to_streams {α : Type u} {n : Nat} (xv : Stream' (Vector α n)) : Vector (Stream' α) n :=
+def vec_to_streams' {α : Type u} {n : Nat} (xv : Stream' (Vector α n)) : Vector (Stream' α) n :=
   /- `.ofFn` creates a vector with `n` elements (for each `k` from `0` to `n - 1`),
       where each element is a stream `fun (i : Nat) => ...` containing the `k`-th element of the
       `i`-th element of stream `xv`.

From e3d217d2f5d2fac000388b612fbff1083bd2a8ae Mon Sep 17 00:00:00 2001
From: luisacicolini <luisacicolini@gmail.com>
Date: Thu, 11 Dec 2025 07:52:01 +0000
Subject: [PATCH 3/9] chore: fix fork and add to ci

---
 SSA/Projects/CIRCT/Register/Basic.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/SSA/Projects/CIRCT/Register/Basic.lean b/SSA/Projects/CIRCT/Register/Basic.lean
index 7577d38426..3be5a782ad 100644
--- a/SSA/Projects/CIRCT/Register/Basic.lean
+++ b/SSA/Projects/CIRCT/Register/Basic.lean
@@ -1,12 +1,17 @@
 import SSA.Projects.CIRCT.Stream.Basic
 import SSA.Projects.CIRCT.Stream.Lemmas
+import SSA.Projects.CIRCT.Handshake.Handshake
 
+<<<<<<< HEAD:SSA/Projects/CIRCT/Register/Basic.lean
 <<<<<<< HEAD:SSA/Projects/CIRCT/Register/Basic.lean
 /-! We model a register storing a value for one cycle -/
 
 namespace HandshakeStream
 =======
 namespace CIRCTStream
+=======
+open HandshakeStream
+>>>>>>> 3410b43d9 (chore: fix fork and add to ci):SSA/Projects/CIRCT/Handshake-to-HW/fork.lean
 
 /-!
 Trace monoidal categories:

From 9578a207cd09a59c4193f0dd2704d34931678a3c Mon Sep 17 00:00:00 2001
From: luisacicolini <luisacicolini@gmail.com>
Date: Thu, 11 Dec 2025 07:56:38 +0000
Subject: [PATCH 4/9] chore: fix fork and add to ci

---
 SSA/Projects/CIRCT/CIRCT.lean         | 1 +
 SSA/Projects/CIRCT/Stream/Lemmas.lean | 5 -----
 2 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/SSA/Projects/CIRCT/CIRCT.lean b/SSA/Projects/CIRCT/CIRCT.lean
index cc3ed1e700..f86d5aab15 100644
--- a/SSA/Projects/CIRCT/CIRCT.lean
+++ b/SSA/Projects/CIRCT/CIRCT.lean
@@ -2,6 +2,7 @@ import SSA.Projects.CIRCT.Handshake.Handshake
 import SSA.Projects.CIRCT.HSxComb.HSxCombFunctor
 import SSA.Projects.CIRCT.DC.DC
 import SSA.Projects.CIRCT.DCxComb.DCxCombFunctor
+import SSA.Projects.CIRCT.Handshake-to-HW.fork
 import SSA.Projects.CIRCT.DCPlus.DCPlus
 import SSA.Projects.CIRCT.Comb.Comb
 import SSA.Projects.CIRCT.Register.Basic
diff --git a/SSA/Projects/CIRCT/Stream/Lemmas.lean b/SSA/Projects/CIRCT/Stream/Lemmas.lean
index 8e50944471..fbcb18c048 100644
--- a/SSA/Projects/CIRCT/Stream/Lemmas.lean
+++ b/SSA/Projects/CIRCT/Stream/Lemmas.lean
@@ -332,8 +332,3 @@ theorem syncMap2_syncMap2_eq_syncMap3 (f : α → β → γ) (g : γ → ε →
     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

From d45ad832e4a0bcdba80e9bdab6c92359330311f1 Mon Sep 17 00:00:00 2001
From: luisacicolini <luisacicolini@gmail.com>
Date: Thu, 11 Dec 2025 09:26:16 +0000
Subject: [PATCH 5/9] chore: correct

---
 SSA/Projects/CIRCT/HandshakeToHW/fork.lean | 22 +++++++++++++--
 SSA/Projects/CIRCT/Register/Basic.lean     | 32 ++++++++++++----------
 2 files changed, 36 insertions(+), 18 deletions(-)

diff --git a/SSA/Projects/CIRCT/HandshakeToHW/fork.lean b/SSA/Projects/CIRCT/HandshakeToHW/fork.lean
index 78e6d83b67..5e5a327483 100644
--- a/SSA/Projects/CIRCT/HandshakeToHW/fork.lean
+++ b/SSA/Projects/CIRCT/HandshakeToHW/fork.lean
@@ -47,7 +47,7 @@ namespace HandshakeStream
   }
 
 -/
-def module
+def fork
       (arg_0 : Stream' (BitVec 1))
       (arg_0_valid : Stream' (BitVec 1))
       (arg_1 : Stream' (BitVec 1))
@@ -56,9 +56,9 @@ def module
       (out1_ready : Stream' (BitVec 1))
       (out2_ready : Stream' (BitVec 1))
   : Vector (Stream' (BitVec 1)) 8 :=
-    let vec_streams := HandshakeStream.streams_to_vec
+    let vec_streams := streams_to_vec'
                         (#v[arg_0, arg_0_valid, arg_1, arg_1_valid, out0_ready, out1_ready, out2_ready])
-    vec_to_streams <| register_wrapper
+    vec_to_streams' <| register_wrapper
       (inputs := vec_streams)
       (init_regs := #v[0#1, 0#1])
       (update_fun := -- (Vector (BitVec 1) 7 × Vector (BitVec 1) 2) → (Vector α 9 × Vector α 2)
@@ -80,3 +80,19 @@ def module
           let updated_reg1 := v7
           (#v[v12, inp[6], 0#1, v3, 0#1, v9, inp[2], inp[3]], #v[updated_reg0, updated_reg1])
       )
+
+/-- We prove that the description at handshake level and the description at lower (RTL) level are bisimilar. -/
+theorem fork_bisim
+    (arg0_data arg0_valid arg1_data arg1_valid out0_ready out1_ready out2_ready : Stream' (BitVec 1))
+    (arg0 arg1 out0 out1 out2 : Stream (BitVec 1)) :
+    let := ReadyValid #v[arg0_data, arg0_valid, arg0_ready] arg0
+    let := ReadyValid #v[arg1_data, arg1_valid, arg1_ready] arg1
+    let := ReadyValid #v[out0_data, out0_valid, out0_ready] out0
+    let := ReadyValid #v[out1_data, out1_valid, out1_ready] out1
+    let := ReadyValid #v[out2_data, out2_valid, out2_ready] out2
+    Bisim (iso_unary' ((fork arg0_data arg0_valid arg1_data arg1_valid out0_ready oue1_ready out2_ready).get 0))  (HandshakeOp.fork arg0).fst := by
+  unfold iso_unary' HandshakeOp.fork
+  unfold Bisim
+  simp
+
+  sorry
diff --git a/SSA/Projects/CIRCT/Register/Basic.lean b/SSA/Projects/CIRCT/Register/Basic.lean
index 3be5a782ad..c54e37de83 100644
--- a/SSA/Projects/CIRCT/Register/Basic.lean
+++ b/SSA/Projects/CIRCT/Register/Basic.lean
@@ -2,24 +2,9 @@ import SSA.Projects.CIRCT.Stream.Basic
 import SSA.Projects.CIRCT.Stream.Lemmas
 import SSA.Projects.CIRCT.Handshake.Handshake
 
-<<<<<<< HEAD:SSA/Projects/CIRCT/Register/Basic.lean
-<<<<<<< HEAD:SSA/Projects/CIRCT/Register/Basic.lean
 /-! We model a register storing a value for one cycle -/
 
 namespace HandshakeStream
-=======
-namespace CIRCTStream
-=======
-open HandshakeStream
->>>>>>> 3410b43d9 (chore: fix fork and add to ci):SSA/Projects/CIRCT/Handshake-to-HW/fork.lean
-
-/-!
-Trace monoidal categories:
-we model a feedback loop as a function with a-many inputs and x-many inputs, producing b-many outputs
-and x-many outputs that are re-fed as inputs to the function (inputs, inputs from feedback, outputs,
-outputs to be fed-back)
--/
->>>>>>> 6701d2b8a (chore: proof statement):SSA/Projects/CIRCT/Handshake-to-HW/fork.lean
 
 /--
   The sequential logics defining the behaviour of a register, assuming it operates on a stream
@@ -148,3 +133,20 @@ def vec_to_streams' {α : Type u} {n : Nat} (xv : Stream' (Vector α n)) : Vecto
       `i`-th element of stream `xv`.
   -/
   Vector.ofFn (fun (k : Fin n) => fun (i : Nat) => (xv i).get k)
+
+/-! # Prove equivalence with handhshake circuit-/
+
+
+def drop_from_bitvecs (x : Vector (Stream' (BitVec 1)) 3) (n : Nat) : Vector (Stream' (BitVec 1)) 3 :=
+  x.map (fun (s : Stream' (BitVec 1)) => s.drop (n + 1))
+
+
+/-- We define the relation between a vector `Vector (Stream' (BitVec 1)) 3` containing the
+  data, ready and valid signals, and a `Stream (BitVec 1)` containing the same information
+  at handshake level.
+  `a[0]` contains the data, `a[1]` contains the `ready` signal, `a[2]` contains the `valid` signal.
+  -/
+def ReadyValid  (a : Vector (Stream' (BitVec 1)) 3) (b : Stream (BitVec 1)) :=
+  ∀ (n : Nat),
+      ((a[1] n = 1#1) ∧ (a[2] n = 1#1) ∧ (some (a[0] n) = b.get n))
+      ∨ ((a[1] n = 0#1) ∨ (a[2] n = 0#1) ∧ (none = b.get n))

From 55741ba84b4741510adc79392c87e261277cc9a9 Mon Sep 17 00:00:00 2001
From: luisacicolini <luisacicolini@gmail.com>
Date: Thu, 11 Dec 2025 09:26:48 +0000
Subject: [PATCH 6/9] chore: correct

---
 SSA/Projects/CIRCT/CIRCT.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/SSA/Projects/CIRCT/CIRCT.lean b/SSA/Projects/CIRCT/CIRCT.lean
index f86d5aab15..cc3ed1e700 100644
--- a/SSA/Projects/CIRCT/CIRCT.lean
+++ b/SSA/Projects/CIRCT/CIRCT.lean
@@ -2,7 +2,6 @@ import SSA.Projects.CIRCT.Handshake.Handshake
 import SSA.Projects.CIRCT.HSxComb.HSxCombFunctor
 import SSA.Projects.CIRCT.DC.DC
 import SSA.Projects.CIRCT.DCxComb.DCxCombFunctor
-import SSA.Projects.CIRCT.Handshake-to-HW.fork
 import SSA.Projects.CIRCT.DCPlus.DCPlus
 import SSA.Projects.CIRCT.Comb.Comb
 import SSA.Projects.CIRCT.Register.Basic

From 3f6508c28a54569d611be5c7cbf99dc42a505f07 Mon Sep 17 00:00:00 2001
From: luisacicolini <luisacicolini@gmail.com>
Date: Thu, 11 Dec 2025 09:27:25 +0000
Subject: [PATCH 7/9] chore: correct

---
 SSA/Projects/CIRCT/Stream/Lemmas.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/SSA/Projects/CIRCT/Stream/Lemmas.lean b/SSA/Projects/CIRCT/Stream/Lemmas.lean
index fbcb18c048..8e50944471 100644
--- a/SSA/Projects/CIRCT/Stream/Lemmas.lean
+++ b/SSA/Projects/CIRCT/Stream/Lemmas.lean
@@ -332,3 +332,8 @@ theorem syncMap2_syncMap2_eq_syncMap3 (f : α → β → γ) (g : γ → ε →
     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

From c3685ee46fae4e4e5274012a21f483d6891b3dea Mon Sep 17 00:00:00 2001
From: luisacicolini <luisacicolini@gmail.com>
Date: Thu, 11 Dec 2025 09:29:01 +0000
Subject: [PATCH 8/9] chore: correct

---
 SSA/Projects/CIRCT/Register/Basic.lean | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/SSA/Projects/CIRCT/Register/Basic.lean b/SSA/Projects/CIRCT/Register/Basic.lean
index c54e37de83..f1b5ac19be 100644
--- a/SSA/Projects/CIRCT/Register/Basic.lean
+++ b/SSA/Projects/CIRCT/Register/Basic.lean
@@ -134,18 +134,19 @@ def vec_to_streams' {α : Type u} {n : Nat} (xv : Stream' (Vector α n)) : Vecto
   -/
   Vector.ofFn (fun (k : Fin n) => fun (i : Nat) => (xv i).get k)
 
-/-! # Prove equivalence with handhshake circuit-/
-
-
+/--
+  Drop the first `n` elements of all the three streams in `x`.
+-/
 def drop_from_bitvecs (x : Vector (Stream' (BitVec 1)) 3) (n : Nat) : Vector (Stream' (BitVec 1)) 3 :=
-  x.map (fun (s : Stream' (BitVec 1)) => s.drop (n + 1))
+  x.map (fun (s : Stream' (BitVec 1)) => s.drop n)
 
-
-/-- We define the relation between a vector `Vector (Stream' (BitVec 1)) 3` containing the
+/--
+  We define the relation between a vector `Vector (Stream' (BitVec 1)) 3` containing the
   data, ready and valid signals, and a `Stream (BitVec 1)` containing the same information
   at handshake level.
   `a[0]` contains the data, `a[1]` contains the `ready` signal, `a[2]` contains the `valid` signal.
-  -/
+  This relation is useful to prove the equivalence between streams at handshake and hardware levels.
+-/
 def ReadyValid  (a : Vector (Stream' (BitVec 1)) 3) (b : Stream (BitVec 1)) :=
   ∀ (n : Nat),
       ((a[1] n = 1#1) ∧ (a[2] n = 1#1) ∧ (some (a[0] n) = b.get n))

From 25ad2a8f12f99af22d95c8f4d3045c903eba45b3 Mon Sep 17 00:00:00 2001
From: luisacicolini <luisacicolini@gmail.com>
Date: Thu, 11 Dec 2025 09:32:48 +0000
Subject: [PATCH 9/9] chore: it is important to be precise

---
 SSA/Projects/CIRCT/Register/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/SSA/Projects/CIRCT/Register/Basic.lean b/SSA/Projects/CIRCT/Register/Basic.lean
index f1b5ac19be..80223e0a61 100644
--- a/SSA/Projects/CIRCT/Register/Basic.lean
+++ b/SSA/Projects/CIRCT/Register/Basic.lean
@@ -145,7 +145,7 @@ def drop_from_bitvecs (x : Vector (Stream' (BitVec 1)) 3) (n : Nat) : Vector (St
   data, ready and valid signals, and a `Stream (BitVec 1)` containing the same information
   at handshake level.
   `a[0]` contains the data, `a[1]` contains the `ready` signal, `a[2]` contains the `valid` signal.
-  This relation is useful to prove the equivalence between streams at handshake and hardware levels.
+  This relation is useful to prove the bisimilarity between streams at handshake and hardware levels.
 -/
 def ReadyValid  (a : Vector (Stream' (BitVec 1)) 3) (b : Stream (BitVec 1)) :=
   ∀ (n : Nat),