HW.fork lowering : lemmas and refactoring

SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean

@@ -7,13 +7,18 @@ namespace HWComponents
 
 open HandshakeStream
 
-def hw_constant (b : Bool) : BitVec 1 :=
-  if b then 1#1 else 0#1
+/-
+  RTL-level definitions of circuit components
+-/
+def hw_constant (b : Bool) : BitVec 1 := if b then 1#1 else 0#1
+
+def comb_xor (x y : BitVec 1) : BitVec 1 := BitVec.xor x y
+
+def comb_and (x y : BitVec 1) : BitVec 1 := BitVec.and x y
+
+def comb_add (x y : BitVec 32) : BitVec 32 := BitVec.add x y
 
-def comb_xor : BitVec 1 → BitVec 1 → BitVec 1 := BitVec.xor
-def comb_and : BitVec 1 → BitVec 1 → BitVec 1 := BitVec.and
-def comb_add : BitVec 32 → BitVec 32 → BitVec 32 := BitVec.add
-def comb_or : BitVec 1 → BitVec 1 → BitVec 1 := BitVec.or
+def comb_or (x y : BitVec 1) : BitVec 1 := BitVec.or x y
 
 namespace TRY1
 
@@ -1179,7 +1184,7 @@ theorem hw_fork_refines1_with_fork:
             intro hcontra
             specialize hfstVldTrue2 fstSentIdx (by omega)
             simp [toStream, hfstVldTrue2] at hfstSentIdx
-          by_cases fstRecfst  : fstRdyOut ≤ fstRdyOut2
+          by_cases fstRecfst : fstRdyOut ≤ fstRdyOut2
           · /- first receiver comes first -/
             by_cases fstRecBeforeSent : fstVldTrue + fstRdyOut ≤ fstSentIdx
             · /- first receiver before sent -/
@@ -1190,28 +1195,40 @@ theorem hw_fork_refines1_with_fork:
                 · funext i
                   have := rdOut1_before_allDone (hfork := h_6) (n := i)
                   /- what happens to `rdOut1` after data is dispatched? -/
-
-                  sorry
+                  have heq : Stream'.drop (fstSentIdx + 1) rdIn_1 i = rdIn_1 (fstSentIdx + 1 + i) := by
+                    simp [Stream'.drop]
+                    congr 1
+                    grind
+                  rw [heq]
+                  by_cases hfalse : rdIn_1 (fstSentIdx + 1 + i) = 0#1
+                  · have := congr_fun h_7 (fstSentIdx + 1 + i)
+                    unfold toStream at this
+                    simp [hfalse] at *
+                    rw [hw_fork_eq]
+
+                    have : ∀ k, ∀ i, Stream'.drop k rdOut1_1 i =  rdOut1_1 (i + k) := by
+                      intros
+                      simp [Stream'.drop, Stream'.get]
+                    simp [hw_fork', Stream'.corec']
+                    unfold fork_corec
+                    simp [comb_and, comb_xor, comb_or, hw_constant]
+
+                    sorry
+                  · sorry
                 · sorry
                 · sorry
                 · sorry
                 · sorry
               · /- first receiver after sent -/
                 sorry
-            · /- first receiver after sent -/
-              by_cases sndRecBeforeSent : fstVldTrue + fstRdyOut2 ≤ fstSentIdx
-              · /- second receiver before sent -/
-                sorry
-              · /- first receiver after sent -/
-                sorry
+            · /- first receiver after sent, implies second receiver after sent -/
+              have : fstSentIdx ≤ fstVldTrue + fstRdyOut2 := by omega
+              sorry
           · /- second receiver comes first -/
             by_cases fstRecBeforeSent : fstVldTrue + fstRdyOut ≤ fstSentIdx
-            · /- first receiver before sent -/
-              by_cases sndRecBeforeSent : fstVldTrue + fstRdyOut2 ≤ fstSentIdx
-              · /- second receiver before sent -/
-                sorry
-              · /- first receiver after sent -/
-                sorry
+            · /- first receiver before sent, implies second receiver before sent -/
+              have : fstVldTrue + fstRdyOut2 ≤ fstSentIdx := by omega
+              sorry
             · /- first receiver after sent -/
               by_cases sndRecBeforeSent : fstVldTrue + fstRdyOut2 ≤ fstSentIdx
               · /- second receiver before sent -/