From a8464c8103bbac6462174baa1e098c850cc287bb Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Fri, 17 Apr 2026 13:51:06 +0100 Subject: [PATCH 1/6] polishing --- SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean | 25 ++++++++++---------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean b/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean index db58a4c633..66eefc1f1c 100644 --- a/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean +++ b/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean @@ -1179,7 +1179,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,6 +1190,11 @@ 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? -/ + have heq : Stream'.drop (fstSentIdx + 1) rdIn_1 i = rdIn_1 (fstSentIdx + 1 + i) := by + simp [Stream'.drop] + congr 1 + grind + rw [heq] sorry · sorry @@ -1198,20 +1203,14 @@ theorem hw_fork_refines1_with_fork: · 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 -/ From cd9730f9c314e734f90d017b7bfc236388d0f20d Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 30 Apr 2026 13:31:53 +0100 Subject: [PATCH 2/6] fix --- SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean | 34 +++++++++++++++----- 1 file changed, 26 insertions(+), 8 deletions(-) diff --git a/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean b/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean index 66eefc1f1c..c13b164b7e 100644 --- a/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean +++ b/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_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_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_or (x y : BitVec 1) : BitVec 1 := BitVec.or x y namespace TRY1 @@ -1195,8 +1200,21 @@ theorem hw_fork_refines1_with_fork: congr 1 grind rw [heq] - - sorry + 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 From 5bbb70a64b55e554f3056428b69b17c7d24d5362 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 30 Apr 2026 13:32:13 +0100 Subject: [PATCH 3/6] pull out main lemma --- .../CIRCT/HandshakeToHW/fork_lowering.lean | 1614 +++++++++++++++++ 1 file changed, 1614 insertions(+) create mode 100644 SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean diff --git a/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean new file mode 100644 index 0000000000..ca62d028c6 --- /dev/null +++ b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean @@ -0,0 +1,1614 @@ +import SSA.Projects.CIRCT.Stream.Basic +import SSA.Projects.CIRCT.Stream.Lemmas +import SSA.Projects.CIRCT.Register.Basic +import SSA.Projects.CIRCT.Register.Lemmas + +namespace HWComponents + +open HandshakeStream + + + +/-- + Latency-insensitive (handshake) fork component. + We assume that there are infinite buffers at the input and output of the fork. + This implies that ready == 1 (at the output), and that the input stream can be delayed infinitely long. + + Under this assumption, we do not really need the registers, + because we will instantly emit a value, and the registers will be constant true. + + This spec is the same as the hardware implementation if we guarantee that + a `ready` signal is received (no deadlock). + -/ +def handshake.fork (in0 : Stream (BitVec 32)) : Stream (BitVec 32) × Stream (BitVec 32) := + (in0, in0) + + +/- + 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_or (x y : BitVec 1) : BitVec 1 := BitVec.or x y + +/-- + RTL implementation of fork circuit. + We assume that valid signals are given by the stream, + and that ready signals are given by nondeterministic booleans. + -/ +def rtl.fork (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec 32)) + : Stream' ( BitVec 1 -- ready (_12) + × BitVec 1 -- valid_0 (_3) + × BitVec 1 -- valid_1 (_9) + × BitVec 32 -- rawOutput + × BitVec 32 -- rawOutput + ) + := + Stream'.corec' (α := Nat × BitVec 1 × BitVec 1) (fun (i, _emitted_0, _emitted_1) => + let _true := hw_constant true + let _false := hw_constant false + let _2 := comb_xor _emitted_0 _true + let _3 := comb_and _2 (_valid i) + let _4 := comb_and (_ready i) _3 + let _5 := comb_or _4 _emitted_0 -- done0 + let _8 := comb_xor _emitted_1 _true + let _9 := comb_and _8 (_valid i) + let _10 := comb_and (_ready_1 i) _9 + let _11 := comb_or _10 _emitted_1 -- done1 + let _12 := comb_and _5 _11 -- allDone + let _rawOutput := _in0 i + let _0 := comb_xor _12 _true + let _1 := comb_and _5 _0 + let _6 := comb_xor _12 _true + let _7 := comb_and _11 _6 + ((_12, _3, _9, _rawOutput, _rawOutput), (i + 1, _1, _7)) + ) (0, 0#1, 0#1) + +def split_stream2 : + Stream' (a × b × c × d × e) → Stream' a × Stream' b × Stream' c × Stream' d × Stream' e := + fun g => + (fun i => (g i).1, + fun i => (g i).2.1, + fun i => (g i).2.2.1, + fun i => (g i).2.2.2.1, + fun i => (g i).2.2.2.2) + + +/-- At the handshake level: (manual) delayed fork ~ normal fork: the outputs of the fork are bisimilar + for any delay (up to any numbers of `none` inserted, anywhere). -/ +theorem fork_refines {a x y x' y'} : + (x, y) = handshake.fork a → + x ~ x' → + y ~ y' → + x ~ x' ∧ y ~ y' := by grind + +/-- Stream := Stream' (Option α) -/ +def toStream {α} (rdy : Stream' (BitVec 1)) (vld : Stream' (BitVec 1)) (data : Stream' α) : Stream α := fun i => + if rdy i == 1#1 && vld i == 1#1 then + .some (data i) + else + .none + +/- the standard implementation of the fork refines the handshake fork (`TRY2.hw_fork`) -/ + +/-- weaker def where we do not assume that rdy is by default 0#1 -/ +def globallyValidUntilReady (vld rdy : Stream' (BitVec 1)) : Prop := + ∀ (i : Nat), + (vld i = 1#1) → + ∃ (k : Nat), + rdy (i + k) = 1#1 ∧ vld (i + k) = 1#1 ∧ + ∀ (j : Nat) (_hj : j < k), + vld (i + j) = 1#1 + +/-- This def is stronger than the one above -/ +def globallyValidUntilReady' (vld rdy : Stream' (BitVec 1)) : Prop := + ∀ (i : Nat), + (vld i = 1#1) → + ∃ (k : Nat), + rdy (i + k) = 1#1 ∧ vld (i + k) = 1#1 ∧ + ∀ (j : Nat) (_hj : j < k), + vld (i + j) = 1#1 ∧ rdy (i + j) = 0#1 + -- we should add sth like vld (i + k + 1) = 0#1? + +def globallyValidAndData (vld : Stream' (BitVec 1)) (data : Stream' (BitVec w)) : Prop := + ∀ (i : Nat), + (vld i = 1#1 ∧ vld (i + 1) = 1#1) → + data i = data (i + 1) + +def relation : Stream (BitVec w) → Stream (BitVec w) → Prop := fun x y => + ∃ (rd1 vld1 : Stream' (BitVec 1)) (data1 : Stream' (BitVec w)) + (rd2 vld2 : Stream' (BitVec 1)) (data2 : Stream' (BitVec w)), + x = toStream rd1 vld1 data1 ∧ + globallyValidUntilReady rd1 vld1 ∧ + globallyValidAndData vld1 data1 ∧ + y = toStream rd2 vld2 data2 ∧ + globallyValidUntilReady rd2 vld2 ∧ + globallyValidAndData vld2 data2 + /- we need to say something about `x` and `y`. -/ + +/-- G(F(val = 1))-/ +def globallyFinallyReady (x : Stream' (BitVec 1)) := + ∀ (i : Nat), + ∃ (k : Nat), + x (i + k) = 1#1 + +inductive relation' : Stream (BitVec w) → Stream (BitVec w) → Prop where + | intro x y rd vld data rd1 vld1 o1 : /- same as `∀ x y` -/ + /- x is the high-level (input), y is the low-level (output) -/ + x = toStream rd vld data → + y = toStream rd1 vld1 o1 → + (∀ j, (rd j = 1#1 ∧ vld j = 1#1) ↔ rd1 j = 1#1 ∧ vld1 j = 1#1) → + -- (∃ k, rd k = 1#1 ∧ vld k = 1) → /- at least one transition happens frfr -/ + globallyValidUntilReady vld rd → + globallyValidAndData vld data → + globallyFinallyReady rd1 → + (∀ n, vld n = 1#1 → data n = o1 n) → /- when the signal is valid, data and output are the same -/ + relation' x y /- defining the type of the relation -/ + +inductive relation_fork : Stream (BitVec w) → Stream (BitVec w) → Prop where + | intro x y rdIn vldIn dataIn rdOut1 vldOut1 dataOut1 rdOut2 vldOut2 dataOut2 : /- same as `∀ x y` -/ + /- x is the high-level (input), y is the low-level (output) -/ + x = toStream rdIn vldIn dataIn → + y = toStream rdOut1 vldOut1 dataOut1 → + /- if a signal in `x` is valid (`vldIn i = 1#1`), it will remain valid (at least) until a + ready signal is received (`rdIn (i + k) = 1#1`). A ready signal is eventually definitely received. -/ + globallyValidUntilReady vldIn rdIn → + globallyValidUntilReady vldOut1 rdOut1 → + globallyValidUntilReady vldOut2 rdOut2 → + /- if a signal in `x` is valid for more than one cycle (`vldIn i = 1#1 ∧ vldIn (i + 1) = 1#1`), + the data does not change (`dataIn i = dataIn (i + 1)`) -/ + globallyValidAndData vldIn dataIn → + /- eventually a ready signal arrives from both receivers (`rdOut1 i = 1#1`), (`rdOut2 i = 1#1`) -/ + globallyFinallyReady rdOut1 → + globallyFinallyReady rdOut2 → + /- input/output relationship around the `fork` module -/ + + (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn) → + relation_fork x y + + +/- + our implementation of `fork` should not allow this, assuming that the input is + well-formed (including its ready signals!). + + val1 = 1 1 1 + data1 = 2 3 4 + rd1 = 1 1 1 + out1: 2 3 4 + + val2 = 1 1 1 + data2 = 2 3 4 + rd2 = 0 1 1 + out2: - 3 4 + +-/ + + +/-- We unfold one step of the corecursive definition of `fork` -/ +def fork_corec (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec 32)) := + fun (i, _emitted_0, _emitted_1) => + let _true := hw_constant true + let _false := hw_constant false + let _2 := comb_xor _emitted_0 _true + let _3 := comb_and _2 (_valid i) + let _4 := comb_and (_ready i) _3 + let _5 := comb_or _4 _emitted_0 -- done0 + let _8 := comb_xor _emitted_1 _true + let _9 := comb_and _8 (_valid i) + let _10 := comb_and (_ready_1 i) _9 + let _11 := comb_or _10 _emitted_1 -- done1 + let _12 := comb_and _5 _11 -- allDone + let _rawOutput := _in0 i + let _0 := comb_xor _12 _true + let _1 := comb_and _5 _0 + let _6 := comb_xor _12 _true + let _7 := comb_and _11 _6 + ((_12, _3, _9, _rawOutput, _rawOutput), (i+1, _1, _7)) + +/-- We re-define the fork circuit in terms of `fork_corec` -/ +def hw_fork' (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec 32)) + : Stream' ( BitVec 1 -- ready (_12) + × BitVec 1 -- valid_0 (_3) + × BitVec 1 -- valid_1 (_9) + × BitVec 32 -- rawOutput + × BitVec 32 -- rawOutput + ) + := Stream'.corec' (α := Nat × BitVec 1 × BitVec 1) (fork_corec _ready _ready_1 _valid _in0) (0, 0#1, 0#1) + + + + +/-- Prove that iterating `n` times starting from the `m`-th index of the stream yields the `n + m`-th index-/ +theorem fork_corec1 : + (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (m, x, y) n).1 = n + m := by + induction n generalizing m x y with + | zero => grind [Stream'.iterate] + | succ x h => + rw [Stream'.iterate_eq] + dsimp [Stream'.cons] + dsimp [fork_corec] + grind + +theorem hw_fork'_vldOut1_of_none (h : ∀ k, vldIn k = 0#1) : + ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).2.1 = 0#1 := by + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get + generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, hw_constant] + specialize h a + simp [h] + +theorem hw_fork'_vldOut2_of_none (h : ∀ k, vldIn k = 0#1) : + ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).2.2.1 = 0#1 := by + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get + generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, hw_constant] + specialize h a + simp [h] + +lemma iterate_back_succ (f : α → α) (s : α) (n : ℕ) : + Stream'.iterate f s (n + 1) = f (Stream'.iterate f s n) := by + induction n generalizing s with + | zero => simp [Stream'.iterate_eq, Stream'.cons] + | succ k ih => rw [Stream'.iterate_eq, Stream'.cons, ih]; rfl + +lemma fork_emitted_zero_of_all_none (h : ∀ k, vldIn k = 0#1) : + ∀ k, (Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) + (0, 0#1, 0#1) k).2 = (0#1, 0#1) := by + intro k + induction k with + | zero => simp [Stream'.iterate] + | succ k ih => + rw [iterate_back_succ] + generalize hsk : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s + obtain ⟨a, b, c⟩ := s + simp [hsk] at ih + obtain ⟨rfl, rfl⟩ := ih + simp only [Function.comp] + dsimp [fork_corec, comb_and, comb_xor, comb_or, hw_constant] + simp [h a] + +-- when vld is always 0, all signal outputs (not data) are 0 +theorem hw_fork'_of_all_none (h : ∀ k, vldIn k = 0#1) : + ∀ k, ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).1 = 0#1 ∧ + ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).2.1 = 0#1 ∧ + ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).2.2.1 = 0#1 := by + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get + intro k + and_intros + · generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, hw_constant] + have hbc := fork_emitted_zero_of_all_none (dataIn := dataIn) (rdOut1 := rdOut1) + (rdOut2 := rdOut2) h k + rw [hst] at hbc + simp at hbc + obtain ⟨rfl, rfl⟩ := hbc + simp [h a, comb_or] + · generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, hw_constant] + specialize h a + simp [h] + · generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, hw_constant] + specialize h a + simp [h] + +/-- Prove that (at RTL level) the input and output data at the `n`-th position are the same. + This is possible because `hw_fork'` does not introduce any delay, and there is no transformation + happening on the data. -/ +theorem hw_fork_out0 + (h : ⟨rdy_out, vld0_out, vld1_out, data0_out, data1_out⟩ = split_stream2 (hw_fork' rd0_in rd1_in vld_in data_in)) : + (∀ n, data_in n = data0_out n) := by + intro n + simp [split_stream2] at h + simp [h] + unfold hw_fork'; clear h + unfold Stream'.corec' Stream'.corec Stream'.map Stream'.get + generalize h: (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (0, 0#1, 0#1) n) = y + obtain ⟨a, b, c⟩ := y + dsimp [fork_corec] + rw [show a = (a, b, c).1 by rfl, ←h, fork_corec1]; rfl + +theorem hw_fork_out1 + (h : ⟨rdy_out, vld0_out, vld1_out, data0_out, data1_out⟩ = + split_stream2 (hw_fork' rd0_in rd1_in vld_in data_in)) : + (∀ n, data_in n = data1_out n) := by + intro n + simp [split_stream2] at h + simp [h] + unfold hw_fork'; clear h + unfold Stream'.corec' Stream'.corec Stream'.map Stream'.get + generalize h: (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (0, 0#1, 0#1) n) = y + obtain ⟨a, b, c⟩ := y + dsimp [fork_corec] + rw [show a = (a, b, c).1 by rfl, ←h, fork_corec1]; rfl + + + + +theorem fork_corec1bis : + (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (m, x, y) n).1 = n + m := by + induction n generalizing m x y with + | zero => grind [Stream'.iterate] + | succ x h => + rw [Stream'.iterate_eq] + dsimp [Stream'.cons] + dsimp [fork_corec] + grind + +theorem hw_fork_eq : rtl.fork rd0 rd1 vld data = hw_fork' rd0 rd1 vld data := by + unfold rtl.fork hw_fork' + congr 1 + +theorem vldOut1_implies_vldIn + (h : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + (hvld : vldOut1 n = 1#1) : vldIn n = 1#1 := by + rw [hw_fork_eq] at h + simp [split_stream2] at h + obtain ⟨-, hvldout1, -⟩ := h + have hn := congr_fun hvldout1 n + rw [hvld] at hn + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) n = s at hn + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn + have heq : a = n := by + have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n + rw [hst] at this + simp at this + assumption + rw [← heq] + apply Classical.byContradiction + intro hcontra + have : vldIn a = 0#1 := by grind + simp [this] at hn + +theorem vldOut2_implies_vldIn + (h : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + (hvld : vldOut2 n = 1#1) : vldIn n = 1#1 := by + rw [hw_fork_eq] at h + simp [split_stream2] at h + obtain ⟨-, -, hvldout2, -⟩ := h + have hn := congr_fun hvldout2 n + rw [hvld] at hn + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) n = s at hn + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn + have heq : a = n := by + have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n + rw [hst] at this + simp at this + assumption + rw [← heq] + apply Classical.byContradiction + intro hcontra + have : vldIn a = 0#1 := by grind + simp [this] at hn + +theorem rdOut1_before_allDone + (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hvldOut1 : vldOut1 n = 1#1) + (hgvurIn : globallyValidUntilReady vldIn rdIn) : + ∃ k, rdIn (n + k) = 1#1 ∧ vldIn (n + k) = 1#1 := by + have hvldIn := vldOut1_implies_vldIn hfork hvldOut1 + unfold globallyValidUntilReady at hgvurIn + specialize hgvurIn n hvldIn + obtain ⟨k, hk⟩ := hgvurIn + exists k + simp [hk] + +lemma iterate_succ_apply (f : α → α) (s : α) (n : ℕ) : + Stream'.iterate f s (n + 1) = f (Stream'.iterate f s n) := by + induction n generalizing s with + | zero => simp [Stream'.iterate] + | succ k ih => + rw [Stream'.iterate_eq, Stream'.cons] + exact ih _ + + + +theorem vldOut_eq_vldIn_of_fork_unitl_sent + (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + /- nothing is emitted before `n`, as emission occurs if `rdOut1 j ∧ vldOut1 j` -/ + (hbefore : ∀ j < n, rdOut1 j = 0#1 ∨ vldOut1 j = 0#1) : + vldOut1 n = vldIn n := by + rw [hw_fork_eq] at hfork + simp [split_stream2] at hfork + obtain ⟨-, hvldout1, -⟩ := hfork + have hn := congr_fun hvldout1 n + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) n = s at hn + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn + have hb : b = 0#1 := by + apply Classical.byContradiction + intro hcontra + have : b = 1#1 := by grind + subst this + simp at hn + suffices key : ∀ m, (∀ j < m, rdOut1 j = 0#1 ∨ vldOut1 j = 0#1) → + (Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) m).2.1 = 0#1 by + have := key n hbefore + rw [hst] at this + simp at this + intro m + induction m with + | zero => simp [Stream'.iterate] + | succ k ihk => + intro hbef + have hbk := ihk (fun j hj => hbef j (Nat.lt_succ_of_lt hj)) + generalize hsk : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = sk + obtain ⟨ak, bk, ck⟩ := sk + simp [hsk] at hbk; subst hbk + rw [iterate_back_succ, hsk] + have hak : ak = k := by + have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 k + simp [hsk] at this; omega + have hk := hbef k (Nat.lt_succ_self k) + simp only [Function.comp] + have hvldk : vldOut1 k = vldIn ak := by + have h := congr_fun hvldout1 k + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at h + simp_rw [hsk] at h + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at h + simp_all + ext k hk + simp [show k = 0 by omega] + dsimp [fork_corec, comb_and, comb_xor, comb_or, hw_constant] + subst hak + by_cases hrd : rdOut1 ak = 1#1 <;> by_cases hvld : vldIn ak = 1#1 <;> by_cases hck : ck = 1#1 <;> by_cases hrd2 : rdOut2 ak = 1#1 + · simp [hrd, hvld, hck] + · simp [hrd, hvld, hck] + · have h0 : ck = 0#1 := by grind + simp [hrd, hvld, h0, hrd2] + · have h0 : ck = 0#1 := by grind + have h1 : rdOut2 ak = 0#1 := by grind + simp [hrd] at hk + simp_all + · have h0 : vldIn ak = 0#1 := by grind + simp [hrd, h0, hrd2] + · have h0 : vldIn ak = 0#1 := by grind + have h1 : rdOut2 ak = 0#1 := by grind + simp [hrd, h0, h1] + · have h0 : vldIn ak = 0#1 := by grind + simp [hrd, h0] + · simp [hrd] at hk + simp_all + · have h1 : rdOut1 ak = 0#1 := by grind + simp [h1, hvld, hck] + · have h1 : rdOut1 ak = 0#1 := by grind + simp [hvld, hck, h1] + · have h1 : rdOut1 ak = 0#1 := by grind + simp [hvld, h1] + · have h1 : rdOut1 ak = 0#1 := by grind + simp [h1, hvld] + · have h1 : rdOut1 ak = 0#1 := by grind + simp [h1, hck] + · have h1 : rdOut1 ak = 0#1 := by grind + simp [h1, hck] + · have h1 : rdOut1 ak = 0#1 := by grind + simp [h1] + · have h1 : rdOut1 ak = 0#1 := by grind + simp [h1] + simp [hb] at hn + have heq : a = n := by + have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n + rw [hst] at this + simp at this + assumption + rw [← heq] at ⊢ hn + simp [hn] + ext k hk + simp [show k = 0 by omega] + +theorem vldOut_of_vldIn_rdy + (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + /- nothing has been accepted so far -/ + (hbefore : ∀ l < j, rdOut1 l = 0#1 ∨ vldOut1 l = 0#1) + (hin : vldIn j = 1#1 ∧ rdIn j = 1#1) : + vldOut1 j = 1#1 := by + rw [vldOut_eq_vldIn_of_fork_unitl_sent (hfork := hfork) (hbefore := hbefore)] + simp [hin] + +theorem vldOut_eq_vldIn_of_fork_unitl_sent2 + (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + /- nothing is emitted before `n`, as emission occurs if `rdOut1 j ∧ vldOut1 j` -/ + (hbefore : ∀ j < n, rdOut2 j = 0#1 ∨ vldOut2 j = 0#1) : + vldOut2 n = vldIn n := by + rw [hw_fork_eq] at hfork + simp [split_stream2] at hfork + obtain ⟨-, -, hvldout2, -⟩ := hfork + have hn := congr_fun hvldout2 n + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) n = s at hn + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn + have hc0 : c = 0#1 := by + suffices key : ∀ m, (∀ j < m, rdOut2 j = 0#1 ∨ vldOut2 j = 0#1) → + (Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) + (0, 0#1, 0#1) m).2.2 = 0#1 by + have := key n hbefore + rw [hst] at this; simpa using this + intro m + induction m with + | zero => simp [Stream'.iterate] + | succ k ihk => + intro hbef + have hck := ihk (fun j hj => hbef j (Nat.lt_succ_of_lt hj)) + generalize hsk : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = sk + obtain ⟨ak, bk, ck⟩ := sk + simp [hsk] at hck; subst hck + have hak : ak = k := by + have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 k + grind + have hvldk : vldOut2 k = vldIn ak := by + have h := congr_fun hvldout2 k + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at h + simp_rw [hsk] at h + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at h + simp_all + ext k hk + simp [show k = 0 by omega] + have hk := hbef k (Nat.lt_succ_self k) + rw [iterate_back_succ, hsk] + simp only [Function.comp] + dsimp [fork_corec, comb_and, comb_xor, comb_or, hw_constant] + rcases hk with h | h + · simp_all + · rw [hvldk] at h + rcases hak ▸ h with h + have hvldInA : vldIn ak = 0#1 := by grind + simp [hvldInA]; + have heq : a = n := by + have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n + rw [hst] at this + simp at this + assumption + rw [← heq] at ⊢ hn + simp [hn] + ext k hk + simp [show k = 0 by omega] + intros + simp [hc0] + +theorem data_remains_constant_if + (h : globallyValidAndData vld data) + (h' : globallyValidUntilReady vld rdy) : + ∀ i, vld i = 1#1 → + ∃ k, (rdy (i + k) = 1#1 ∧ vld (i + k) = 1#1 ∧ + (∀ j (_hj : j ≤ k), vld (i + j) = 1#1 )∧ + (∀ j (_hj : j ≤ k), data (i + j) = data i)) := by + unfold globallyValidAndData at h + unfold globallyValidUntilReady at h' + intros i + specialize h' i + by_cases htrue : vld i = 1#1 + · simp [htrue] at h' ⊢ + obtain ⟨k, hk⟩ := h' + exists k + simp [hk] + by_cases hk0 : 0 < k + · and_intros + · intro j hj + obtain ⟨h1, h2, h3⟩ := hk + by_cases hlt : j < k + · apply h3 + exact hlt + · simp [show j = k by omega, h2] + · intros l hl + induction l + · simp + · case _ l' ihl' => + rw [show (i + (l' + 1)) = (i + l') + 1 by omega] + obtain ⟨h1, h2, h3⟩ := hk + by_cases hle : l' + 1 < k + · rw [← ihl' (by omega)] + apply Eq.symm + apply h + simp_all + and_intros + · apply h3 + omega + · rw [show (i + l') + 1 = (i + (l' + 1)) by omega] + apply h3 + assumption + · have : l' + 1 = k := by omega + specialize ihl' (by omega) + rw [← ihl'] + apply Eq.symm + apply h + and_intros + · apply h3 + assumption + · rw [show k = l' + 1 by omega, show (i + (l' + 1)) = (i + l') + 1 by omega] at h2 + assumption + · simp [show k = 0 by omega, htrue] + · simp [show vld i = 0#1 by grind] + + + +theorem not_exists_transmitted_element + (hv : ∀ i, vld i = 0#1) + (hx : x = toStream rdy vld data) : + ∀ k, x k = none := by + unfold toStream at hx + simp at hx + intros k + have hkx := congr_fun hx k + simp [show vld k = 0#1 by grind] at hkx + simp [hkx] + +theorem not_exists_transmitted_element_before + (hv : ∀ i (_ : i < limit), vld i = 0#1) + (hx : x = toStream rdy vld data) : + ∀ k (_ : k < limit), x k = none := by + intros k hk + unfold toStream at hx + simp at hx + have hkx := congr_fun hx k + simp [show vld k = 0#1 by grind] at hkx + simp [hkx] + +theorem if_exists_first_exists {st : Stream' (BitVec 1)} (h : ∃ k , st k = 1#1) : + ∃ j, (st j = 1#1 ∧ ∀ n (_ : n < j), st n = 0#1) := by + suffices key : ∀ k, st k = 1#1 → ∃ j, st j = 1#1 ∧ ∀ n < j, st n = 0#1 by + obtain ⟨k, hk⟩ := h; exact key k hk + intro k + induction k using Nat.strongRecOn with + | _ k ih => + intro hk + by_cases h0 : ∃ m < k, st m = 1#1 + · obtain ⟨m, hm, hms⟩ := h0 + exact ih m hm hms + · refine ⟨k, hk, fun n hn => ?_⟩ + by_contra hc + have hst : st n = 1#1 := by grind + exact h0 ⟨n, hn, hst⟩ + +theorem exists_first_transmitted_element + (hv : ∃ i, vld i = 1#1) + (hgf : globallyValidUntilReady vld rdy) + (hx : x = toStream rdy vld data) : + ∃ k, (x k = some (data k) ∧ ∀ j (_ : j < k), x j = none) := by + obtain ⟨i, hi⟩ := hv + obtain ⟨k, hkr, hkv, -⟩ := hgf i hi + let combined := fun n => if rdy n == 1#1 && vld n == 1#1 then 1#1 else (0#1 : BitVec 1) + have hex : ∃ n, combined n = 1#1 := ⟨i + k, by simp [combined, hkr, hkv]⟩ + obtain ⟨j, hjfire, hjmin⟩ := if_exists_first_exists hex + refine ⟨j, ?_, ?_⟩ + · simp [combined] at hjfire + rw [hx, toStream] + simp [hjfire.1, hjfire.2] + · intro l hl + rw [hx, toStream] + have h0 := hjmin l hl + simp [combined] at h0 + grind + +theorem exists_first_received_element + (hv : ∃ i, rdy i = 1#1 ∧ vld i = 1#1) + (hx : x = toStream rdy vld data) : + ∃ k, (x k = some (data k) ∧ ∀ j (_ : j < k), x j = none) := by + obtain ⟨fst, hfst_fire, hfst_min⟩ := if_exists_first_exists + (st := fun n => if ((rdy n == 1#1) && (vld n == 1#1)) then 1#1 else 0#1) + (by + obtain ⟨k, hk⟩ := hv + exists k + simp [hk]) + refine ⟨fst, ?_, ?_⟩ + · rw [hx, toStream] + have : ((rdy fst == 1#1) && (vld fst == 1#1))= true := by + by_contra hc; simp [hc] at hfst_fire + simp only [Bool.and_eq_true, beq_iff_eq] at this + simp [this.1, this.2] + · intro j hj + rw [hx, toStream] + have hj_not := hfst_min j hj + by_cases hrdy : rdy j == 1#1 && vld j == 1#1 + · simp [hrdy] at hj_not + · simp only [Bool.and_eq_true, beq_iff_eq, not_and] at hrdy + by_cases hr : rdy j = 1#1 + · have hvj := hrdy (by simpa using hr) + simp [show (rdy j == 1#1) = true by simpa, show (vld j == 1#1) = false by simpa] + · simp [show (rdy j == 1#1) = false by simpa] + + +theorem exists_transmitted_element + (h : globallyValidUntilReady vld rdy) + (hx : x = toStream rdy vld data) : + ∃ k, x k = some (data k) ∨ ∀ k, x k = none := by + by_cases hexists : ∃ i, vld i = 1#1 + · unfold toStream at hx + unfold globallyValidUntilReady at h + obtain ⟨i, hi⟩ := hexists + specialize h i (by omega) + obtain ⟨k, hk1, hk2, hk3⟩ := h + exists (i + k) + have hkx := congr_fun hx (i + k) + simp [hk1, hk2] at hkx + simp [hkx] + · simp [not_exists_transmitted_element (x := x) (data := data) (rdy := rdy) (vld := vld) (by grind) hx] + +theorem false_of_width_one (b : BitVec 1) (h : ¬ b = 1#1 ) : b = 0#1 := by grind + +theorem true_of_width_one (b : BitVec 1) (h : ¬ b = 0#1 ) : b = 1#1 := by grind + +theorem vldIn_and_eventually_ready_implies_vldOut1 + (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + (hvldIn : globallyFinallyReady vldIn) : + ∃ k, vldOut1 k = 1#1 := by + obtain ⟨n, hvldn, hnmin⟩ := if_exists_first_exists (hvldIn 0 |>.imp (fun k hk => by simpa using hk)) + have hbefore : ∀ j < n, rdOut1 j = 0#1 ∨ vldOut1 j = 0#1 := by + intro j hj + right + have hvldj : vldIn j = 0#1 := hnmin j hj + by_contra hc + have : vldIn j = 1#1 := vldOut1_implies_vldIn hfork (by grind) + rw [this] at hvldj + simp at hvldj + exact ⟨n, vldOut_eq_vldIn_of_fork_unitl_sent hfork hbefore |>.symm ▸ hvldn⟩ + +theorem vldIn_and_ready_implies_vldOut1 + (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + (hvldIn : ∃ j, vldIn j = 1#1) : + ∃ k, vldOut1 k = 1#1 := by + obtain ⟨n, hvldn, hnmin⟩ := if_exists_first_exists (st := vldIn) (by grind) + have hbefore : ∀ j < n, rdOut1 j = 0#1 ∨ vldOut1 j = 0#1 := by + intro j hj + right + have hvldj : vldIn j = 0#1 := hnmin j hj + by_contra hc + have : vldIn j = 1#1 := vldOut1_implies_vldIn hfork (by grind) + rw [this] at hvldj + simp at hvldj + exact ⟨n, vldOut_eq_vldIn_of_fork_unitl_sent hfork hbefore |>.symm ▸ hvldn⟩ + +theorem vldIn_and_ready_implies_vldOut2 + (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + (hvldIn : ∃ j, vldIn j = 1#1) : + ∃ k, vldOut2 k = 1#1 := by + obtain ⟨n, hvldn, hnmin⟩ := if_exists_first_exists (st := vldIn) (by grind) + have hbefore : ∀ j < n, rdOut2 j = 0#1 ∨ vldOut2 j = 0#1 := by + intro j hj + right + have hvldj : vldIn j = 0#1 := hnmin j hj + by_contra hc + have : vldIn j = 1#1 := vldOut2_implies_vldIn hfork (by grind) + rw [this] at hvldj + simp at hvldj + exact ⟨n, vldOut_eq_vldIn_of_fork_unitl_sent2 hfork hbefore |>.symm ▸ hvldn⟩ + +lemma fork_globallyValidAndData_out1 + (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + (hgv : globallyValidAndData vldIn dataIn) : + globallyValidAndData vldOut1 dataOut1 := by + intro i ⟨hi1, hi2⟩ + have hdata := hw_fork_out0 hfork + rw [← hdata i, ← hdata (i+1)] + apply hgv + exact ⟨vldOut1_implies_vldIn hfork hi1, vldOut1_implies_vldIn hfork hi2⟩ + + +lemma globallyValidAndData_stable (hgv : globallyValidAndData vld data) + (hrange : ∀ j, m ≤ j → j ≤ n → vld j = 1#1) (h : m ≤ n) : + data m = data n := by + induction h with + | refl => rfl + | step h ih => + rw [ih (fun j hj1 hj2 => hrange j hj1 (Nat.le_succ_of_le hj2))] + apply hgv + exact ⟨hrange _ (by omega) (by omega), + hrange _ (Nat.le_succ_of_le h) (Nat.le_refl _)⟩ + +theorem data_remains_constant_until_first + (h : globallyValidAndData vld data) + (h' : globallyValidUntilReady vld rdy) + (hi : vld i = 1#1) : + ∃ k, rdy (i + k) = 1#1 ∧ vld (i + k) = 1#1 ∧ + (∀ j (_hj : j ≤ k), vld (i + j) = 1#1) ∧ + (∀ j (_hj : j ≤ k), data (i + j) = data i) ∧ + (∀ m (_hm : m < k), rdy (i + m) = 0#1) := by + -- get any witness first + obtain ⟨k, hkrd, hkvld, hkvldall, hkdata⟩ := data_remains_constant_if h h' i hi + -- find the minimum via if_exists_first_exists + obtain ⟨kMin, hkMin_fire, hkMin_min⟩ := if_exists_first_exists + (st := fun m => if rdy (i + m) == 1#1 && vld (i + m) == 1#1 then 1#1 else 0#1) + ⟨k, by simp [hkrd, hkvld]⟩ + simp only [ite_eq_left_iff, Bool.and_eq_true, beq_iff_eq, not_and] at hkMin_fire hkMin_min + -- extract rdy and vld at kMin + have hkMinrd : rdy (i + kMin) = 1#1 := by + by_contra hc + simp [show rdy (i + kMin) ≠ 1#1 from hc] at hkMin_fire + have hkMinvld : vld (i + kMin) = 1#1 := by + by_contra hc + grind + -- kMin ≤ k + have hkMinlek : kMin ≤ k := by + by_contra hlt; push_neg at hlt + have := hkMin_min k hlt + simp [hkrd, hkvld] at this + refine ⟨kMin, hkMinrd, hkMinvld, ?_, ?_, ?_⟩ + · -- vld stays 1 for j ≤ kMin + intro j hj + exact hkvldall j (by omega) + · -- data stays constant for j ≤ kMin + intro j hj + exact hkdata j (by omega) + · -- rdy = 0 before kMin + intro m hm + by_contra hc + have hrdm : rdy (i + m) = 1#1 := by grind + -- vld (i + m) = 1 since m < kMin ≤ k + have hvldm : vld (i + m) = 1#1 := hkvldall m (by omega) + have := hkMin_min m hm + simp [hrdm, hvldm] at this + + +def readyOut1UntilAllReceiversAre(rdOut1 rdOut2 : Stream' (BitVec 1)) := + ∀ i, + rdOut1 i = 1#1 → + ∀ j, rdOut2 (i + j) = 0#1 → rdOut1 (i + j) = 1#1 + +def readyOut2UntilAllReceiversAre (rdOut1 rdOut2 : Stream' (BitVec 1)) := + ∀ i, + rdOut2 i = 1#1 → + ∀ j, rdOut1 (i + j) = 0#1 → rdOut2 (i + j) = 1#1 + +/-- the standard implementation of the fork refines the handshake fork (`TRY2.hw_fork`) -/ +theorem hw_fork_refines1_with_fork: + /- Given a handshake fork taking `a` as input and returning `(a, a)`, we take + its lowering (with input a bisimilar ready-valid wrapped stream) -/ + (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn) → + /- We want to make sure that stalling is correctly modeled for `a` (input). + We constrain the input and prove that if the input behaves properly, + the output will. -/ + globallyValidUntilReady vldOut1 rdOut1 → + globallyValidUntilReady vldOut2 rdOut2 → + globallyValidUntilReady vldIn rdIn → + readyOut1UntilAllReceiversAre (rdOut1 := rdOut1) (rdOut2 := rdOut2) → + readyOut2UntilAllReceiversAre (rdOut1 := rdOut1) (rdOut2 := rdOut2) → + globallyValidAndData vldOut1 dataOut1 → + globallyValidAndData vldOut2 dataOut2 → + globallyValidAndData vldIn dataIn → + /- we assume no deadlock -/ + globallyFinallyReady rdIn → + globallyFinallyReady rdOut1 → + globallyFinallyReady rdOut2 → + /- if we know that the hshake input stream is bisimilar to the ready-valid input of the hw fork (`a ~ rdy vld i`), meaning that the two outputs are also bisimilar by transitivity-/ + /- we want to prove that the outputs of the handshake fork are respectively + bisimilar to the ready-valid wrapping of the output of the hardware fork -/ + (toStream rdIn vldIn dataIn) ~ (toStream rdOut1 vldOut1 dataOut1) := by + intros hfork hgvurOutt1 hvgurOut2 hgvurIn hout1 hout2 hgvdOut1 hgvdOut2 hgvdIn hgfrIn hgfrOut1 hgfrOut2 + /- if 0, 0 works we don't need bisimilarity -/ + /- the high-level fork will never wait for anything (whenever an input is available), + while the low-level one might have to, and depends on the `rd1` signal eventually being true. + if we choose `pred := Eq` the relation is too strong, the second goal is not provable. + -/ + apply Bisim.coinduct (pred := relation_fork) + · intros sin sout hrel + /- `sin` and `sout` exist at the handshake level of the design -/ + rcases hrel + expose_names + by_cases hvldExists : ∃ k, vldIn_1 k = 1#1 + · have := if_exists_first_exists hvldExists + obtain ⟨fstVldTrue, hfstVldTrue1, hfstVldTrue2⟩ := this + /- we need to find the first element that is transmitted -/ + have hfstSent := exists_first_transmitted_element + (data := dataIn_1) (vld := vldIn_1) (rdy := rdIn_1) (x := sin) + (by grind) (by assumption) (by assumption) + have ⟨fstRdyOut, hfstRdyOut⟩ := if_exists_first_exists (h_4 fstVldTrue) + have ⟨fstRdyOut2, hfstRdyOut2⟩ := if_exists_first_exists (h_5 fstVldTrue) + unfold globallyFinallyReady at h_4 + have hvldinout := vldIn_and_ready_implies_vldOut1 + (dataIn := dataIn_1) (vldIn := vldIn_1) (rdIn := rdIn_1) + (rdOut1 := rdOut1_1) (rdOut2 := rdOut2_1) (vldOut1 := vldOut1_1) (vldOut2 := vldOut2_1) + (dataOut1 := dataOut1_1) (dataOut2 := dataOut2_1) (by grind) (by grind) + have hvldinout2 := vldIn_and_ready_implies_vldOut2 + (dataIn := dataIn_1) (vldIn := vldIn_1) (rdIn := rdIn_1) + (rdOut1 := rdOut1_1) (rdOut2 := rdOut2_1) (vldOut1 := vldOut1_1) (vldOut2 := vldOut2_1) + (dataOut1 := dataOut1_1) (dataOut2 := dataOut2_1) (by grind) (by grind) + have hfstRec := exists_first_received_element + (data := dataOut1_1) (vld := vldOut1_1) (rdy := rdOut1_1) (x := sout) (hx := h_8) + have ⟨fstSentIdx, hfstSentIdx⟩ := hfstSent + exists fstSentIdx, (fstVldTrue + fstRdyOut) + and_intros + · apply relation_fork.intro + (Stream'.drop (fstSentIdx + 1) sin) (Stream'.drop (fstVldTrue + fstRdyOut + 1) sout) + (dataIn := Stream'.drop (fstSentIdx + 1) dataIn_1) + (rdIn := Stream'.drop (fstSentIdx + 1) rdIn_1) + (vldIn := Stream'.drop (fstSentIdx + 1) vldIn_1) + (vldOut1 := Stream'.drop (fstVldTrue + fstRdyOut + 1) vldOut1_1) + (vldOut2 := Stream'.drop (fstVldTrue + fstRdyOut + 1) vldOut2_1) + (dataOut1 := Stream'.drop (fstVldTrue + fstRdyOut + 1) dataOut1_1) + (dataOut2 := Stream'.drop (fstSentIdx + 1) dataOut2_1) + (rdOut1 := Stream'.drop (fstVldTrue + fstRdyOut + 1) rdOut1_1) + (rdOut2 := Stream'.drop (fstVldTrue + fstRdyOut + 1) rdOut2_1) + · simp_all + rfl + · simp_all + rfl + · unfold globallyValidUntilReady at ⊢ h + intro j hj + specialize h (j + fstSentIdx + 1) hj + obtain ⟨k, hk1, hk2, hk3⟩ := h + exists k + have hv : Stream'.drop (fstSentIdx + 1) vldIn_1 j = vldIn_1 (j + fstSentIdx + 1) := by rfl + rw [hv] at hj + have hv : Stream'.drop (fstSentIdx + 1) vldIn_1 (j + k) = vldIn_1 (j + k + fstSentIdx + 1) := by rfl + have hr : Stream'.drop (fstSentIdx + 1) rdIn_1 (j + k) = rdIn_1 (j + k + fstSentIdx + 1) := by rfl + simp [hv, hr, show j + k + fstSentIdx + 1 = j + fstSentIdx + 1 + k by omega, hk1, hk2] + intros n hn + have hn : Stream'.drop (fstSentIdx + 1) vldIn_1 (j + n) = vldIn_1 (j + n + fstSentIdx + 1) := by rfl + simp [hn] + specialize hk3 n (by omega) + simp [show j + n + fstSentIdx + 1 = j + fstSentIdx + 1 + n by omega, hk3] + · unfold globallyValidUntilReady at ⊢ h_1 + intro j hj + have hj2 : Stream'.drop (fstVldTrue + fstRdyOut + 1) vldOut1_1 j = vldOut1_1 (j + fstVldTrue + fstRdyOut + 1) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + rw [hj2] at hj + specialize h_1 (j + fstVldTrue + fstRdyOut + 1) hj + obtain ⟨k, hk1, hk2, hk3⟩ := h_1 + exists k + have hv : Stream'.drop (fstVldTrue + fstRdyOut + 1) vldOut1_1 (j + k) = vldOut1_1 (j + k + fstVldTrue + fstRdyOut + 1) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + have hr : Stream'.drop (fstVldTrue + fstRdyOut + 1) rdOut1_1 (j + k) = rdOut1_1 (j + k + fstVldTrue + fstRdyOut + 1) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + simp [hv, hr, show j + k + fstVldTrue + fstRdyOut + 1 = j + fstVldTrue + fstRdyOut + 1 + k by omega, hk1, hk2] + intros n hn + have hn : Stream'.drop (fstVldTrue + fstRdyOut + 1) vldOut1_1 (j + n) = vldOut1_1 (j + n + fstVldTrue + fstRdyOut + 1) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + simp [hn] + specialize hk3 n (by omega) + simp [show j + n + fstVldTrue + fstRdyOut + 1 = j + fstVldTrue + fstRdyOut + 1 + n by omega, hk3] + · unfold globallyValidUntilReady at ⊢ h_2 + intro j hj + have hj2 : Stream'.drop (fstVldTrue + fstRdyOut + 1) vldOut2_1 j = vldOut2_1 (j + fstVldTrue + fstRdyOut + 1) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + rw [hj2] at hj + specialize h_2 (j + fstVldTrue + fstRdyOut + 1) hj + obtain ⟨k, hk1, hk2, hk3⟩ := h_2 + exists k + have hv : Stream'.drop (fstVldTrue + fstRdyOut + 1) vldOut2_1 (j + k) = vldOut2_1 (j + k + fstVldTrue + fstRdyOut + 1) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + have hr : Stream'.drop (fstVldTrue + fstRdyOut + 1) rdOut2_1 (j + k) = rdOut2_1 (j + k + fstVldTrue + fstRdyOut + 1) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + simp [hv, hr, show j + k + fstVldTrue + fstRdyOut + 1 = j + fstVldTrue + fstRdyOut + 1 + k by omega, hk1, hk2] + intros n hn + have hn : Stream'.drop (fstVldTrue + fstRdyOut + 1) vldOut2_1 (j + n) = vldOut2_1 (j + n + fstVldTrue + fstRdyOut + 1) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + simp [hn] + specialize hk3 n (by omega) + simp [show j + n + fstVldTrue + fstRdyOut + 1 = j + fstVldTrue + fstRdyOut + 1 + n by omega, hk3] + · unfold globallyValidAndData at ⊢ h_3 + intro j + specialize h_3 (j + fstSentIdx + 1) + have hr : Stream'.drop (fstSentIdx + 1) dataIn_1 j = dataIn_1 (j + fstSentIdx + 1) := by rfl + have hr' : Stream'.drop (fstSentIdx + 1) dataIn_1 (j + 1) = dataIn_1 (j + 1 + fstSentIdx + 1) := by rfl + simp [hr, hr'] + simp [show j + 1 + fstSentIdx + 1 = j + fstSentIdx + 1 + 1 by omega] + intro h1 h2 + apply h_3 + have htmp : Stream'.drop (fstSentIdx + 1) vldIn_1 j = vldIn_1 (j + fstSentIdx + 1) := by rfl + rw [htmp] at h1 + simp [h1] + have htmp : Stream'.drop (fstSentIdx + 1) vldIn_1 (j + 1) = vldIn_1 (j + 1 + fstSentIdx + 1) := by rfl + simp [show j + 1 + fstSentIdx + 1 = j + fstSentIdx + 1 + 1 by omega, htmp] at h2 + simp [h2] + · unfold globallyFinallyReady + intros i + specialize h_4 (i + fstVldTrue + fstRdyOut + 1) + obtain ⟨k, hk⟩ := h_4 + exists k + have htmp : Stream'.drop (fstVldTrue + fstRdyOut + 1) rdOut1_1 (i + k) = rdOut1_1 (i + k + fstVldTrue + fstRdyOut + 1) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + simp [htmp, show i + k + fstVldTrue + fstRdyOut + 1 = i + fstVldTrue + fstRdyOut + 1 + k by omega, hk] + · unfold globallyFinallyReady at h_5 ⊢ + intro j + specialize h_5 (fstVldTrue + fstRdyOut + 1 + j) + obtain ⟨k, hk⟩ := h_5 + exists k + have h : Stream'.drop (fstVldTrue + fstRdyOut + 1) rdOut2_1 (j + k) = rdOut2_1 (fstVldTrue + fstRdyOut + 1 + j + k) := by + simp [Stream'.drop, Stream'.get] + congr 1 + omega + simp [h, hk] + · have : fstVldTrue ≤ fstSentIdx := by + simp_all + apply Classical.byContradiction + intro hcontra + specialize hfstVldTrue2 fstSentIdx (by omega) + simp [toStream, hfstVldTrue2] at hfstSentIdx + by_cases fstRecfst : fstRdyOut ≤ fstRdyOut2 + · /- first receiver comes first -/ + by_cases fstRecBeforeSent : fstVldTrue + fstRdyOut ≤ fstSentIdx + · /- first receiver before sent -/ + by_cases sndRecBeforeSent : fstVldTrue + fstRdyOut2 ≤ fstSentIdx + · /- second receiver before sent -/ + simp [split_stream2] + and_intros + · funext i + have := rdOut1_before_allDone (hfork := h_6) (n := i) + /- what happens to `rdOut1` after data is dispatched? -/ + 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, 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, 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 -/ + sorry + · /- first receiver after sent -/ + sorry + · simp [Stream'.get, h_8, h_7, toStream] + have hdataeq := hw_fork_out0 (h := h_6) + by_cases hle : fstVldTrue ≤ fstSentIdx + · have hreadyIn : rdIn_1 fstSentIdx = 1#1 := by + unfold toStream at h_7 + have h_6sent := congr_fun h_7 fstSentIdx + simp [hfstSentIdx] at h_6sent + simp [h_6sent] + have hvalidIn: vldIn_1 fstSentIdx = 1#1 := by + unfold toStream at h_7 + have h_6sent := congr_fun h_7 fstSentIdx + simp [hfstSentIdx] at h_6sent + simp [h_6sent] + have hrdout : rdOut1_1 (fstVldTrue + fstRdyOut) = 1#1 := by + simp [hfstRdyOut] + have hvldout : vldOut1_1 (fstVldTrue + fstRdyOut) = 1#1 := by + have hbefore : ∀ j < fstVldTrue + fstRdyOut, rdOut1_1 j = 0#1 ∨ vldOut1_1 j = 0#1 := by + intro j hj + by_cases hjlt : j < fstVldTrue + · right; by_contra hc + have : vldOut1_1 j = 1#1 := by grind + have := vldOut1_implies_vldIn h_6 (n := j) (by assumption) + specialize hfstVldTrue2 j hjlt + simp [this] at hfstVldTrue2 + · left + have := hfstRdyOut.2 (j - fstVldTrue) (by omega) + rwa [Nat.add_sub_cancel' (by omega)] at this + rw [vldOut_eq_vldIn_of_fork_unitl_sent h_6 hbefore] + obtain ⟨k, hkrd, hkvld, hkall⟩ := h fstVldTrue hfstVldTrue1 + by_contra hlt; push_neg at hlt + have hrda : rdOut1_1 (fstVldTrue + k) = 0#1 := by + have := hfstRdyOut.2 k (by grind) + simpa using this + -- rdIn fires at fstVldTrue + k with k < fstRdyOut, but rdOut1 hasn't fired + have hh5 := h_6 + rw [hw_fork_eq] at h_6 + simp [split_stream2] at h_6 + obtain ⟨hrdin, -⟩ := h_6 + have hcirc := congr_fun hrdin (fstVldTrue + k) + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hcirc + generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) (0, 0#1, 0#1) + (fstVldTrue + k) = s at hcirc + obtain ⟨a, b, c⟩ := s + dsimp [fork_corec, comb_and, comb_xor, comb_or, hw_constant] at hcirc + have ha : a = fstVldTrue + k := by + have := @fork_corec1 rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 0 0#1 0#1 (fstVldTrue + k) + simp [hst] at this + simp [this] + have hb0 : b = 0#1 := by + suffices key : ∀ m, (∀ j < m, rdOut1_1 j = 0#1 ∨ vldOut1_1 j = 0#1) → + (Stream'.iterate (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) + (0, 0#1, 0#1) m).2.1 = 0#1 by + have := key (fstVldTrue + k) (by + intro j hj + by_cases hjlt : j < fstVldTrue + · right; by_contra hc + have : vldOut1_1 j = 1#1 := true_of_width_one (b := vldOut1_1 j) hc + have := vldOut1_implies_vldIn hh5 (n := j) (by assumption) + specialize hfstVldTrue2 j hjlt + simp [this] at hfstVldTrue2 + · have hklt : k < fstRdyOut := by + by_contra hkge; push_neg at hkge + rcases Nat.lt_or_eq_of_le hkge with hlt' | rfl + · exact hlt (hkall fstRdyOut hlt') + · exact hlt hkvld + have hklt : k < fstRdyOut := by + by_contra hkge; push_neg at hkge + exact hlt (hkall fstRdyOut (by omega)) + left + have := hfstRdyOut.2 (j - fstVldTrue) (by omega) + rwa [Nat.add_sub_cancel' (by omega)] at this + ) + rw [hst] at this; simpa using this + intro m; induction m with + | zero => simp [Stream'.iterate] + | succ km ihkm => + intro hbef + have hbk := ihkm (fun j hj => hbef j (Nat.lt_succ_of_lt hj)) + generalize hsk : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) (0, 0#1, 0#1) km = sk + obtain ⟨ak, bk, ck⟩ := sk + simp [hsk] at hbk; subst hbk + have hak : ak = km := by + have := @fork_corec1 rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 0 0#1 0#1 km + simp [hsk] at this; omega + have hvldk : vldOut1_1 km = vldIn_1 ak := by + rw [hw_fork_eq] at hh5; simp [split_stream2] at hh5 + obtain ⟨-, hvldout1, -⟩ := hh5 + have hn := congr_fun hvldout1 km + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + simp_rw [hsk] at hn + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn + simp [hn] + ext k hk + simp [show k = 0 by omega] + have hkbef := hbef km (Nat.lt_succ_self km) + rw [iterate_back_succ, hsk]; simp only [Function.comp] + dsimp [fork_corec, comb_and, comb_xor, comb_or, hw_constant] + subst hak + rcases hkbef with hh | hh + · simp [hh] + · rw [hvldk] at hh; simp [hh] + rw [hkrd, hb0, ha] at hcirc + simp [hrda] at hcirc + simp [hvalidIn, hreadyIn, hrdout, hvldout] + rw [← hdataeq] + let diff := fstSentIdx - fstVldTrue + have hdiff : fstSentIdx = fstVldTrue + diff := by omega + have hdatain : dataIn_1 fstSentIdx = dataIn_1 fstVldTrue := by + rw [hdiff] + have := data_remains_constant_if (i := fstVldTrue) (rdy := rdIn_1) (vld := vldIn_1) (data := dataIn_1) + (by assumption) (by assumption) (by assumption) + obtain ⟨kd, hkd1, hkd2, hkd3, hkd4⟩ := this + by_cases hle : diff ≤ kd + · specialize hkd4 diff hle + apply hkd4 + · /- contra -/ + exfalso + have hkdlt : fstVldTrue + kd < fstSentIdx := by omega + have := hfstSentIdx.2 (fstVldTrue + kd) hkdlt + rw [h_7, toStream] at this + simp [hkd1, hkd2] at this + rw [hdatain] + symm + have := data_remains_constant_until_first (i := fstVldTrue) + (data := dataIn_1) (rdy := rdIn_1) (vld := vldIn_1) (by assumption) + (by assumption) (by assumption) + obtain ⟨k, hk1, hk2, hk3, hk4, hk5⟩ := this + have hkeqdiff : k = diff := by + apply Nat.le_antisymm + · by_contra hlt; push_neg at hlt + -- hlt : diff < k + have := hk5 diff (by omega) + rw [← hdiff] at this + simp [hreadyIn] at this + · by_contra hlt; push_neg at hlt + have := hfstSentIdx.2 (fstVldTrue + k) (by omega) + rw [h_7, toStream] at this + simp [hk1, hk2] at this + subst hkeqdiff + apply hk4 fstRdyOut + -- fstRdyOut ≤ diff, i.e., fstVldTrue + fstRdyOut ≤ fstSentIdx + -- proved by contradiction: if fstSentIdx < fstVldTrue + fstRdyOut, + -- allDone fires but rdOut1 hasn't, contradicting the circuit + have hrdyOutLe : fstVldTrue + fstRdyOut ≤ fstSentIdx := by + by_contra hlt; push_neg at hlt + have hh5 := h_6 + rw [hw_fork_eq] at h_6 + simp [split_stream2] at h_6 + obtain ⟨hrdin, -⟩ := h_6 + have hcirc2 := congr_fun hrdin fstSentIdx + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hcirc2 + generalize hst2 : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) (0, 0#1, 0#1) + fstSentIdx = s2 at hcirc2 + obtain ⟨a2, b2, c2⟩ := s2 + dsimp [fork_corec, comb_and, comb_xor, comb_or, hw_constant] at hcirc2 + have ha2 : a2 = fstSentIdx := by + have := @fork_corec1 rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 0 0#1 0#1 fstSentIdx + simp [hst2] at this; omega + have hb02 : b2 = 0#1 := by + suffices key2 : ∀ m, (∀ j < m, rdOut1_1 j = 0#1 ∨ vldOut1_1 j = 0#1) → + (Stream'.iterate (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) + (0, 0#1, 0#1) m).2.1 = 0#1 by + have := key2 fstSentIdx (by + intro j hj + by_cases hjlt : j < fstVldTrue + · right; by_contra hc + have : vldOut1_1 j = 1#1 := by grind + have := vldOut1_implies_vldIn hh5 (n := j) this + exact absurd (hfstVldTrue2 j hjlt) (by grind) + · left + have := hfstRdyOut.2 (j - fstVldTrue) (by omega) + rwa [Nat.add_sub_cancel' (by omega)] at this) + rw [hst2] at this; simpa using this + intro m; induction m with + | zero => simp [Stream'.iterate] + | succ km ihkm => + intro hbef + have hbk := ihkm (fun j hj => hbef j (Nat.lt_succ_of_lt hj)) + generalize hsk : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) (0, 0#1, 0#1) km = sk + obtain ⟨ak, bk, ck⟩ := sk + simp [hsk] at hbk; subst hbk + have hak : ak = km := by + have := @fork_corec1 rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 0 0#1 0#1 km + simp [hsk] at this; omega + have hvldk2 : vldOut1_1 km = vldIn_1 ak := by + rw [hw_fork_eq] at hh5; simp [split_stream2] at hh5 + obtain ⟨-, hvldout1, -⟩ := hh5 + have hn := congr_fun hvldout1 km + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + simp_rw [hsk] at hn + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn + simp [hn] + ext k + simp [show k = 0 by omega] + rw [iterate_back_succ, hsk]; simp only [Function.comp] + dsimp [fork_corec, comb_and, comb_xor, comb_or, hw_constant] + subst hak + rcases hbef ak (Nat.lt_succ_self ak) with hh | hh + · simp [hh] + · rw [hvldk2] at hh; simp [hh] + have hrda2 : rdOut1_1 fstSentIdx = 0#1 := by + have := hfstRdyOut.2 (fstSentIdx - fstVldTrue) (by omega) + rwa [Nat.add_sub_cancel' (by omega)] at this + rw [hreadyIn, hb02, ha2, hrda2] at hcirc2 + simp at hcirc2 + omega + · /- contradiction: nothing can be sent before `fstSentIdx` -/ + simp_all + intro hcontra + specialize hfstVldTrue2 fstSentIdx hle + simp [toStream, hfstVldTrue2] at hfstSentIdx + · intro i hi + exact hfstSentIdx.2 i hi + · intros j hj + by_cases hj' : j < fstVldTrue + · simp [Stream'.get, h_8, toStream] + intro hvld + have := vldOut1_implies_vldIn h_6 (n := j) + have := hfstVldTrue2 j hj' + grind + · simp [h_8, toStream, Stream'.get] + let diff := j - fstVldTrue + have : j = fstVldTrue + diff := by omega + rw [this] + obtain ⟨h1,h2⟩ := hfstRdyOut + specialize h2 diff (by omega) + intro hc + simp [hc] at h2 + · /- if we never have a valid signal, all streams are empty and the relation holds trivially -/ + have hnonein := not_exists_transmitted_element (x := sin) (data := dataIn_1) (rdy := rdIn_1) + (vld := vldIn_1) (by grind) h_7 + /- the fork module will never transmit anything meaningful -/ + rw [hw_fork_eq] at h_6 + unfold split_stream2 at h_6 + simp at h_6 + have hhfork1 := h_6 + obtain ⟨hrd', hvld1', hvld2', hdata1', hdata2'⟩ := hhfork1 + rw [h_7, h_8] + have hnoneout : ∀ k, vldOut1_1 k = 0#1 := by + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hvld1' + intros k + generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s at hvld1' + simp [fork_corec] at hvld1' + have hk := congr_fun hvld1' k + simp [comb_and, hw_constant] at hk + simp_all + + have : vldIn_1 (Stream'.iterate (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) (0, 0#1, 0#1) k).1 = 0#1 := by + grind + simp [this] + have hnoneout2 : ∀ k, vldOut2_1 k = 0#1 := by + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hvld2' + intros k + generalize hst : Stream'.iterate + (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s at hvld2' + simp [fork_corec] at hvld2' + have hk := congr_fun hvld2' k + simp [comb_and, hw_constant] at hk + simp_all + have : vldIn_1 (Stream'.iterate (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) (0, 0#1, 0#1) k).1 = 0#1 := by + grind + simp [this] + have hnevldin : ∀ k, vldIn_1 k = 0#1 := by grind + have hnonet := not_exists_transmitted_element (x := sout) (data := dataOut1_1) (rdy := rdOut1_1) + (vld := vldOut1_1) (by grind) h_8 + exists 0, 0 + and_intros + · simp + generalize hxgen : Stream'.drop 1 (toStream rdIn_1 vldIn_1 dataIn_1) = y' + generalize hygen : Stream'.drop 1 (toStream rdOut1_1 vldOut1_1 dataOut1_1) = x' + apply relation_fork.intro (x := y') (y := x') + (dataIn := Stream'.drop 1 dataIn_1) + (rdIn := Stream'.drop 1 rdIn_1) + (vldIn := Stream'.drop 1 vldIn_1) + (vldOut1 := Stream'.drop 1 vldOut1_1) + (vldOut2 := Stream'.drop 1 vldOut2_1) + (dataOut1 := Stream'.drop 1 dataOut1_1) + (dataOut2 := Stream'.drop 1 dataOut2_1) + (rdOut1 := Stream'.drop 1 rdOut1_1) + (rdOut2 := Stream'.drop 1 rdOut2_1) + · rw [← hxgen] + rfl + · rw [← hygen] + rfl + · /- contra in hj: there is no i such that vldIn' = 1#1 -/ + unfold globallyValidUntilReady + intros j hj + specialize hnevldin (j + 1) + have : Stream'.drop 1 vldIn_1 j = vldIn_1 (j + 1) := by rfl + simp [this, hnevldin] at hj + · unfold globallyValidUntilReady + intros j hj + apply Classical.byContradiction + simp [Stream'.drop] at hj + have := hnoneout (1 + j) + simp [show vldOut1_1.get (j + 1) = vldOut1_1 (j + 1) by rfl] at hj + simp [Nat.add_comm (n := j), this] at hj + · unfold globallyValidUntilReady + intros j hj + apply Classical.byContradiction + simp [Stream'.drop] at hj + have := hnoneout2 (1 + j) + simp [show vldOut2_1.get (j + 1) = vldOut2_1 (j + 1) by rfl] at hj + simp [Nat.add_comm (n := j), this] at hj + · /- contra in hj: there is no i such that vldIn' = 1#1 -/ + unfold globallyValidAndData + intros j hj + have : Stream'.drop 1 vldIn_1 j = vldIn_1 (j + 1) := by rfl + specialize hnevldin (j + 1) + simp [this, hnevldin] at hj + · /- follows from `hgfrOut1'` -/ + unfold globallyFinallyReady at h_4 ⊢ + intros i + specialize h_4 (i + 1) + obtain ⟨j, hj⟩ := h_4 + exists j + have : Stream'.drop 1 rdOut1_1 (i + j) = rdOut1_1 ((i + j) + 1) := by rfl + rw [this, show i + j + 1 = i + 1 + j by omega, hj] + · unfold globallyFinallyReady at h_5 ⊢ + intros i + specialize h_5 (i + 1) + obtain ⟨j, hj⟩ := h_5 + exists j + have : Stream'.drop 1 rdOut2_1 (i + j) = rdOut2_1 ((i + j) + 1) := by rfl + rw [this, show i + j + 1 = i + 1 + j by omega, hj] + · /- after dropping one element, all the relations defined by the fork module remain. + We see this by unfolding the fork hypotheses -/ + unfold split_stream2 + simp + have h1 := hw_fork'_of_all_none + (dataIn := Stream'.drop 1 dataIn_1) + (vldIn := Stream'.drop 1 vldIn_1) + (rdOut1 := Stream'.drop 1 rdOut1_1) + (rdOut2 := Stream'.drop 1 rdOut2_1) + (by + intro k + specialize hnevldin (k + 1) + simp [show Stream'.drop 1 vldIn_1 k = vldIn_1 (k + 1) by rfl, hnevldin] + ) + have h2 := hw_fork'_of_all_none + (dataIn := dataIn_1) + (vldIn := vldIn_1) + (rdOut1 := rdOut1_1) + (rdOut2 := rdOut2_1) + (by grind) + rw [hw_fork_eq] + simp_all + and_intros + · rfl + · ext l n + have hlhs := hw_fork_out0 + (data_in := dataIn_1) + (vld_in := vldIn_1) + (rd0_in := rdOut1_1) + (rd1_in := rdOut2_1) + (rdy_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).1) + (vld0_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.1) + (vld1_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.1) + (data0_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) + (data1_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) + (by rw [← hw_fork_eq]; simp [split_stream2]) (1 + l) + have hrhs := hw_fork_out0 + (rdy_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).1) + (vld0_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.1) + (vld1_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.1) + (data0_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.1) + (data1_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.2) + (by rw [← hw_fork_eq]; simp [split_stream2]) l + simp [Stream'.drop] at hrhs + have h1 : Stream'.get (fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) (1 + l) = + (fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) (1 + l) := by rfl + simp [h1] + have h2 : (Stream'.get (fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) + (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) + (Stream'.drop 1 dataIn_1) i).2.2.2.1) l) = + (fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) + (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) + (Stream'.drop 1 dataIn_1) i).2.2.2.1) l := by rfl + simp [h2] + simp [← hrhs, ← hlhs] + simp [show dataIn_1.get (l + 1) = dataIn_1 (l + 1) by rfl, Nat.add_comm] + · ext l n + have hlhs := hw_fork_out1 + (data_in := dataIn_1) + (vld_in := vldIn_1) + (rd0_in := rdOut1_1) + (rd1_in := rdOut2_1) + (rdy_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).1) + (vld0_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.1) + (vld1_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.1) + (data0_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) + (data1_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) + (by rw [← hw_fork_eq]; simp [split_stream2]) (1 + l) + have hrhs := hw_fork_out1 + (rdy_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).1) + (vld0_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.1) + (vld1_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.1) + (data0_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.1) + (data1_out := fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.2) + (by rw [← hw_fork_eq]; simp [split_stream2]) l + simp [Stream'.drop] at hrhs + + have h1 : Stream'.get (fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) (1 + l) = + (fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) (1 + l) := by rfl + simp [h1] + have h2 : (Stream'.get (fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) + (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) + (Stream'.drop 1 dataIn_1) i).2.2.2.2) l) = + (fun i => + (hw_fork' (Stream'.drop 1 rdOut1_1) + (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) + (Stream'.drop 1 dataIn_1) i).2.2.2.2) l := by rfl + simp [h2] + simp [← hrhs, ← hlhs] + simp [show dataIn_1.get (l + 1) = dataIn_1 (l + 1) by rfl, Nat.add_comm] + · unfold toStream + congr + have : (fun i => if rdIn_1 i = 1#1 ∧ vldIn_1 i = 1#1 then some (dataIn_1 i) else none) = + fun i => none := by + ext k hk + grind + simp [this] + have : (fun i => if rdOut1_1 i = 1#1 ∧ vldOut1_1 i = 1#1 then some (dataOut1_1 i) else none) = + fun i => none := by + ext k hk + grind + simp [this] + · simp + · simp + · apply relation_fork.intro (toStream rdIn vldIn dataIn) (toStream rdOut1 vldOut1 dataOut1) + (dataOut2 := dataOut2) (vldOut2 := vldOut2) + · rfl + · rfl + · assumption + · assumption + · assumption + · congr + · assumption + · assumption + · assumption + + +theorem hw_fork_refines': + /- Given a handshake fork -/ + (x, y) = TRY2.hw_fork a → + /- we get the output of the corresponding lowered fork -/ + (rdy, vld1, vld2, o1, o2) = split_stream2 (a := BitVec 1) (rtl.fork rd1 rd2 vld data) → + /- if we know that the hshake input stream is bisimilar to the ready-valid input of the hw fork -/ + a ~ (toStream rdy vld data) → + /- We want to make sure that stalling is correctly modeled for `a` (input). + We constrain the input and prove that if the input behaves properly, + the output will. -/ + globallyValidUntilReady vld rdy → + globallyValidAndData vld data → + /- we assume no deadlock -/ + globallyFinallyReady rd1 → + globallyFinallyReady rd2 → + /- we want to prove that the outputs of the handshake fork are respectively + bisimilar to the ready-valid wrapping of the output of the hardware fork -/ + x ~ (toStream rd1 vld1 o1) ∧ y ~ (toStream rd2 vld2 o2) := by + intros handshake_fork hardware_fork inputs_bisim valready_ valdata_a finready1 finready2 + · unfold handshake.fork at handshake_fork + have heq : x = a := by + simp at handshake_fork + exact handshake_fork.1 + have heq' : y = a := by + simp at handshake_fork + exact handshake_fork.2 + rw [heq, heq'] + and_intros + · sorry + · sorry + +end HWComponents From 84d9b446d2bd04e72b9da7c3307f1a35d65f98f9 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 30 Apr 2026 13:58:10 +0100 Subject: [PATCH 4/6] first set of comments --- .../CIRCT/HandshakeToHW/fork_lowering.lean | 354 +++++++++--------- 1 file changed, 167 insertions(+), 187 deletions(-) diff --git a/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean index ca62d028c6..16b3412e5c 100644 --- a/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean +++ b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean @@ -24,7 +24,7 @@ def handshake.fork (in0 : Stream (BitVec 32)) : Stream (BitVec 32) × Stream (Bi (in0, in0) -/- +/-! RTL-level definitions of circuit components -/ def hw_constant (b : Bool) : BitVec 1 := if b then 1#1 else 0#1 @@ -70,7 +70,11 @@ def rtl.fork (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitV ((_12, _3, _9, _rawOutput, _rawOutput), (i + 1, _1, _7)) ) (0, 0#1, 0#1) -def split_stream2 : +/-- + Split a stream containing the product of 5 objects into a product of 5 streams, + each representing a stream of single objects. +-/ +def project_stream : Stream' (a × b × c × d × e) → Stream' a × Stream' b × Stream' c × Stream' d × Stream' e := fun g => (fun i => (g i).1, @@ -79,118 +83,81 @@ def split_stream2 : fun i => (g i).2.2.2.1, fun i => (g i).2.2.2.2) - -/-- At the handshake level: (manual) delayed fork ~ normal fork: the outputs of the fork are bisimilar - for any delay (up to any numbers of `none` inserted, anywhere). -/ -theorem fork_refines {a x y x' y'} : - (x, y) = handshake.fork a → - x ~ x' → - y ~ y' → - x ~ x' ∧ y ~ y' := by grind - -/-- Stream := Stream' (Option α) -/ +/-- + Define the relation between a latency-insensitive `Stream := Stream' (Option α)` + and three concrete `Stream'` (representingready, valid, data signal). +-/ def toStream {α} (rdy : Stream' (BitVec 1)) (vld : Stream' (BitVec 1)) (data : Stream' α) : Stream α := fun i => if rdy i == 1#1 && vld i == 1#1 then .some (data i) else .none -/- the standard implementation of the fork refines the handshake fork (`TRY2.hw_fork`) -/ -/-- weaker def where we do not assume that rdy is by default 0#1 -/ +/-- + For every valid signal at any point in time `vld i = 1#1`, + there is a later point in time `i + k` where the ready signal is true (`rdy (i + k) = 1#1`), + and the valid signal remains constantly true until then. +-/ def globallyValidUntilReady (vld rdy : Stream' (BitVec 1)) : Prop := - ∀ (i : Nat), - (vld i = 1#1) → - ∃ (k : Nat), - rdy (i + k) = 1#1 ∧ vld (i + k) = 1#1 ∧ - ∀ (j : Nat) (_hj : j < k), - vld (i + j) = 1#1 - -/-- This def is stronger than the one above -/ -def globallyValidUntilReady' (vld rdy : Stream' (BitVec 1)) : Prop := - ∀ (i : Nat), - (vld i = 1#1) → - ∃ (k : Nat), - rdy (i + k) = 1#1 ∧ vld (i + k) = 1#1 ∧ - ∀ (j : Nat) (_hj : j < k), - vld (i + j) = 1#1 ∧ rdy (i + j) = 0#1 - -- we should add sth like vld (i + k + 1) = 0#1? + ∀ (i : Nat), (vld i = 1#1) → + ∃ (k : Nat), rdy (i + k) = 1#1 ∧ vld (i + k) = 1#1 ∧ + ∀ (j : Nat) (_hj : j < k), vld (i + j) = 1#1 +/-- + Given a couple of consecutive valid signals (`vld i = 1#1 ∧ vld (i + 1) = 1#1`), + the `data` stream at both points in time remains constant. +-/ def globallyValidAndData (vld : Stream' (BitVec 1)) (data : Stream' (BitVec w)) : Prop := - ∀ (i : Nat), - (vld i = 1#1 ∧ vld (i + 1) = 1#1) → - data i = data (i + 1) - -def relation : Stream (BitVec w) → Stream (BitVec w) → Prop := fun x y => - ∃ (rd1 vld1 : Stream' (BitVec 1)) (data1 : Stream' (BitVec w)) - (rd2 vld2 : Stream' (BitVec 1)) (data2 : Stream' (BitVec w)), - x = toStream rd1 vld1 data1 ∧ - globallyValidUntilReady rd1 vld1 ∧ - globallyValidAndData vld1 data1 ∧ - y = toStream rd2 vld2 data2 ∧ - globallyValidUntilReady rd2 vld2 ∧ - globallyValidAndData vld2 data2 - /- we need to say something about `x` and `y`. -/ - -/-- G(F(val = 1))-/ -def globallyFinallyReady (x : Stream' (BitVec 1)) := - ∀ (i : Nat), - ∃ (k : Nat), - x (i + k) = 1#1 - -inductive relation' : Stream (BitVec w) → Stream (BitVec w) → Prop where - | intro x y rd vld data rd1 vld1 o1 : /- same as `∀ x y` -/ - /- x is the high-level (input), y is the low-level (output) -/ - x = toStream rd vld data → - y = toStream rd1 vld1 o1 → - (∀ j, (rd j = 1#1 ∧ vld j = 1#1) ↔ rd1 j = 1#1 ∧ vld1 j = 1#1) → - -- (∃ k, rd k = 1#1 ∧ vld k = 1) → /- at least one transition happens frfr -/ - globallyValidUntilReady vld rd → - globallyValidAndData vld data → - globallyFinallyReady rd1 → - (∀ n, vld n = 1#1 → data n = o1 n) → /- when the signal is valid, data and output are the same -/ - relation' x y /- defining the type of the relation -/ + ∀ (i : Nat), (vld i = 1#1 ∧ vld (i + 1) = 1#1) → data i = data (i + 1) +/-- + For every point in time `i` of the ready signal, there exists a later (or simultaneous) + point in time `i + k` where the signal is true. +-/ +def globallyFinallyReady (rdy : Stream' (BitVec 1)) := + ∀ (i : Nat), ∃ (k : Nat), rdy (i + k) = 1#1 + +/-- + We propose a bisimilarity relation between latency-insensitive streams at the input and + output of a `fork` circuit. +-/ inductive relation_fork : Stream (BitVec w) → Stream (BitVec w) → Prop where | intro x y rdIn vldIn dataIn rdOut1 vldOut1 dataOut1 rdOut2 vldOut2 dataOut2 : /- same as `∀ x y` -/ - /- x is the high-level (input), y is the low-level (output) -/ + /- *If* x is the input stream, encoded via 3-way-handshake of streams rdIn, vldIn, dataIn -/ x = toStream rdIn vldIn dataIn → + /- *If* y is either of output streams of the fork, + encoded via 3-way-handshake of streams rdOut1, vldOut1, dataOut1 -/ y = toStream rdOut1 vldOut1 dataOut1 → - /- if a signal in `x` is valid (`vldIn i = 1#1`), it will remain valid (at least) until a - ready signal is received (`rdIn (i + k) = 1#1`). A ready signal is eventually definitely received. -/ + /- *If* when a signal in `x` is valid (`vldIn i = 1#1`), it will remain valid (at least) until a + ready signal is received (`rdIn (i + k) = 1#1`). + A ready signal is eventually definitely received. -/ globallyValidUntilReady vldIn rdIn → + /- *If* when a signal in `y` is valid (`vldOut1 i = 1#1`), it will remain valid (at least) until a + ready signal is received (`rdOut1 (i + k) = 1#1`). + A ready signal is eventually definitely received. -/ globallyValidUntilReady vldOut1 rdOut1 → + /- *If* when a signal in `y` is valid (`vldOut2 i = 1#1`), it will remain valid (at least) until a + ready signal is received (`rdOut2 (i + k) = 1#1`). + A ready signal is eventually definitely received. -/ globallyValidUntilReady vldOut2 rdOut2 → - /- if a signal in `x` is valid for more than one cycle (`vldIn i = 1#1 ∧ vldIn (i + 1) = 1#1`), - the data does not change (`dataIn i = dataIn (i + 1)`) -/ + /- *If* when a signal in `x` is valid for more than one cycle (`vldIn i = 1#1 ∧ vldIn (i + 1) = 1#1`), + the data stream at those points in time remains constant (`dataIn i = dataIn (i + 1)`). -/ globallyValidAndData vldIn dataIn → - /- eventually a ready signal arrives from both receivers (`rdOut1 i = 1#1`), (`rdOut2 i = 1#1`) -/ + /- *If* eventually, + a ready signal arrives from both receivers (`rdOut1 i = 1#1`), (`rdOut2 i = 1#1`). -/ globallyFinallyReady rdOut1 → globallyFinallyReady rdOut2 → - /- input/output relationship around the `fork` module -/ - - (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn) → + /- *If* the relations between the input and output ready, valid, data signals + are given by the `rtl.fork` component. -/ + (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn) → + /- The relation holds. -/ relation_fork x y -/- - our implementation of `fork` should not allow this, assuming that the input is - well-formed (including its ready signals!). - - val1 = 1 1 1 - data1 = 2 3 4 - rd1 = 1 1 1 - out1: 2 3 4 - - val2 = 1 1 1 - data2 = 2 3 4 - rd2 = 0 1 1 - out2: - 3 4 - +/-- + Define the unfolding of one step of the corecursive definition of `fork`. -/ - - -/-- We unfold one step of the corecursive definition of `fork` -/ def fork_corec (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec 32)) := fun (i, _emitted_0, _emitted_1) => let _true := hw_constant true @@ -211,8 +178,10 @@ def fork_corec (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (Bi let _7 := comb_and _11 _6 ((_12, _3, _9, _rawOutput, _rawOutput), (i+1, _1, _7)) -/-- We re-define the fork circuit in terms of `fork_corec` -/ -def hw_fork' (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec 32)) +/-- + Define the fork circuit in terms of `fork_corec`. +-/ +def rtl.fork' (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec 32)) : Stream' ( BitVec 1 -- ready (_12) × BitVec 1 -- valid_0 (_3) × BitVec 1 -- valid_1 (_9) @@ -221,11 +190,11 @@ def hw_fork' (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitV ) := Stream'.corec' (α := Nat × BitVec 1 × BitVec 1) (fork_corec _ready _ready_1 _valid _in0) (0, 0#1, 0#1) - - - -/-- Prove that iterating `n` times starting from the `m`-th index of the stream yields the `n + m`-th index-/ -theorem fork_corec1 : +/-- + Prove that iterating `n` times starting from the `m`-th index of the stream + yields the `n + m`-th index. +-/ +theorem fork_corec_iter : (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (m, x, y) n).1 = n + m := by induction n generalizing m x y with | zero => grind [Stream'.iterate] @@ -235,9 +204,13 @@ theorem fork_corec1 : dsimp [fork_corec] grind -theorem hw_fork'_vldOut1_of_none (h : ∀ k, vldIn k = 0#1) : - ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).2.1 = 0#1 := by - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get +/-- + If the valid input stream is false at all points in time (`vldIn k = 0#1`), + the first valid output stream of the fork component is also false at all times. +-/ +theorem fork'_vldOut1_of_none (h : ∀ k, vldIn k = 0#1) : + ((rtl.fork' rdOut1 rdOut2 vldIn dataIn) k).2.1 = 0#1 := by + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get generalize hst : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s obtain ⟨a, b, c⟩ := s @@ -245,9 +218,13 @@ theorem hw_fork'_vldOut1_of_none (h : ∀ k, vldIn k = 0#1) : specialize h a simp [h] -theorem hw_fork'_vldOut2_of_none (h : ∀ k, vldIn k = 0#1) : - ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).2.2.1 = 0#1 := by - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get +/-- + If the valid input stream is false at all points in time (`vldIn k = 0#1`), + the second valid output stream of the fork component is also false at all times. +-/ +theorem fork'_vldOut2_of_none (h : ∀ k, vldIn k = 0#1) : + ((rtl.fork' rdOut1 rdOut2 vldIn dataIn) k).2.2.1 = 0#1 := by + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get generalize hst : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s obtain ⟨a, b, c⟩ := s @@ -255,6 +232,9 @@ theorem hw_fork'_vldOut2_of_none (h : ∀ k, vldIn k = 0#1) : specialize h a simp [h] +/-- + Applying a function `f` to +-/ lemma iterate_back_succ (f : α → α) (s : α) (n : ℕ) : Stream'.iterate f s (n + 1) = f (Stream'.iterate f s n) := by induction n generalizing s with @@ -279,11 +259,11 @@ lemma fork_emitted_zero_of_all_none (h : ∀ k, vldIn k = 0#1) : simp [h a] -- when vld is always 0, all signal outputs (not data) are 0 -theorem hw_fork'_of_all_none (h : ∀ k, vldIn k = 0#1) : - ∀ k, ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).1 = 0#1 ∧ - ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).2.1 = 0#1 ∧ - ((hw_fork' rdOut1 rdOut2 vldIn dataIn) k).2.2.1 = 0#1 := by - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get +theorem rtl.fork'_of_all_none (h : ∀ k, vldIn k = 0#1) : + ∀ k, ((rtl.fork' rdOut1 rdOut2 vldIn dataIn) k).1 = 0#1 ∧ + ((rtl.fork' rdOut1 rdOut2 vldIn dataIn) k).2.1 = 0#1 ∧ + ((rtl.fork' rdOut1 rdOut2 vldIn dataIn) k).2.2.1 = 0#1 := by + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get intro k and_intros · generalize hst : Stream'.iterate @@ -310,15 +290,15 @@ theorem hw_fork'_of_all_none (h : ∀ k, vldIn k = 0#1) : simp [h] /-- Prove that (at RTL level) the input and output data at the `n`-th position are the same. - This is possible because `hw_fork'` does not introduce any delay, and there is no transformation + This is possible because `rtl.fork'` does not introduce any delay, and there is no transformation happening on the data. -/ theorem hw_fork_out0 - (h : ⟨rdy_out, vld0_out, vld1_out, data0_out, data1_out⟩ = split_stream2 (hw_fork' rd0_in rd1_in vld_in data_in)) : + (h : ⟨rdy_out, vld0_out, vld1_out, data0_out, data1_out⟩ = project_stream (rtl.fork' rd0_in rd1_in vld_in data_in)) : (∀ n, data_in n = data0_out n) := by intro n - simp [split_stream2] at h + simp [project_stream] at h simp [h] - unfold hw_fork'; clear h + unfold rtl.fork'; clear h unfold Stream'.corec' Stream'.corec Stream'.map Stream'.get generalize h: (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (0, 0#1, 0#1) n) = y obtain ⟨a, b, c⟩ := y @@ -327,12 +307,12 @@ theorem hw_fork_out0 theorem hw_fork_out1 (h : ⟨rdy_out, vld0_out, vld1_out, data0_out, data1_out⟩ = - split_stream2 (hw_fork' rd0_in rd1_in vld_in data_in)) : + project_stream (rtl.fork' rd0_in rd1_in vld_in data_in)) : (∀ n, data_in n = data1_out n) := by intro n - simp [split_stream2] at h + simp [project_stream] at h simp [h] - unfold hw_fork'; clear h + unfold rtl.fork'; clear h unfold Stream'.corec' Stream'.corec Stream'.map Stream'.get generalize h: (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (0, 0#1, 0#1) n) = y obtain ⟨a, b, c⟩ := y @@ -352,20 +332,20 @@ theorem fork_corec1bis : dsimp [fork_corec] grind -theorem hw_fork_eq : rtl.fork rd0 rd1 vld data = hw_fork' rd0 rd1 vld data := by - unfold rtl.fork hw_fork' +theorem hw_fork_eq : rtl.fork rd0 rd1 vld data = rtl.fork' rd0 rd1 vld data := by + unfold rtl.fork rtl.fork' congr 1 theorem vldOut1_implies_vldIn (h : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hvld : vldOut1 n = 1#1) : vldIn n = 1#1 := by rw [hw_fork_eq] at h - simp [split_stream2] at h + simp [project_stream] at h obtain ⟨-, hvldout1, -⟩ := h have hn := congr_fun hvldout1 n rw [hvld] at hn - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn generalize hst : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) n = s at hn obtain ⟨a, b, c⟩ := s @@ -383,14 +363,14 @@ theorem vldOut1_implies_vldIn theorem vldOut2_implies_vldIn (h : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hvld : vldOut2 n = 1#1) : vldIn n = 1#1 := by rw [hw_fork_eq] at h - simp [split_stream2] at h + simp [project_stream] at h obtain ⟨-, -, hvldout2, -⟩ := h have hn := congr_fun hvldout2 n rw [hvld] at hn - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn generalize hst : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) n = s at hn obtain ⟨a, b, c⟩ := s @@ -408,7 +388,7 @@ theorem vldOut2_implies_vldIn theorem rdOut1_before_allDone (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hvldOut1 : vldOut1 n = 1#1) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hvldOut1 : vldOut1 n = 1#1) (hgvurIn : globallyValidUntilReady vldIn rdIn) : ∃ k, rdIn (n + k) = 1#1 ∧ vldIn (n + k) = 1#1 := by have hvldIn := vldOut1_implies_vldIn hfork hvldOut1 @@ -430,15 +410,15 @@ lemma iterate_succ_apply (f : α → α) (s : α) (n : ℕ) : theorem vldOut_eq_vldIn_of_fork_unitl_sent (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) /- nothing is emitted before `n`, as emission occurs if `rdOut1 j ∧ vldOut1 j` -/ (hbefore : ∀ j < n, rdOut1 j = 0#1 ∨ vldOut1 j = 0#1) : vldOut1 n = vldIn n := by rw [hw_fork_eq] at hfork - simp [split_stream2] at hfork + simp [project_stream] at hfork obtain ⟨-, hvldout1, -⟩ := hfork have hn := congr_fun hvldout1 n - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn generalize hst : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) n = s at hn obtain ⟨a, b, c⟩ := s @@ -472,7 +452,7 @@ theorem vldOut_eq_vldIn_of_fork_unitl_sent simp only [Function.comp] have hvldk : vldOut1 k = vldIn ak := by have h := congr_fun hvldout1 k - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at h + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at h simp_rw [hsk] at h dsimp [fork_corec, comb_and, comb_xor, hw_constant] at h simp_all @@ -527,7 +507,7 @@ theorem vldOut_eq_vldIn_of_fork_unitl_sent theorem vldOut_of_vldIn_rdy (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) /- nothing has been accepted so far -/ (hbefore : ∀ l < j, rdOut1 l = 0#1 ∨ vldOut1 l = 0#1) (hin : vldIn j = 1#1 ∧ rdIn j = 1#1) : @@ -537,15 +517,15 @@ theorem vldOut_of_vldIn_rdy theorem vldOut_eq_vldIn_of_fork_unitl_sent2 (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) /- nothing is emitted before `n`, as emission occurs if `rdOut1 j ∧ vldOut1 j` -/ (hbefore : ∀ j < n, rdOut2 j = 0#1 ∨ vldOut2 j = 0#1) : vldOut2 n = vldIn n := by rw [hw_fork_eq] at hfork - simp [split_stream2] at hfork + simp [project_stream] at hfork obtain ⟨-, -, hvldout2, -⟩ := hfork have hn := congr_fun hvldout2 n - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn generalize hst : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) n = s at hn obtain ⟨a, b, c⟩ := s @@ -571,7 +551,7 @@ theorem vldOut_eq_vldIn_of_fork_unitl_sent2 grind have hvldk : vldOut2 k = vldIn ak := by have h := congr_fun hvldout2 k - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at h + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at h simp_rw [hsk] at h dsimp [fork_corec, comb_and, comb_xor, hw_constant] at h simp_all @@ -763,7 +743,7 @@ theorem true_of_width_one (b : BitVec 1) (h : ¬ b = 0#1 ) : b = 1#1 := by grind theorem vldIn_and_eventually_ready_implies_vldOut1 (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hvldIn : globallyFinallyReady vldIn) : ∃ k, vldOut1 k = 1#1 := by obtain ⟨n, hvldn, hnmin⟩ := if_exists_first_exists (hvldIn 0 |>.imp (fun k hk => by simpa using hk)) @@ -779,7 +759,7 @@ theorem vldIn_and_eventually_ready_implies_vldOut1 theorem vldIn_and_ready_implies_vldOut1 (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hvldIn : ∃ j, vldIn j = 1#1) : ∃ k, vldOut1 k = 1#1 := by obtain ⟨n, hvldn, hnmin⟩ := if_exists_first_exists (st := vldIn) (by grind) @@ -795,7 +775,7 @@ theorem vldIn_and_ready_implies_vldOut1 theorem vldIn_and_ready_implies_vldOut2 (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hvldIn : ∃ j, vldIn j = 1#1) : ∃ k, vldOut2 k = 1#1 := by obtain ⟨n, hvldn, hnmin⟩ := if_exists_first_exists (st := vldIn) (by grind) @@ -811,7 +791,7 @@ theorem vldIn_and_ready_implies_vldOut2 lemma fork_globallyValidAndData_out1 (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = - split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hgv : globallyValidAndData vldIn dataIn) : globallyValidAndData vldOut1 dataOut1 := by intro i ⟨hi1, hi2⟩ @@ -890,7 +870,7 @@ def readyOut2UntilAllReceiversAre (rdOut1 rdOut2 : Stream' (BitVec 1)) := theorem hw_fork_refines1_with_fork: /- Given a handshake fork taking `a` as input and returning `(a, a)`, we take its lowering (with input a bisimilar ready-valid wrapped stream) -/ - (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = split_stream2 (rtl.fork rdOut1 rdOut2 vldIn dataIn) → + (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn) → /- We want to make sure that stalling is correctly modeled for `a` (input). We constrain the input and prove that if the input behaves properly, the output will. -/ @@ -1075,7 +1055,7 @@ theorem hw_fork_refines1_with_fork: · /- first receiver before sent -/ by_cases sndRecBeforeSent : fstVldTrue + fstRdyOut2 ≤ fstSentIdx · /- second receiver before sent -/ - simp [split_stream2] + simp [project_stream] and_intros · funext i have := rdOut1_before_allDone (hfork := h_6) (n := i) @@ -1094,7 +1074,7 @@ theorem hw_fork_refines1_with_fork: 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'] + simp [rtl.fork', Stream'.corec'] unfold fork_corec simp [comb_and, comb_xor, comb_or, hw_constant] @@ -1156,10 +1136,10 @@ theorem hw_fork_refines1_with_fork: -- rdIn fires at fstVldTrue + k with k < fstRdyOut, but rdOut1 hasn't fired have hh5 := h_6 rw [hw_fork_eq] at h_6 - simp [split_stream2] at h_6 + simp [project_stream] at h_6 obtain ⟨hrdin, -⟩ := h_6 have hcirc := congr_fun hrdin (fstVldTrue + k) - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hcirc + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hcirc generalize hst : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) (0, 0#1, 0#1) (fstVldTrue + k) = s at hcirc @@ -1207,10 +1187,10 @@ theorem hw_fork_refines1_with_fork: have := @fork_corec1 rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 0 0#1 0#1 km simp [hsk] at this; omega have hvldk : vldOut1_1 km = vldIn_1 ak := by - rw [hw_fork_eq] at hh5; simp [split_stream2] at hh5 + rw [hw_fork_eq] at hh5; simp [project_stream] at hh5 obtain ⟨-, hvldout1, -⟩ := hh5 have hn := congr_fun hvldout1 km - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn simp_rw [hsk] at hn dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn simp [hn] @@ -1269,10 +1249,10 @@ theorem hw_fork_refines1_with_fork: by_contra hlt; push_neg at hlt have hh5 := h_6 rw [hw_fork_eq] at h_6 - simp [split_stream2] at h_6 + simp [project_stream] at h_6 obtain ⟨hrdin, -⟩ := h_6 have hcirc2 := congr_fun hrdin fstSentIdx - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hcirc2 + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hcirc2 generalize hst2 : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1_1 rdOut2_1 vldIn_1 dataIn_1) (0, 0#1, 0#1) fstSentIdx = s2 at hcirc2 @@ -1309,10 +1289,10 @@ theorem hw_fork_refines1_with_fork: have := @fork_corec1 rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 0 0#1 0#1 km simp [hsk] at this; omega have hvldk2 : vldOut1_1 km = vldIn_1 ak := by - rw [hw_fork_eq] at hh5; simp [split_stream2] at hh5 + rw [hw_fork_eq] at hh5; simp [project_stream] at hh5 obtain ⟨-, hvldout1, -⟩ := hh5 have hn := congr_fun hvldout1 km - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hn simp_rw [hsk] at hn dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn simp [hn] @@ -1357,13 +1337,13 @@ theorem hw_fork_refines1_with_fork: (vld := vldIn_1) (by grind) h_7 /- the fork module will never transmit anything meaningful -/ rw [hw_fork_eq] at h_6 - unfold split_stream2 at h_6 + unfold project_stream at h_6 simp at h_6 have hhfork1 := h_6 obtain ⟨hrd', hvld1', hvld2', hdata1', hdata2'⟩ := hhfork1 rw [h_7, h_8] have hnoneout : ∀ k, vldOut1_1 k = 0#1 := by - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hvld1' + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hvld1' intros k generalize hst : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s at hvld1' @@ -1376,7 +1356,7 @@ theorem hw_fork_refines1_with_fork: grind simp [this] have hnoneout2 : ∀ k, vldOut2_1 k = 0#1 := by - unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hvld2' + unfold rtl.fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get at hvld2' intros k generalize hst : Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) (0, 0#1, 0#1) k = s at hvld2' @@ -1452,9 +1432,9 @@ theorem hw_fork_refines1_with_fork: rw [this, show i + j + 1 = i + 1 + j by omega, hj] · /- after dropping one element, all the relations defined by the fork module remain. We see this by unfolding the fork hypotheses -/ - unfold split_stream2 + unfold project_stream simp - have h1 := hw_fork'_of_all_none + have h1 := rtl.fork'_of_all_none (dataIn := Stream'.drop 1 dataIn_1) (vldIn := Stream'.drop 1 vldIn_1) (rdOut1 := Stream'.drop 1 rdOut1_1) @@ -1464,7 +1444,7 @@ theorem hw_fork_refines1_with_fork: specialize hnevldin (k + 1) simp [show Stream'.drop 1 vldIn_1 k = vldIn_1 (k + 1) by rfl, hnevldin] ) - have h2 := hw_fork'_of_all_none + have h2 := rtl.fork'_of_all_none (dataIn := dataIn_1) (vldIn := vldIn_1) (rdOut1 := rdOut1_1) @@ -1480,34 +1460,34 @@ theorem hw_fork_refines1_with_fork: (vld_in := vldIn_1) (rd0_in := rdOut1_1) (rd1_in := rdOut2_1) - (rdy_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).1) - (vld0_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.1) - (vld1_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.1) - (data0_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) - (data1_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) - (by rw [← hw_fork_eq]; simp [split_stream2]) (1 + l) + (rdy_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).1) + (vld0_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.1) + (vld1_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.1) + (data0_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) + (data1_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) + (by rw [← hw_fork_eq]; simp [project_stream]) (1 + l) have hrhs := hw_fork_out0 (rdy_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).1) (vld0_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.1) (vld1_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.1) (data0_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.1) (data1_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.2) - (by rw [← hw_fork_eq]; simp [split_stream2]) l + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.2) + (by rw [← hw_fork_eq]; simp [project_stream]) l simp [Stream'.drop] at hrhs - have h1 : Stream'.get (fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) (1 + l) = - (fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) (1 + l) := by rfl + have h1 : Stream'.get (fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) (1 + l) = + (fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) (1 + l) := by rfl simp [h1] have h2 : (Stream'.get (fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.1) l) = (fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.1) l := by rfl simp [h2] @@ -1519,35 +1499,35 @@ theorem hw_fork_refines1_with_fork: (vld_in := vldIn_1) (rd0_in := rdOut1_1) (rd1_in := rdOut2_1) - (rdy_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).1) - (vld0_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.1) - (vld1_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.1) - (data0_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) - (data1_out := fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) - (by rw [← hw_fork_eq]; simp [split_stream2]) (1 + l) + (rdy_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).1) + (vld0_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.1) + (vld1_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.1) + (data0_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.1) + (data1_out := fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) + (by rw [← hw_fork_eq]; simp [project_stream]) (1 + l) have hrhs := hw_fork_out1 (rdy_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).1) (vld0_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.1) (vld1_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.1) (data0_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.1) (data1_out := fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.2) - (by rw [← hw_fork_eq]; simp [split_stream2]) l + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.2) + (by rw [← hw_fork_eq]; simp [project_stream]) l simp [Stream'.drop] at hrhs - have h1 : Stream'.get (fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) (1 + l) = - (fun i => (hw_fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) (1 + l) := by rfl + have h1 : Stream'.get (fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) (1 + l) = + (fun i => (rtl.fork' rdOut1_1 rdOut2_1 vldIn_1 dataIn_1 i).2.2.2.2) (1 + l) := by rfl simp [h1] have h2 : (Stream'.get (fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.2) l) = (fun i => - (hw_fork' (Stream'.drop 1 rdOut1_1) + (rtl.fork' (Stream'.drop 1 rdOut1_1) (Stream'.drop 1 rdOut2_1) (Stream'.drop 1 vldIn_1) (Stream'.drop 1 dataIn_1) i).2.2.2.2) l := by rfl simp [h2] @@ -1582,9 +1562,9 @@ theorem hw_fork_refines1_with_fork: theorem hw_fork_refines': /- Given a handshake fork -/ - (x, y) = TRY2.hw_fork a → + (x, y) = handshake.fork a → /- we get the output of the corresponding lowered fork -/ - (rdy, vld1, vld2, o1, o2) = split_stream2 (a := BitVec 1) (rtl.fork rd1 rd2 vld data) → + (rdy, vld1, vld2, o1, o2) = project_stream (a := BitVec 1) (rtl.fork rd1 rd2 vld data) → /- if we know that the hshake input stream is bisimilar to the ready-valid input of the hw fork -/ a ~ (toStream rdy vld data) → /- We want to make sure that stalling is correctly modeled for `a` (input). From 1deafa746906b66d0b557230c498873afb294f1e Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 30 Apr 2026 14:07:25 +0100 Subject: [PATCH 5/6] wip --- .../CIRCT/HandshakeToHW/fork_lowering.lean | 64 +++++++++++-------- 1 file changed, 38 insertions(+), 26 deletions(-) diff --git a/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean index 16b3412e5c..93a757cc12 100644 --- a/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean +++ b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean @@ -233,7 +233,7 @@ theorem fork'_vldOut2_of_none (h : ∀ k, vldIn k = 0#1) : simp [h] /-- - Applying a function `f` to + TODO: Luisa does not understand what the gist of this lemma is. -/ lemma iterate_back_succ (f : α → α) (s : α) (n : ℕ) : Stream'.iterate f s (n + 1) = f (Stream'.iterate f s n) := by @@ -241,8 +241,11 @@ lemma iterate_back_succ (f : α → α) (s : α) (n : ℕ) : | zero => simp [Stream'.iterate_eq, Stream'.cons] | succ k ih => rw [Stream'.iterate_eq, Stream'.cons, ih]; rfl +/-- + TODO: Luisa does not understand what the gist of this lemma is. +-/ lemma fork_emitted_zero_of_all_none (h : ∀ k, vldIn k = 0#1) : - ∀ k, (Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) + ∀ k, (Stream'.iterate (Prod.snd ∘ (fork_corec rdOut1 rdOut2 vldIn dataIn)) (0, 0#1, 0#1) k).2 = (0#1, 0#1) := by intro k induction k with @@ -258,8 +261,12 @@ lemma fork_emitted_zero_of_all_none (h : ∀ k, vldIn k = 0#1) : dsimp [fork_corec, comb_and, comb_xor, comb_or, hw_constant] simp [h a] --- when vld is always 0, all signal outputs (not data) are 0 -theorem rtl.fork'_of_all_none (h : ∀ k, vldIn k = 0#1) : +/-- + If the input's valid signal is always false, + for every point in time `k` the ready signal of the input and valid signals of the outputs of + a fork circuit are false as well. +-/ +theorem fork'_of_all_none (h : ∀ k, vldIn k = 0#1) : ∀ k, ((rtl.fork' rdOut1 rdOut2 vldIn dataIn) k).1 = 0#1 ∧ ((rtl.fork' rdOut1 rdOut2 vldIn dataIn) k).2.1 = 0#1 ∧ ((rtl.fork' rdOut1 rdOut2 vldIn dataIn) k).2.2.1 = 0#1 := by @@ -289,10 +296,12 @@ theorem rtl.fork'_of_all_none (h : ∀ k, vldIn k = 0#1) : specialize h a simp [h] -/-- Prove that (at RTL level) the input and output data at the `n`-th position are the same. - This is possible because `rtl.fork'` does not introduce any delay, and there is no transformation - happening on the data. -/ -theorem hw_fork_out0 +/-- + We prove that, at RTL level, the input and first output data stream at the `n`-th position are the same. + This is possible because `rtl.fork'` does not introduce any delay nor buffering, + and there is no transformation happening on the data. +-/ +theorem fork_dataIn_eq_dataOut1 (h : ⟨rdy_out, vld0_out, vld1_out, data0_out, data1_out⟩ = project_stream (rtl.fork' rd0_in rd1_in vld_in data_in)) : (∀ n, data_in n = data0_out n) := by intro n @@ -303,9 +312,14 @@ theorem hw_fork_out0 generalize h: (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (0, 0#1, 0#1) n) = y obtain ⟨a, b, c⟩ := y dsimp [fork_corec] - rw [show a = (a, b, c).1 by rfl, ←h, fork_corec1]; rfl + rw [show a = (a, b, c).1 by rfl, ← h, fork_corec_iter]; rfl -theorem hw_fork_out1 +/-- + We prove that, at RTL level, the input and second output data stream at the `n`-th position are the same. + This is possible because `rtl.fork'` does not introduce any delay nor buffering, + and there is no transformation happening on the data. +-/ +theorem fork_dataIn_eq_dataOut2 (h : ⟨rdy_out, vld0_out, vld1_out, data0_out, data1_out⟩ = project_stream (rtl.fork' rd0_in rd1_in vld_in data_in)) : (∀ n, data_in n = data1_out n) := by @@ -317,25 +331,19 @@ theorem hw_fork_out1 generalize h: (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (0, 0#1, 0#1) n) = y obtain ⟨a, b, c⟩ := y dsimp [fork_corec] - rw [show a = (a, b, c).1 by rfl, ←h, fork_corec1]; rfl - - - - -theorem fork_corec1bis : - (Stream'.iterate (Prod.snd ∘ fork_corec rd0_in rd1_in vld_in data_in) (m, x, y) n).1 = n + m := by - induction n generalizing m x y with - | zero => grind [Stream'.iterate] - | succ x h => - rw [Stream'.iterate_eq] - dsimp [Stream'.cons] - dsimp [fork_corec] - grind + rw [show a = (a, b, c).1 by rfl, ← h, fork_corec_iter]; rfl +/-- + Prove the equivalence of the two definitions of `rtl.fork`. +-/ theorem hw_fork_eq : rtl.fork rd0 rd1 vld data = rtl.fork' rd0 rd1 vld data := by unfold rtl.fork rtl.fork' congr 1 +/-- + If at a certain point in time `n` the first output valid signal is true, + then the input valid signal at that point in time is also true. +-/ theorem vldOut1_implies_vldIn (h : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) @@ -351,7 +359,7 @@ theorem vldOut1_implies_vldIn obtain ⟨a, b, c⟩ := s dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn have heq : a = n := by - have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n + have := @fork_corec_iter rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n rw [hst] at this simp at this assumption @@ -361,6 +369,10 @@ theorem vldOut1_implies_vldIn have : vldIn a = 0#1 := by grind simp [this] at hn +/-- + If at a certain point in time `n` the second output valid signal is true, + then the input valid signal at that point in time is also true. +-/ theorem vldOut2_implies_vldIn (h : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) @@ -376,7 +388,7 @@ theorem vldOut2_implies_vldIn obtain ⟨a, b, c⟩ := s dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn have heq : a = n := by - have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n + have := @fork_corec_iter rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n rw [hst] at this simp at this assumption From a47417b5e6ac04b67f68c4dcc7054ceb6169a15e Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Thu, 30 Apr 2026 18:18:32 +0100 Subject: [PATCH 6/6] more polishing --- .../CIRCT/HandshakeToHW/fork_lowering.lean | 23 +++++++++---------- 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean index 93a757cc12..8eeaa79fba 100644 --- a/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean +++ b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean @@ -398,6 +398,11 @@ theorem vldOut2_implies_vldIn have : vldIn a = 0#1 := by grind simp [this] at hn +/-- + In a fork component with no-deadlock guarantees, there always exists a point in time + when both the ready and the valid input signals are true, and therefore a valid input + data signal arrives. +-/ theorem rdOut1_before_allDone (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) (hvldOut1 : vldOut1 n = 1#1) @@ -410,16 +415,10 @@ theorem rdOut1_before_allDone exists k simp [hk] -lemma iterate_succ_apply (f : α → α) (s : α) (n : ℕ) : - Stream'.iterate f s (n + 1) = f (Stream'.iterate f s n) := by - induction n generalizing s with - | zero => simp [Stream'.iterate] - | succ k ih => - rw [Stream'.iterate_eq, Stream'.cons] - exact ih _ - - - +/-- + In a fork circuit, at all points in time that come before the first element is transmitted, + the input and output valid signal have the same value. +-/ theorem vldOut_eq_vldIn_of_fork_unitl_sent (hfork : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) @@ -458,7 +457,7 @@ theorem vldOut_eq_vldIn_of_fork_unitl_sent simp [hsk] at hbk; subst hbk rw [iterate_back_succ, hsk] have hak : ak = k := by - have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 k + have := @fork_corec_iter rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 k simp [hsk] at this; omega have hk := hbef k (Nat.lt_succ_self k) simp only [Function.comp] @@ -508,7 +507,7 @@ theorem vldOut_eq_vldIn_of_fork_unitl_sent simp [h1] simp [hb] at hn have heq : a = n := by - have := @fork_corec1 rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n + have := @fork_corec_iter rdOut1 rdOut2 vldIn dataIn 0 0#1 0#1 n rw [hst] at this simp at this assumption