diff --git a/SSA/Projects/CIRCT/Handshake/Handshake.lean b/SSA/Projects/CIRCT/Handshake/Handshake.lean index bf0aaf0716..6b3409cd7b 100644 --- a/SSA/Projects/CIRCT/Handshake/Handshake.lean +++ b/SSA/Projects/CIRCT/Handshake/Handshake.lean @@ -120,6 +120,26 @@ def fork (x : Stream α) : Stream α × Stream α := let x' := x.tail (x0, x0, x') +/-- The handshake fork duplicates its input stream: both outputs are `x` +itself. (Its `corec_prod` emits the current head twice and advances by +`tail`, so the corec state after `n` steps is `x.drop n` and the output at +position `n` is `x n` on both sides.) -/ +theorem fork_eq (x : Stream α) : fork x = (x, x) := by + have hiter : ∀ (n : Nat), + Stream'.iterate Stream'.tail x n = Stream'.drop n x := by + intro n + induction n with + | zero => rfl + | succ k ih => + show Stream'.tail (Stream'.iterate Stream'.tail x k) = _ + rw [ih] + exact Stream'.tail_drop' + refine Prod.ext ?_ ?_ <;> funext n <;> + · show ((Stream'.iterate Stream'.tail x n) 0 : Option α) = x n + rw [hiter] + show x.get (0 + n) = x.get n + rw [Nat.zero_add] + -- not entirely nondeterministic (still picks left first) def controlMerge (x y : Stream α) : Stream α × Stream (BitVec 1) := corec_prod (β := Stream α × Stream α) (x, y) fun ⟨x, y⟩ => diff --git a/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean b/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean index db58a4c633..7134a46442 100644 --- a/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean +++ b/SSA/Projects/CIRCT/HandshakeToHW/HWFork.lean @@ -7,18 +7,28 @@ 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 +-/ +@[bv_normalize, grind] +def hw_constant (b : Bool) : BitVec 1 := if b then 1#1 else 0#1 + +@[bv_normalize, grind] +def comb_xor (x y : BitVec 1) : BitVec 1 := BitVec.xor x y + +@[bv_normalize, grind] +def comb_and (x y : BitVec 1) : BitVec 1 := BitVec.and x y + +@[bv_normalize, grind] +def comb_add (x y : BitVec w) : BitVec w := BitVec.add x y -def comb_xor : BitVec 1 → BitVec 1 → BitVec 1 := BitVec.xor -def comb_and : BitVec 1 → BitVec 1 → BitVec 1 := BitVec.and -def comb_add : BitVec 32 → BitVec 32 → BitVec 32 := BitVec.add -def comb_or : BitVec 1 → BitVec 1 → BitVec 1 := BitVec.or +@[bv_normalize, grind] +def comb_or (x y : BitVec 1) : BitVec 1 := BitVec.or x y namespace TRY1 -axiom esi_unwrap_vr : Stream (BitVec 32) → BitVec 1 → Stream (BitVec 32) × BitVec 1 -axiom esi_wrap_vr : Stream (BitVec 32) → BitVec 1 → Stream (BitVec 32) × BitVec 1 +axiom esi_unwrap_vr : Stream (BitVec w) → BitVec 1 → Stream (BitVec w) × BitVec 1 +axiom esi_wrap_vr : Stream (BitVec w) → BitVec 1 → Stream (BitVec w) × BitVec 1 /- This first implementation with all the "correct" types does not work because of the feedback between ready, valid and @@ -28,7 +38,7 @@ axiom esi_wrap_vr : Stream (BitVec 32) → BitVec 1 → Stream (BitVec 32) × Bi -/ #guard_msgs (drop error) in -def hw_fork_fails (_in0 : Stream (BitVec 32)) : Stream (BitVec 32) × Stream (BitVec 32) := +def hw_fork_fails (_in0 : Stream (BitVec w)) : Stream (BitVec w) × Stream (BitVec w) := let _true := hw_constant true let _false := hw_constant false let _2 := comb_xor _emitted_0 _true @@ -67,7 +77,7 @@ namespace TRY2 a `rdy` signal is received (no deadlock). -/ -def hw_fork (_in0 : Stream (BitVec 32)) : Stream (BitVec 32) × Stream (BitVec 32) := +def hw_fork (_in0 : Stream (BitVec w)) : Stream (BitVec w) × Stream (BitVec w) := (_in0, _in0) end TRY2 @@ -85,12 +95,12 @@ namespace TRY3 2. How do we model the nondeterministic signals (...some time later: we don't have to, we just expose them as streams) -/ -def hw_fork (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec 32)) +def hw_fork (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec w)) : Stream' ( BitVec 1 -- ready (_12) × BitVec 1 -- valid_0 (_3) × BitVec 1 -- valid_1 (_9) - × BitVec 32 -- rawOutput - × BitVec 32 -- rawOutput + × BitVec w -- rawOutput + × BitVec w -- rawOutput ) := Stream'.corec' (α := Nat × BitVec 1 × BitVec 1) (fun (i, _emitted_0, _emitted_1) => @@ -122,11 +132,11 @@ def hw_fork (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVe -/ def hw_add (_in0_valid _in1_valid _out0_ready : Stream' (BitVec 1)) - (_in0 _in1 : Stream' (BitVec 32)) + (_in0 _in1 : Stream' (BitVec w)) : Stream' ( BitVec 1 -- %in0_ready × BitVec 1 -- %in1_ready × BitVec 1 -- %out0_valid - × BitVec 32 -- %out0 + × BitVec w -- %out0 ) := Stream'.corec' (α := Nat) (fun i => @@ -145,31 +155,31 @@ def split_stream2 : Stream' (a × b × c × d × e) → Stream' a × Stream' b def combine_stream : Stream' a × Stream' b × Stream' c × Stream' d × Stream' e × Stream' f × Stream' g → Stream' (a × b × c × d × e × f × g) := fun gr i => (gr.1 i, gr.2.1 i, gr.2.2.1 i, gr.2.2.2.1 i, gr.2.2.2.2.1 i, gr.2.2.2.2.2.1 i, gr.2.2.2.2.2.2 i) -/-- +/- We have a working circuit, except that we took out the feedback into and output and an input. `fork_i_rdy -> add_out_rdy` -/ -def hw_add_fork af_a_valid af_b_valid af_a af_b af_o_rdy af_p_rdy add_out_rdy := - let add_a_valid := af_a_valid - let add_b_valid := af_b_valid - let add_a := af_a - let add_b := af_b - let (add_a_rdy, add_b_rdy, add_out_valid, add_out) := split_stream <| hw_add add_a_valid add_b_valid add_out_rdy add_a add_b - let fork_i_valid := add_out_valid - let fork_i := add_out - let fork_o_rdy := af_o_rdy - let fork_p_rdy := af_p_rdy - let (fork_i_rdy, fork_o_valid, fork_p_valid, fork_o, fork_p) := split_stream2 <| hw_fork fork_o_rdy fork_p_rdy fork_i_valid fork_i - combine_stream <| (fork_o_valid, fork_p_valid, fork_o, fork_p, add_a_rdy, add_b_rdy, fork_i_rdy) +-- def hw_add_fork af_a_valid af_b_valid af_a af_b af_o_rdy af_p_rdy add_out_rdy := +-- let add_a_valid := af_a_valid +-- let add_b_valid := af_b_valid +-- let add_a := af_a +-- let add_b := af_b +-- let (add_a_rdy, add_b_rdy, add_out_valid, add_out) := split_stream <| hw_add add_a_valid add_b_valid add_out_rdy add_a add_b +-- let fork_i_valid := add_out_valid +-- let fork_i := add_out +-- let fork_o_rdy := af_o_rdy +-- let fork_p_rdy := af_p_rdy +-- let (fork_i_rdy, fork_o_valid, fork_p_valid, fork_o, fork_p) := split_stream2 <| hw_fork fork_o_rdy fork_p_rdy fork_i_valid fork_i +-- combine_stream <| (fork_o_valid, fork_p_valid, fork_o, fork_p, add_a_rdy, add_b_rdy, fork_i_rdy) /-- The assumption is that you always converge in 2 steps, so this should faithfully implement add -> fork -/ -def hw_add_fork_fix af_a_valid af_b_valid af_a af_b af_o_rdy af_p_rdy := - let x := hw_add_fork af_a_valid af_b_valid af_a af_b af_o_rdy af_p_rdy (Stream'.const 0) - let x := hw_add_fork af_a_valid af_b_valid af_a af_b af_o_rdy af_p_rdy (fun i => (x i).2.2.2.2.2.2) - fun i => ((x i).1, (x i).2.1, (x i).2.2.1, (x i).2.2.2.1, (x i).2.2.2.2.1, (x i).2.2.2.2.2.1, (x i).2.2.2.2.2.2.1) +-- def hw_add_fork_fix af_a_valid af_b_valid af_a af_b af_o_rdy af_p_rdy := +-- let x := hw_add_fork af_a_valid af_b_valid af_a af_b af_o_rdy af_p_rdy (Stream'.const 0) +-- let x := hw_add_fork af_a_valid af_b_valid af_a af_b af_o_rdy af_p_rdy (fun i => (x i).2.2.2.2.2.2) +-- fun i => ((x i).1, (x i).2.1, (x i).2.2.1, (x i).2.2.2.1, (x i).2.2.2.2.1, (x i).2.2.2.2.2.1, (x i).2.2.2.2.2.2.1) def cyc {α} (l : List α) (h := by simp) := Stream'.cycle l h @@ -181,8 +191,8 @@ We can stabilise with two iterations: + We set `add_out_rdy` to that value, and check if `add_out_rdy` now equals `fork_i_rdy`. -/ -#eval Stream'.take 3 <| hw_add_fork_fix (cyc [0, 0, 1]) (cyc [0, 1, 1]) (cyc [11, 12, 13]) (cyc [21, 22, 23]) (cyc [1]) (cyc [1]) -#eval Stream'.take 3 <| hw_add_fork_fix (cyc [0, 0, 1]) (cyc [0, 1, 1]) (cyc [11, 12, 13]) (cyc [21, 22, 23]) (cyc [0, 0, 1]) (cyc [0, 0, 1]) +-- #eval Stream'.take 3 <| hw_add_fork_fix (cyc [0, 0, 1]) (cyc [0, 1, 1]) (cyc [11, 12, 13]) (cyc [21, 22, 23]) (cyc [1]) (cyc [1]) +-- #eval Stream'.take 3 <| hw_add_fork_fix (cyc [0, 0, 1]) (cyc [0, 1, 1]) (cyc [11, 12, 13]) (cyc [21, 22, 23]) (cyc [0, 0, 1]) (cyc [0, 0, 1]) /- #eval Stream'.take 1 <| hw_add_fork_fix (cyc [1]) (cyc [1]) (cyc [10]) (cyc [20]) (cyc [1]) (cyc [1]) - #eval Stream'.take 1 <| hw_add_fork_fix (cyc [1]) (cyc [1]) (cyc [10]) (cyc [20]) (cyc [1]) (cyc [1]) - #eval Stream'.take 1 <| hw_add_fork_fix (cyc [1]) (cyc [1]) (cyc [10]) (cyc [20]) (cyc [1]) (cyc [1]) -/ @@ -194,13 +204,13 @@ end TRY3 · delayed fork ~ normal fork -/ -/-- At the handshake level: (manual) delayed fork ~ normal fork: the outputs of the fork are bisimilar +/- 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) = TRY2.hw_fork a → - x ~ x' → - y ~ y' → - x ~ x' ∧ y ~ y' := by grind +-- theorem fork_refines {a x y x' y'} : +-- (x, y) = TRY2.hw_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 => @@ -265,6 +275,11 @@ inductive relation' : Stream (BitVec w) → Stream (BitVec w) → Prop where (∀ 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 -/ + +/- + `(rdIn, vldOut1, ...) = TRY3.split_stream2 (TRY3.hw_fork rdOut1 rdOut2 vldIn dataIn)` + and `TRY3.hw_fork` starts from `(0, 0#1, 0#1)`. In the coinductive step you must re-establish relation_fork for the dropped streams — which requires the dropped streams to again satisfy the fork equation from registers (0,0). That only holds if you cut at an instant where both emitted registers are actually 0, i.e. right after allDone fired. But the proof cuts at fstVldTrue + fstRdyOut + 1 — the instant out1 fired — and out2 may not have fired yet, so _emitted_0 = 1 at the cut and the restarted equation is false. The fix is to generalize the relation over register state: parameterize it by (e₀, e₁) (or quantify over a start state) and make hw_fork' take an initial state argument. Alternatively cut at the first allDone instant instead of the first out1 firing +-/ 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) -/ @@ -305,7 +320,7 @@ inductive relation_fork : Stream (BitVec w) → Stream (BitVec w) → Prop where /-- We unfold one step of the corecursive definition of `fork` -/ -def fork_corec (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec 32)) := +def fork_corec (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec w)) := fun (i, _emitted_0, _emitted_1) => let _true := hw_constant true let _false := hw_constant false @@ -326,12 +341,12 @@ def fork_corec (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (Bi ((_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)) +def hw_fork' (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitVec w)) : Stream' ( BitVec 1 -- ready (_12) × BitVec 1 -- valid_0 (_3) × BitVec 1 -- valid_1 (_9) - × BitVec 32 -- rawOutput - × BitVec 32 -- rawOutput + × BitVec w -- rawOutput + × BitVec w -- rawOutput ) := Stream'.corec' (α := Nat × BitVec 1 × BitVec 1) (fork_corec _ready _ready_1 _valid _in0) (0, 0#1, 0#1) @@ -339,7 +354,10 @@ def hw_fork' (_ready _ready_1 _valid : Stream' (BitVec 1)) (_in0 : Stream' (BitV /-- Prove that iterating `n` times starting from the `m`-th index of the stream yields the `n + m`-th index-/ -theorem fork_corec1 : +theorem fork_corec1 {w : Nat} + {rd0_in rd1_in vld_in : Stream' (BitVec 1)} + {data_in : Stream' (BitVec w)} + {m n : Nat} {x y : BitVec 1} : (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] @@ -469,7 +487,9 @@ theorem hw_fork_eq : TRY3.hw_fork rd0 rd1 vld data = hw_fork' rd0 rd1 vld data : unfold TRY3.hw_fork hw_fork' congr 1 -theorem vldOut1_implies_vldIn +theorem vldOut1_implies_vldIn {w : Nat} + {rdIn rdOut1 rdOut2 vldIn vldOut1 vldOut2 : Stream' (BitVec 1)} + {dataIn dataOut1 dataOut2 : Stream' (BitVec w)} {n : Nat} (h : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = TRY3.split_stream2 (TRY3.hw_fork rdOut1 rdOut2 vldIn dataIn)) (hvld : vldOut1 n = 1#1) : vldIn n = 1#1 := by @@ -484,7 +504,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_corec1 (rd0_in := rdOut1) (rd1_in := rdOut2) (vld_in := vldIn) (data_in := dataIn) (m := 0) (x := 0#1) (y := 0#1) (n := n) rw [hst] at this simp at this assumption @@ -509,7 +529,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_corec1 (rd0_in := rdOut1) (rd1_in := rdOut2) (vld_in := vldIn) (data_in := dataIn) (m := 0) (x := 0#1) (y := 0#1) (n := n) rw [hst] at this simp at this assumption @@ -579,7 +599,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_corec1 (rd0_in := rdOut1) (rd1_in := rdOut2) (vld_in := vldIn) (data_in := dataIn) (m := 0) (x := 0#1) (y := 0#1) (n := k) simp [hsk] at this; omega have hk := hbef k (Nat.lt_succ_self k) simp only [Function.comp] @@ -629,7 +649,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_corec1 (rd0_in := rdOut1) (rd1_in := rdOut2) (vld_in := vldIn) (data_in := dataIn) (m := 0) (x := 0#1) (y := 0#1) (n := n) rw [hst] at this simp at this assumption @@ -680,7 +700,7 @@ theorem vldOut_eq_vldIn_of_fork_unitl_sent2 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 + have := fork_corec1 (rd0_in := rdOut1) (rd1_in := rdOut2) (vld_in := vldIn) (data_in := dataIn) (m := 0) (x := 0#1) (y := 0#1) (n := k) grind have hvldk : vldOut2 k = vldIn ak := by have h := congr_fun hvldout2 k @@ -701,7 +721,7 @@ theorem vldOut_eq_vldIn_of_fork_unitl_sent2 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 + have := fork_corec1 (rd0_in := rdOut1) (rd1_in := rdOut2) (vld_in := vldIn) (data_in := dataIn) (m := 0) (x := 0#1) (y := 0#1) (n := n) rw [hst] at this simp at this assumption @@ -986,727 +1006,5 @@ theorem data_remains_constant_until_first 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) = TRY3.split_stream2 (TRY3.hw_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 [TRY3.split_stream2] - and_intros - · funext i - have := rdOut1_before_allDone (hfork := h_6) (n := i) - /- what happens to `rdOut1` after data is dispatched? -/ - - sorry - · sorry - · sorry - · sorry - · sorry - · /- first receiver after sent -/ - sorry - · /- first receiver after sent -/ - by_cases sndRecBeforeSent : fstVldTrue + fstRdyOut2 ≤ fstSentIdx - · /- second receiver before sent -/ - sorry - · /- first receiver after sent -/ - sorry - · /- 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 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 [TRY3.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 [TRY3.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 [TRY3.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 [TRY3.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 TRY3.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 TRY3.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 [TRY3.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 [TRY3.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 [TRY3.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 [TRY3.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) = TRY3.split_stream2 (a := BitVec 1) (TRY3.hw_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 TRY2.hw_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 diff --git a/SSA/Projects/CIRCT/HandshakeToHW/HWForkSampling.lean b/SSA/Projects/CIRCT/HandshakeToHW/HWForkSampling.lean new file mode 100644 index 0000000000..c9e8c8c0c3 --- /dev/null +++ b/SSA/Projects/CIRCT/HandshakeToHW/HWForkSampling.lean @@ -0,0 +1,820 @@ +import SSA.Projects.CIRCT.HandshakeToHW.HWFork + +/-! +# Transaction-level sampling of the `fork` circuit — definitions + +Refactoring of the fork refinement around the *`allDone` sampling* idea: + +* The refinement theorem `toStream rdIn vldIn dataIn ~ toStream rdOut1 vldOut1 dataOut1` + is factored through a third, auxiliary stream: output 1 *sampled at `allDone`*, + i.e. observed only when **all** receivers have received the current token. +* Since `rdIn = allDone` and `dataOut1 = dataIn` hold pointwise in the circuit, + the sampled stream is *equal* to the input stream. All bisimulation content + is then concentrated in one lemma (`out1_sampling_bisim`): moving each token's + observation instant from receiver 1's accept (`fire1`) to the transaction's + completion (`allDone`) only changes the stream by finitely many `none`s. + The producer interprets rdIn = 1 as "this token is consumed — I may present the next one." + + +Layout: +1. register trajectory (`emitted`) as a plain recursion over time, and named + combinational signals (`fire1`, `done0`, `allDone`, ...); +2. pointwise characterization of `hw_fork'` (`hw_fork'_get`) — the only place + `Stream'.corec'` ever needs to be unfolded; +3. statements for the library of circuit facts (the intermediate predicates, + *derived* from the circuit rather than assumed); +4. the coinduction relation `SampleRel` and the statements of + `out1_sampling_bisim` and `hw_fork_refines_out1`. +-/ + +namespace HWComponents +namespace Fork + +open HandshakeStream + +/-! ## Boolean infrastructure on `BitVec 1` -/ + +theorem comb_and_eq_one_iff (a b : BitVec 1) : + comb_and a b = 1#1 ↔ a = 1#1 ∧ b = 1#1 := by + bv_decide + +theorem comb_and_eq_zero_iff (a b : BitVec 1) : + comb_and a b = 0#1 ↔ a = 0#1 ∨ b = 0#1 := by + bv_decide + +theorem comb_or_eq_one_iff (a b : BitVec 1) : + comb_or a b = 1#1 ↔ a = 1#1 ∨ b = 1#1 := by + bv_decide + +theorem comb_or_eq_zero_iff (a b : BitVec 1) : + comb_or a b = 0#1 ↔ a = 0#1 ∧ b = 0#1 := by + bv_decide + +theorem comb_not_eq_one_iff (a : BitVec 1) : + comb_xor a (hw_constant true) = 1#1 ↔ a = 0#1 := by + bv_decide + +theorem comb_not_eq_zero_iff (a : BitVec 1) : + comb_xor a (hw_constant true) = 0#1 ↔ a = 1#1 := by + bv_decide + +/-! ## The register trajectory, as a plain recursion over time + +Instead of reasoning through `Stream'.corec'`/`Stream'.iterate`, we define the +`emitted` registers as a recursive function of the cycle index. Every signal of +the circuit then becomes a pure function of the current cycle. -/ + +/-- One clock cycle of the fork's register update. `e.1`/`e.2` are the +`emitted` registers of output 1/output 2. This is (definitionally) the state +update performed by `fork_corec`. -/ +def stepRegs (rd1 rd2 vld : BitVec 1) (e : BitVec 1 × BitVec 1) : + BitVec 1 × BitVec 1 := + let fire1 := comb_and rd1 (comb_and (comb_xor e.1 (hw_constant true)) vld) + let fire2 := comb_and rd2 (comb_and (comb_xor e.2 (hw_constant true)) vld) + let done0 := comb_or fire1 e.1 + let done1 := comb_or fire2 e.2 + let allDone := comb_and done0 done1 -- `_12` in `hw_fork` + (comb_and done0 (comb_xor allDone (hw_constant true)), + comb_and done1 (comb_xor allDone (hw_constant true))) + +variable (rdOut1 rdOut2 vldIn : Stream' (BitVec 1)) + +/-- The trajectory of the fork's `emitted` registers over time. -/ +def emitted : Nat → BitVec 1 × BitVec 1 + | 0 => (0#1, 0#1) + | n + 1 => stepRegs (rdOut1 n) (rdOut2 n) (vldIn n) (emitted n) + +/-- `e0 n = 1` iff receiver 1 has already accepted the token of the transaction +that is still open at cycle `n`. -/ +def e0 (n : Nat) : BitVec 1 := (emitted rdOut1 rdOut2 vldIn n).1 + +/-- `e1 n = 1` iff receiver 2 has already accepted the token of the transaction +that is still open at cycle `n`. -/ +def e1 (n : Nat) : BitVec 1 := (emitted rdOut1 rdOut2 vldIn n).2 + +/-- The fork's `valid` signal on output 1 (`_3` in the MLIR output). -/ +def vldOut1 (n : Nat) : BitVec 1 := + comb_and (comb_xor (e0 rdOut1 rdOut2 vldIn n) (hw_constant true)) (vldIn n) + +/-- The fork's `valid` signal on output 2 (`_9` in the MLIR output). -/ +def vldOut2 (n : Nat) : BitVec 1 := + comb_and (comb_xor (e1 rdOut1 rdOut2 vldIn n) (hw_constant true)) (vldIn n) + +/-- Receiver 1 accepts a token at cycle `n` (`_4` in the MLIR output). -/ +def fire1 (n : Nat) : BitVec 1 := + comb_and (rdOut1 n) (vldOut1 rdOut1 rdOut2 vldIn n) + +/-- Receiver 2 accepts a token at cycle `n` (`_10` in the MLIR output). -/ +def fire2 (n : Nat) : BitVec 1 := + comb_and (rdOut2 n) (vldOut2 rdOut1 rdOut2 vldIn n) + +/-- Receiver 1 has received the current token, now or earlier (`done0`, `_5`). -/ +def done0 (n : Nat) : BitVec 1 := + comb_or (fire1 rdOut1 rdOut2 vldIn n) (e0 rdOut1 rdOut2 vldIn n) + +/-- Receiver 2 has received the current token, now or earlier (`done1`, `_11`). -/ +def done1 (n : Nat) : BitVec 1 := + comb_or (fire2 rdOut1 rdOut2 vldIn n) (e1 rdOut1 rdOut2 vldIn n) + +/-- All receivers have received the current token; this is also the fork's +`ready` signal towards the producer (`allDone`, `_12`). -/ +def allDone (n : Nat) : BitVec 1 := + comb_and (done0 rdOut1 rdOut2 vldIn n) (done1 rdOut1 rdOut2 vldIn n) + +/-! Definitional equations for the registers (all `rfl`). -/ + +@[simp] theorem e0_zero : e0 rdOut1 rdOut2 vldIn 0 = 0#1 := rfl +@[simp] theorem e1_zero : e1 rdOut1 rdOut2 vldIn 0 = 0#1 := rfl + +theorem e0_succ (n : Nat) : + e0 rdOut1 rdOut2 vldIn (n + 1) + = comb_and (done0 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true)) := rfl + +theorem e1_succ (n : Nat) : + e1 rdOut1 rdOut2 vldIn (n + 1) + = comb_and (done1 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true)) := rfl + +/-! Unfolding equations for the combinational signals (all `rfl`). These +signals have no state of their own, so their `_def` equations hold at *every* +cycle; use them with `rw`/`simp` instead of `unfold`. -/ + +theorem vldOut1_def (n : Nat) : + vldOut1 rdOut1 rdOut2 vldIn n + = comb_and (comb_xor (e0 rdOut1 rdOut2 vldIn n) (hw_constant true)) + (vldIn n) := rfl + +theorem vldOut2_def (n : Nat) : + vldOut2 rdOut1 rdOut2 vldIn n + = comb_and (comb_xor (e1 rdOut1 rdOut2 vldIn n) (hw_constant true)) + (vldIn n) := rfl + +theorem fire1_def (n : Nat) : + fire1 rdOut1 rdOut2 vldIn n + = comb_and (rdOut1 n) (vldOut1 rdOut1 rdOut2 vldIn n) := rfl + +theorem fire2_def (n : Nat) : + fire2 rdOut1 rdOut2 vldIn n + = comb_and (rdOut2 n) (vldOut2 rdOut1 rdOut2 vldIn n) := rfl + +theorem done0_def (n : Nat) : + done0 rdOut1 rdOut2 vldIn n + = comb_or (fire1 rdOut1 rdOut2 vldIn n) (e0 rdOut1 rdOut2 vldIn n) := rfl + +theorem done1_def (n : Nat) : + done1 rdOut1 rdOut2 vldIn n + = comb_or (fire2 rdOut1 rdOut2 vldIn n) (e1 rdOut1 rdOut2 vldIn n) := rfl + +theorem allDone_def (n : Nat) : + allDone rdOut1 rdOut2 vldIn n + = comb_and (done0 rdOut1 rdOut2 vldIn n) + (done1 rdOut1 rdOut2 vldIn n) := rfl + +/-! `_succ` forms (all `rfl`): the cycle-`n + 1` value of each signal with the +register occurrence expanded one step, i.e. in terms of cycle-`n` signals and +cycle-`n + 1` inputs. The combinational signals are stateless, so all the +`succ`-structure funnels through `e0_succ`/`e1_succ`; these lemmas just +pre-compose that register step with the `_def` equations, which is the shape an +`induction n` proof consumes. -/ + +theorem vldOut1_succ (n : Nat) : + vldOut1 rdOut1 rdOut2 vldIn (n + 1) + = comb_and + (comb_xor + (comb_and (done0 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true))) + (hw_constant true)) + (vldIn (n + 1)) := rfl + +theorem vldOut2_succ (n : Nat) : + vldOut2 rdOut1 rdOut2 vldIn (n + 1) + = comb_and + (comb_xor + (comb_and (done1 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true))) + (hw_constant true)) + (vldIn (n + 1)) := rfl + +theorem fire1_succ (n : Nat) : + fire1 rdOut1 rdOut2 vldIn (n + 1) + = comb_and (rdOut1 (n + 1)) + (comb_and + (comb_xor + (comb_and (done0 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true))) + (hw_constant true)) + (vldIn (n + 1))) := rfl + +theorem fire2_succ (n : Nat) : + fire2 rdOut1 rdOut2 vldIn (n + 1) + = comb_and (rdOut2 (n + 1)) + (comb_and + (comb_xor + (comb_and (done1 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true))) + (hw_constant true)) + (vldIn (n + 1))) := rfl + +theorem done0_succ (n : Nat) : + done0 rdOut1 rdOut2 vldIn (n + 1) + = comb_or (fire1 rdOut1 rdOut2 vldIn (n + 1)) + (comb_and (done0 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true))) := rfl + +theorem done1_succ (n : Nat) : + done1 rdOut1 rdOut2 vldIn (n + 1) + = comb_or (fire2 rdOut1 rdOut2 vldIn (n + 1)) + (comb_and (done1 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true))) := rfl + +theorem allDone_succ (n : Nat) : + allDone rdOut1 rdOut2 vldIn (n + 1) + = comb_and + (comb_or (fire1 rdOut1 rdOut2 vldIn (n + 1)) + (comb_and (done0 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true)))) + (comb_or (fire2 rdOut1 rdOut2 vldIn (n + 1)) + (comb_and (done1 rdOut1 rdOut2 vldIn n) + (comb_xor (allDone rdOut1 rdOut2 vldIn n) (hw_constant true)))) := rfl + +/-! ## `hw_fork'`, pointwise -/ + +/-- The iteration of `fork_corec`'s state update is `(n, emitted n)`. +Subsumes `fork_corec1`. (Induction on `n` via `iterate_back_succ`.) -/ +theorem iterate_eq_emitted (dataIn : Stream' (BitVec 32)) (n : Nat) : + Stream'.iterate (Prod.snd ∘ fork_corec rdOut1 rdOut2 vldIn dataIn) + (0, 0#1, 0#1) n + = (n, emitted rdOut1 rdOut2 vldIn n) := by + induction n + · simp [emitted, Stream'.iterate] + · case _ m ihm => + simp [Stream'.iterate, ihm] + unfold fork_corec + simp [emitted, stepRegs] + +/-- Pointwise characterization of the fork circuit: at each cycle the outputs +are the combinational signals computed from the current register state and the +current inputs. This is the only lemma that ever needs to unfold +`Stream'.corec'`; everything downstream uses it via `rw`/`simp`. -/ +theorem hw_fork'_get (dataIn : Stream' (BitVec 32)) (n : Nat) : + hw_fork' rdOut1 rdOut2 vldIn dataIn n + = (allDone rdOut1 rdOut2 vldIn n, + vldOut1 rdOut1 rdOut2 vldIn n, + vldOut2 rdOut1 rdOut2 vldIn n, + dataIn n, dataIn n) := by + unfold hw_fork' Stream'.corec' Stream'.corec Stream'.map Stream'.get + rw [iterate_eq_emitted] + rfl + +/-! ## Library of circuit facts + +The intermediate predicates describing the fork's behaviour, stated as +*derived* facts about the circuit (not assumptions). -/ + +/-- `allDone` holds exactly when *every* receiver has received the current +token — accepting it this cycle (`fireᵢ`) or having accepted it earlier +(`emittedᵢ`). This is the circuit-level meaning of "allDone is such after all +receivers have received". -/ +theorem allDone_iff_all_received (n : Nat) : + allDone rdOut1 rdOut2 vldIn n = 1#1 + ↔ (fire1 rdOut1 rdOut2 vldIn n = 1#1 ∨ e0 rdOut1 rdOut2 vldIn n = 1#1) + ∧ (fire2 rdOut1 rdOut2 vldIn n = 1#1 ∨ e1 rdOut1 rdOut2 vldIn n = 1#1) := by + rw [allDone_def, done0_def, done1_def] + bv_decide + +/-- If receiver 1 accepts at cycle `n`, then the receiver is ready, output 1 is +valid, a token is being presented, and the receiver had not accepted the +current token before. -/ +theorem fire1_spec {n : Nat} (h : fire1 rdOut1 rdOut2 vldIn n = 1#1) : + rdOut1 n = 1#1 ∧ vldOut1 rdOut1 rdOut2 vldIn n = 1#1 + ∧ vldIn n = 1#1 ∧ e0 rdOut1 rdOut2 vldIn n = 0#1 := by + rw [fire1_def, vldOut1_def] at h + rw [vldOut1_def] + bv_decide + +/-- The fork does not offer the same token twice: output 1 is not valid while +its receiver has already accepted the current token. -/ +theorem vldOut1_zero_of_e0_one {n : Nat} + (h : e0 rdOut1 rdOut2 vldIn n = 1#1) : + vldOut1 rdOut1 rdOut2 vldIn n = 0#1 := by + rw [vldOut1_def] + bv_decide + +/-- Receiver 1 cannot accept while it has already accepted the current token. -/ +theorem fire1_zero_of_e0_one {n : Nat} (h : e0 rdOut1 rdOut2 vldIn n = 1#1) : + fire1 rdOut1 rdOut2 vldIn n = 0#1 := by + rw [fire1_def, vldOut1_def] + bv_decide + +/-- If output 1 is quiet (register clear, no accept), the transaction cannot +complete this cycle. -/ +theorem allDone_zero_of_quiet {n : Nat} + (he : e0 rdOut1 rdOut2 vldIn n = 0#1) + (hf : fire1 rdOut1 rdOut2 vldIn n = 0#1) : + allDone rdOut1 rdOut2 vldIn n = 0#1 := by + rw [allDone_def] + rw [fire1_def] at hf + rw [done0_def, fire1_def] + bv_decide + +/-- The `emitted` registers are mutually exclusive: at most one output can be +waiting for the other to catch up. (Case on `n`; for `n + 1` both registers +being set would require `allDone n = 1` and `allDone n = 0` at once.) -/ +theorem e0_e1_not_both {n : Nat} : + ¬(e0 rdOut1 rdOut2 vldIn n = 1#1 ∧ e1 rdOut1 rdOut2 vldIn n = 1#1) := by + induction n + · simp [e0_zero, e1_zero] + · simp [e0_succ, e1_succ, allDone_def] + bv_decide + +/-- `allDone` only fires while a token is actually being presented. +(Via `allDone_iff_all_received` and `e0_e1_not_both`.) -/ +theorem vldIn_of_allDone {n : Nat} + (h : allDone rdOut1 rdOut2 vldIn n = 1#1) : vldIn n = 1#1 := by + induction n + · simp [allDone_def, done0_def, done1_def, fire1_def, fire2_def, vldOut1_def] at h + bv_decide + · simp [allDone_succ, fire1_succ, fire2_succ, allDone_def] at h + bv_decide + +/-- Once the transaction completes, the register of output 1 is cleared. -/ +theorem e0_zero_of_allDone {n : Nat} + (h : allDone rdOut1 rdOut2 vldIn n = 1#1) : + e0 rdOut1 rdOut2 vldIn (n + 1) = 0#1 := by + simp [allDone_def, done0_def, done1_def, fire1_def, fire2_def, vldOut1_def, vldOut2_def] at h + simp [e0_succ, done0_def, allDone_def, fire1_def, vldOut1_def, done1_def, fire2_def, vldOut2_def] + bv_decide + +/-- While receiver 1 does not accept, its register stays clear. +(Induction via `Nat.le_induction`.) -/ +theorem e0_zero_of_no_fire {m n : Nat} (hmn : m ≤ n) + (h0 : e0 rdOut1 rdOut2 vldIn m = 0#1) + (hf : ∀ t, m ≤ t → t < n → fire1 rdOut1 rdOut2 vldIn t = 0#1) : + e0 rdOut1 rdOut2 vldIn n = 0#1 := by + induction n + · simp + · case _ t iht => + by_cases hle : m ≤ t + · specialize iht (by omega) (by intros; apply hf <;> omega) + specialize hf t + specialize hf hle (by omega) + simp [e0_succ, allDone_def, done0_def, done1_def] + simp [hf] + simp [comb_and, comb_or, comb_xor, hw_constant] + simp [fire2_def, comb_and, vldOut2, comb_xor, hw_constant] + simp [iht] + · have : m = t + 1 := by omega + subst this + simp [h0] + +/-- After receiver 1 accepts at `F`, its register stays set until the +transaction completes: `e0` is 1 on the whole window `(F, n]` as long as +`allDone` has not fired on `[F, n)`. (Induction via `Nat.le_induction`.) -/ +theorem e0_one_of_window {F n : Nat} (hFn : F < n) + (hF : fire1 rdOut1 rdOut2 vldIn F = 1#1) + (hAD : ∀ t, F ≤ t → t < n → allDone rdOut1 rdOut2 vldIn t = 0#1) : + e0 rdOut1 rdOut2 vldIn n = 1#1 := by + induction n + · omega -- contra + · case _ m ihm => + simp [e0_succ] + by_cases hlt : F < m + · specialize ihm hlt (by intros; apply hAD <;> omega) + specialize hAD m (by omega) (by omega) + simp [hAD] + simp [fire1, vldOut1_def, comb_and, comb_xor, hw_constant] at hF + simp [done0_def, fire1_def, vldOut1_def, ihm, + comb_and, comb_or, comb_xor, hw_constant] + · simp [show F = m by omega] at * + specialize hAD m (by omega) (by omega) + simp [hAD] + simp [done0, hF] + bv_decide + +/-- **Data is constant until all receivers have received.** Whenever a token is +presented, the transaction eventually completes (`allDone`), the token stays +valid throughout, and the data does not change until completion. This is the +predicate "data remains constant until all receivers have received", *derived* +from the handshake contracts and `data_remains_constant_until_first`. -/ +theorem dataIn_constant_until_allDone {dataIn : Stream' (BitVec 32)} + (hvr : globallyValidUntilReady vldIn (allDone rdOut1 rdOut2 vldIn)) + (hvd : globallyValidAndData vldIn dataIn) + {i : Nat} (hi : vldIn i = 1#1) : + ∃ k, allDone rdOut1 rdOut2 vldIn (i + k) = 1#1 ∧ vldIn (i + k) = 1#1 ∧ + (∀ j (_hj : j ≤ k), vldIn (i + j) = 1#1) ∧ + (∀ j (_hj : j ≤ k), dataIn (i + j) = dataIn i) ∧ + (∀ m (_hm : m < k), allDone rdOut1 rdOut2 vldIn (i + m) = 0#1) := + data_remains_constant_until_first hvd hvr hi + +/-! ## The two views of output 1 -/ + +/-- The *receiver-1 view* of output 1: a token is observed at the cycle where +receiver 1 accepts it (`fire1`). This is what receiver 1 actually sees on the +wires, waiting (`none`) included. -/ +def out1View (dataIn : Stream' (BitVec 32)) : Stream (BitVec 32) := + toStream rdOut1 (vldOut1 rdOut1 rdOut2 vldIn) dataIn + +/-- The *transaction-level view* of output 1: a token is observed only at the +cycle where the whole transaction completes (`allDone`), i.e. after **all** +receivers have received it. Note that, pointwise, this is exactly +`toStream rdIn vldIn dataIn` — the input stream — since `rdIn = allDone` and +`dataOut1 = dataIn` in the circuit (`hw_fork'_get`). -/ +def sampledView (dataIn : Stream' (BitVec 32)) : Stream (BitVec 32) := + toStream (allDone rdOut1 rdOut2 vldIn) vldIn dataIn + +/-! `get`-characterizations of the two views: each view is `some` exactly at +its observation instants (`fire1` resp. `allDone`). -/ + +theorem out1View_get_none {dataIn : Stream' (BitVec 32)} {t : Nat} + (h : fire1 rdOut1 rdOut2 vldIn t = 0#1) : + Stream'.get (out1View rdOut1 rdOut2 vldIn dataIn) t = none := by + rw [fire1_def, comb_and_eq_zero_iff] at h + rcases h with h | h <;> simp [out1View, toStream, Stream'.get, h] + +theorem out1View_get_some {dataIn : Stream' (BitVec 32)} {t : Nat} + (h : fire1 rdOut1 rdOut2 vldIn t = 1#1) : + Stream'.get (out1View rdOut1 rdOut2 vldIn dataIn) t = some (dataIn t) := by + obtain ⟨h1, h2, -, -⟩ := fire1_spec rdOut1 rdOut2 vldIn h + simp [out1View, toStream, Stream'.get, h1, h2] + +theorem sampledView_get_none {dataIn : Stream' (BitVec 32)} {t : Nat} + (h : allDone rdOut1 rdOut2 vldIn t = 0#1) : + Stream'.get (sampledView rdOut1 rdOut2 vldIn dataIn) t = none := by + simp [sampledView, toStream, Stream'.get, h] + +theorem sampledView_get_some {dataIn : Stream' (BitVec 32)} {t : Nat} + (h : allDone rdOut1 rdOut2 vldIn t = 1#1) : + Stream'.get (sampledView rdOut1 rdOut2 vldIn dataIn) t = some (dataIn t) := by + simp [sampledView, toStream, Stream'.get, h, + vldIn_of_allDone rdOut1 rdOut2 vldIn h] + +/-- If receiver 1 never accepts from cycle `m` on, the receiver-1 view is +silent from `m` on. -/ +theorem out1View_none_of_no_fire {dataIn : Stream' (BitVec 32)} {m : Nat} + (hf : ∀ t, m ≤ t → fire1 rdOut1 rdOut2 vldIn t = 0#1) : + ∀ t, m ≤ t → Stream'.get (out1View rdOut1 rdOut2 vldIn dataIn) t = none := + fun t ht => out1View_get_none rdOut1 rdOut2 vldIn (hf t ht) + +/-- If receiver 1 never accepts from cycle `m` on (and its register is clear +at `m`), then no transaction ever completes from `m` on: the handshake-level +(transaction-sampled) stream is silent forever. This is the "one stalled +receiver blocks the whole fork" behaviour. -/ +theorem sampledView_none_of_no_fire {dataIn : Stream' (BitVec 32)} {m : Nat} + (he : e0 rdOut1 rdOut2 vldIn m = 0#1) + (hf : ∀ t, m ≤ t → fire1 rdOut1 rdOut2 vldIn t = 0#1) : + ∀ t, m ≤ t → Stream'.get (sampledView rdOut1 rdOut2 vldIn dataIn) t = none := by + intro t ht + refine sampledView_get_none rdOut1 rdOut2 vldIn ?_ + refine allDone_zero_of_quiet rdOut1 rdOut2 vldIn ?_ (hf t ht) + exact e0_zero_of_no_fire rdOut1 rdOut2 vldIn ht he + (fun s hs1 _ => hf s hs1) + + +/-! ## The sampling bisimulation -/ + +/-- Coinduction relation for `out1_sampling_bisim`. Both streams are *tails of +one fixed run* of the circuit, cut at `tA` (receiver-1 view) and `tB` +(transaction-level view). The invariant ties the two cut points together +through the register: `e0` is set exactly on the skew window `[tA, tB)`, i.e. +receiver 1 has already been served the transaction that is still open at the +input side, and `tB` sits at a transaction boundary (`e0 tB = 0`). + +Keeping the *original* streams (cut, never restarted) means the circuit +equation and the handshake contracts never have to be re-established on +suffixes inside the coinduction. -/ +inductive SampleRel (rdOut1 rdOut2 vldIn : Stream' (BitVec 1)) + (dataIn : Stream' (BitVec 32)) : + Stream (BitVec 32) → Stream (BitVec 32) → Prop where + /-- Both streams are silent forever: no token will ever be exchanged again. + (Reached when no receiver-1 accept ever happens after the cut.) -/ + | stuck (a b : Stream (BitVec 32)) + (ha : ∀ i, Stream'.get a i = none) + (hb : ∀ j, Stream'.get b j = none) : + SampleRel rdOut1 rdOut2 vldIn dataIn a b + /-- Tails of one fixed run, with the `e0` window invariant. -/ + | cut (a b : Stream (BitVec 32)) (tA tB : Nat) + (ha : a = Stream'.drop tA (out1View rdOut1 rdOut2 vldIn dataIn)) + (hb : b = Stream'.drop tB (sampledView rdOut1 rdOut2 vldIn dataIn)) + (htAB : tA ≤ tB) + (hwin : ∀ t, tA ≤ t → t < tB → e0 rdOut1 rdOut2 vldIn t = 1#1) + (he0 : e0 rdOut1 rdOut2 vldIn tB = 0#1) : + SampleRel rdOut1 rdOut2 vldIn dataIn a b + + +theorem sampleRel_of_nones (hs1 : ∀ t, s1 t = none) (hs3 : ∀ t, s2 t = none) : + SampleRel rdOut1 rdOut2 vldIn dataIn s1 s2 := by + exact SampleRel.stuck s1 s2 hs1 hs3 + +/-- **Sampling output 1 when receiver 1 accepts, and sampling it when the whole +transaction completes (`allDone`), yield bisimilar streams.** Moving each +token's observation instant from `fire1` to `allDone` changes the stream only +by finitely many `none`s. This is the essential correctness content of the +fork: every presented token is delivered exactly once to receiver 1, with the +value it has at completion time. + +Proof plan (`Bisim.coinduct` with `pred := SampleRel ...`): +* `stuck` case: match `none` with `none` at `0`, stay `stuck`. +* `cut` case, no `fire1` at or after `tA`: both tails are all-`none` + (`e0_zero_of_no_fire` + `allDone_zero_of_quiet`); re-establish via `stuck`. +* `cut` case, first `fire1` at `F ≥ tA`: by the window invariant `F ≥ tB`; + the contract `hvr` yields the first completion `T ≥ F`; match + `some (dataIn F) = some (dataIn T)` (`globallyValidAndData_stable`), with + `none`s before on both sides (minimality of `F` and `T`); re-establish `cut` + at `(F + 1, T + 1)` — the new window is `e0_one_of_window`, the new boundary + is `e0_zero_of_allDone`. -/ +theorem out1_sampling_bisim (dataIn : Stream' (BitVec 32)) + (hvr : globallyValidUntilReady vldIn (allDone rdOut1 rdOut2 vldIn)) + (hvd : globallyValidAndData vldIn dataIn) : + out1View rdOut1 rdOut2 vldIn dataIn ~ sampledView rdOut1 rdOut2 vldIn dataIn := by + apply Bisim.coinduct (pred := SampleRel rdOut1 rdOut2 vldIn dataIn) + · intros s1 s2 hsample + rcases hsample + · case _ hs1 hs2 => + exists 0, 0 + simp + have hz1 := hs1 0 + have hz2 := hs2 0 + simp [hz1, hz2] + exact + SampleRel.stuck (Stream'.drop 1 s1) (Stream'.drop 1 s2) (fun i => hs1 (i + 1)) fun j => + hs2 (j + 1) + · case _ tA tB ha hb hAB hwin he0 => + by_cases hfire : ∃ t, fire1 rdOut1 rdOut2 vldIn (tA + t) = 1#1 + · /- + Next fires at tfst = tA + j + out1 | tA | ... | n | ... | | + out2 | tB | ... | | ... | m | + such that `out1 n = out2 m` and bisimilarity hold from then onwards. + * `n` is the first one to fire for the first stream, obtained from `fire1` + * `m` is the first one after `allDone` (at or after `tB`) + -/ + have hfirst := if_exists_first_exists hfire + obtain ⟨tdiff, htfst, htmin⟩ := hfirst + have hFtB : tB ≤ tA + tdiff := by + by_contra hcon + push_neg at hcon + have h1 := hwin (tA + tdiff) (by omega) hcon + simp [fire1, vldOut1_def, h1] at htfst + bv_decide + /- + out1 | tA | ... | tA + tdiff | ... | | | + out2 | ... | tB | ... | | ... | tA + tdiff + tbfst | + -/ + simp [globallyValidUntilReady] at hvr + specialize hvr (tA + tdiff) + (by simp [fire1, vldOut1_def] at htfst; bv_decide) + have hexists : ∃ k, allDone rdOut1 rdOut2 vldIn (tA + tdiff + k) = 1#1 := by grind + have ⟨tbfst, hbfst1, hbfst2⟩ := if_exists_first_exists hexists + exists tdiff, (tA + tdiff + tbfst - tB) + and_intros + · apply SampleRel.cut _ _ (tA + tdiff + 1) (tA + tdiff + tbfst + 1) + · simp [ha] + congr 1 + · simp [hb] + congr 1 + omega + · omega + · intro j hj hj2 + apply e0_one_of_window rdOut1 rdOut2 vldIn (by omega) htfst + intro jj hjj1 hjj2 + have := hbfst2 (jj - (tA + tdiff)) (by omega) + simp [show tA + tdiff + (jj - (tA + tdiff)) = jj by omega] at this + simp [this] + · exact e0_zero_of_allDone rdOut1 rdOut2 vldIn hbfst1 + · simp [ha, hb, Stream'.drop, show tA + tdiff + tbfst - tB + tB = tA + tdiff + tbfst by omega, Stream'.get] + simp [out1View, sampledView] + simp [fire1] at htfst + simp [toStream] + have hrd1 : rdOut1 (tA + tdiff) = 1#1 := by bv_decide + have hvldIn : vldIn (tA + tdiff + tbfst) = 1#1 := by grind + have hvld1 : vldOut1 rdOut1 rdOut2 vldIn (tA + tdiff) = 1#1 := by bv_decide + simp [show tdiff + tA = tA + tdiff by omega, hrd1, hvld1, hbfst1, hvldIn] + apply globallyValidAndData_stable (m := tA + tdiff) (n := tA + tdiff + tbfst) (data := dataIn) + (vld := vldIn) + · exact hvd + · intro k hk1 hk2 + obtain ⟨l, hl2, hl3, hl4⟩ := hvr + let jj := k - (tA + tdiff) + simp [show k = tA + tdiff + jj by omega] + have : jj ≤ l := by grind + by_cases hlt : jj < l + · apply hl4 + omega + · simp [show jj = l by omega] + exact hl3 + · omega + · simp [ha] + intro i hi + specialize htmin i hi + simp [fire1] at htmin + simp [Stream'.get, out1View, toStream] + bv_decide + · intro i hi + simp [hb] + simp [sampledView] + by_cases hlt : tB + i < tA + tdiff + · have hfire0 : ∀ s, tB ≤ s → s < tB + i + 1 → fire1 rdOut1 rdOut2 vldIn s = 0#1 := by + intro s hs1 hs2 + have := htmin (s - tA) (by omega) + simp [show tA + (s - tA) = s by omega] at this + exact this + have he0' : e0 rdOut1 rdOut2 vldIn (tB + i) = 0#1 := + e0_zero_of_no_fire rdOut1 rdOut2 vldIn (by omega) he0 (fun s h1 h2 => hfire0 s h1 (by omega)) + exact sampledView_get_none rdOut1 rdOut2 vldIn + (allDone_zero_of_quiet rdOut1 rdOut2 vldIn he0' (hfire0 _ (by omega) (by omega))) + · let jj := tB + i - tA - tdiff + simp [show tB + i = tA + tdiff + jj by omega] + specialize hbfst2 jj (by omega) + simp [Stream'.get, toStream, hbfst2] + · /- no fire ever again -/ + exists tA, tB + simp at hfire + have ha1 := out1View_none_of_no_fire rdOut1 rdOut2 vldIn + (m := tB) (dataIn := dataIn) + (by + intro t' ht' + specialize hfire (t' - tA) + simp [show tA + (t' - tA) = t' by omega] at hfire + bv_decide) + have ha2 := out1View_none_of_no_fire rdOut1 rdOut2 vldIn + (m := tA) (dataIn := dataIn) + (by + intro t' ht' + specialize hfire (t' - tA) + simp [show tA + (t' - tA) = t' by omega] at hfire + bv_decide) + simp [out1View] at ha2 + have hb2 := sampledView_none_of_no_fire rdOut1 rdOut2 vldIn (dataIn := dataIn) + (m := tB) he0 + (by + intro t' ht' + specialize hfire (t' - tA) + simp [show tA + (t' - tA) = t' by omega] at hfire + bv_decide) + simp [sampledView] at hb2 + simp [out1View] at ha + simp [sampledView] at hb + and_intros + · apply sampleRel_of_nones + · intro t + simp [ha] + apply ha2 + omega + · intro t + simp [hb] + apply hb2 + omega + · simp [ha, hb] + specialize ha2 (tA + tA) + specialize hb2 (tB + tB) + simp [ha2, hb2] + · simp [ha] + intro j hj + apply ha2 + omega + · simp [hb] + intro j hj + apply hb2 + omega + · apply SampleRel.cut _ _ 0 0 + · simp + · simp + · omega + · intros + simp at * + · simp [e0_zero] + +/-! ## Refinement of the handshake fork -/ + +/-- The components produced by `TRY3.hw_fork` are exactly the named signals of +this file. (Via `hw_fork_eq`, `split_stream2` and `hw_fork'_get`.) -/ +theorem hw_fork_components {dataIn : Stream' (BitVec 32)} + {rdIn vld1 vld2 : Stream' (BitVec 1)} {data1 data2 : Stream' (BitVec 32)} + (hfork : (rdIn, vld1, vld2, data1, data2) + = TRY3.split_stream2 (TRY3.hw_fork rdOut1 rdOut2 vldIn dataIn)) : + rdIn = allDone rdOut1 rdOut2 vldIn + ∧ vld1 = vldOut1 rdOut1 rdOut2 vldIn + ∧ vld2 = vldOut2 rdOut1 rdOut2 vldIn + ∧ data1 = dataIn ∧ data2 = dataIn := by + rw [hw_fork_eq] at hfork + simp only [TRY3.split_stream2, Prod.mk.injEq] at hfork + obtain ⟨hrdIn, hvld1, hvld2, hdata1, hdata2⟩ := hfork + and_intros + · simp [hrdIn, hw_fork'_get, vldOut2_def] + · simp [hvld1, hw_fork'_get] + · simp [hvld2, hw_fork'_get] + · simp [hdata1, hw_fork'_get] + · simp [hdata2, hw_fork'_get] + +/-- **The RTL fork refines the handshake fork on output 1**: under the +handshake contracts on the input (valid persists until acknowledged, data +stable while valid — no deadlock included), the stream of tokens seen by +receiver 1 is bisimilar to the input stream of tokens. + +(The transaction-level view is *pointwise equal* to the input stream by +`hw_fork_components`, so this is `out1_sampling_bisim` up to symmetry of `~`.) -/ +theorem hw_fork_refines_out1 {dataIn : Stream' (BitVec 32)} + {rdIn vld1 vld2 : Stream' (BitVec 1)} {data1 data2 : Stream' (BitVec 32)} + (hfork : (rdIn, vld1, vld2, data1, data2) + = TRY3.split_stream2 (TRY3.hw_fork rdOut1 rdOut2 vldIn dataIn)) + (hvr : globallyValidUntilReady vldIn rdIn) + (hvd : globallyValidAndData vldIn dataIn) : + toStream rdIn vldIn dataIn ~ toStream rdOut1 vld1 data1 := by + obtain ⟨h1, h2, -, h4, -⟩ := hw_fork_components rdOut1 rdOut2 vldIn hfork + subst h1 h2 h4 + apply HandshakeStream.symm + apply out1_sampling_bisim + · exact hvr + · exact hvd + +theorem emitted_swap (n : Nat) : emitted rdOut1 rdOut2 vldIn n = (emitted rdOut2 rdOut1 vldIn n).swap := by + induction n + · simp [emitted] + · case _ m ihm => + simp [emitted, ihm, stepRegs] + bv_decide + +/-! Transport of the signals along the swap (mechanical consequences of +`emitted_swap`): each out2 signal of this run is the corresponding out1 signal +of the run with the receivers' readies swapped, and `allDone` is invariant. -/ + +theorem e0_swap (n : Nat) : + e0 rdOut1 rdOut2 vldIn n = e1 rdOut2 rdOut1 vldIn n := by + unfold e0 e1 + rw [emitted_swap rdOut1 rdOut2 vldIn n] + simp + +theorem e1_swap (n : Nat) : + e1 rdOut1 rdOut2 vldIn n = e0 rdOut2 rdOut1 vldIn n := by + unfold e0 e1 + rw [emitted_swap rdOut1 rdOut2 vldIn n] + simp + +theorem vldOut2_swap : + vldOut2 rdOut1 rdOut2 vldIn = vldOut1 rdOut2 rdOut1 vldIn := by + funext n + rw [vldOut2_def, vldOut1_def, e1_swap rdOut1 rdOut2 vldIn n] + +theorem allDone_swap : + allDone rdOut1 rdOut2 vldIn = allDone rdOut2 rdOut1 vldIn := by + funext n + simp only [allDone_def, done0_def, done1_def, fire1_def, fire2_def, + vldOut1_def, vldOut2_def, + e0_swap rdOut1 rdOut2 vldIn, e1_swap rdOut1 rdOut2 vldIn] + bv_decide + +/-- Mirror of `hw_fork_refines_out1` for output 2. Provable without a second +coinduction: `stepRegs` is symmetric under swapping `(rd1, e.1) ↔ (rd2, e.2)`, +so `emitted rdOut1 rdOut2 vldIn n = (emitted rdOut2 rdOut1 vldIn n).swap` (one +induction over time), hence `vldOut2/fire2/e1` of this run are `vldOut1/fire1/e0` +of the swapped run and `allDone` is invariant under the swap (`comb_and` is +commutative). Transport `hw_fork_refines_out1 rdOut2 rdOut1` along these. -/ +theorem hw_fork_refines_out2 {dataIn : Stream' (BitVec 32)} + {rdIn vld1 vld2 : Stream' (BitVec 1)} {data1 data2 : Stream' (BitVec 32)} + (hfork : (rdIn, vld1, vld2, data1, data2) + = TRY3.split_stream2 (TRY3.hw_fork rdOut1 rdOut2 vldIn dataIn)) + (hvr : globallyValidUntilReady vldIn rdIn) + (hvd : globallyValidAndData vldIn dataIn) : + toStream rdIn vldIn dataIn ~ toStream rdOut2 vld2 data2 := by + obtain ⟨h1, -, h3, -, h5⟩ := hw_fork_components rdOut1 rdOut2 vldIn hfork + subst h1 h3 h5 + rw [allDone_swap rdOut1 rdOut2 vldIn] at hvr ⊢ + rw [vldOut2_swap rdOut1 rdOut2 vldIn] + apply HandshakeStream.symm + apply out1_sampling_bisim + · exact hvr + · exact hvd + + +/-- **The RTL fork refines the handshake fork** (`TRY2.hw_fork`), on both +outputs — the original goal of `HWComponents.hw_fork_refines'`, restated. + +Differences from the original statement, on purpose: +* the input is identified with the ready/valid-wrapped stream by *equality* + (`ha`), not by bisimilarity — composing through a `~`-hypothesis needs + transitivity of `~`, which is still `sorry` in `Stream/Basic.lean`; once + `Bisim.trans` is proven, the `a ~ toStream rdIn vldIn dataIn` version follows + immediately from this one; +* `globallyFinallyReady rd1/rd2` are gone: eventual readiness of the receivers + is subsumed by the no-deadlock contract `hvr` on the input channel, through + the circuit equation (`rdIn = allDone` only fires once both receivers have + received). -/ +theorem hw_fork_refines' {dataIn : Stream' (BitVec 32)} + {rdIn vld1 vld2 : Stream' (BitVec 1)} {data1 data2 : Stream' (BitVec 32)} + {x y a : Stream (BitVec 32)} + (hspec : (x, y) = TRY2.hw_fork a) + (hfork : (rdIn, vld1, vld2, data1, data2) + = TRY3.split_stream2 (TRY3.hw_fork rdOut1 rdOut2 vldIn dataIn)) + (ha : a = toStream rdIn vldIn dataIn) + (hvr : globallyValidUntilReady vldIn rdIn) + (hvd : globallyValidAndData vldIn dataIn) : + x ~ toStream rdOut1 vld1 data1 ∧ y ~ toStream rdOut2 vld2 data2 := by + simp only [TRY2.hw_fork, Prod.mk.injEq] at hspec + simp [hspec, ha] + and_intros + · apply hw_fork_refines_out1 (hfork := hfork) (hvr := hvr) (hvd := hvd) + · apply hw_fork_refines_out2 (hfork := hfork) (hvr := hvr) (hvd := hvd) + +end Fork +end HWComponents diff --git a/SSA/Projects/CIRCT/HandshakeToHW/add.lean b/SSA/Projects/CIRCT/HandshakeToHW/add.lean index 637deaf535..03babab149 100644 --- a/SSA/Projects/CIRCT/HandshakeToHW/add.lean +++ b/SSA/Projects/CIRCT/HandshakeToHW/add.lean @@ -3,6 +3,8 @@ import SSA.Projects.CIRCT.Stream.Lemmas import SSA.Projects.CIRCT.Register.Basic import SSA.Projects.CIRCT.Register.Lemmas import SSA.Projects.CIRCT.Handshake.Handshake +import SSA.Projects.CIRCT.HandshakeToHW.HWForkSampling +import SSA.Projects.CIRCT.HandshakeToHW.HWFork namespace HandshakeStream /-! @@ -68,35 +70,11 @@ def add_handshake (a b : Stream' (Option (BitVec 64))) := %12 = comb.and %5, %11 {sv.namehint = "allDone"} : i1 hw.output %12, %in0, %3, %in0, %9 : i1, i64, i1, i64, i1 } + + This fork is the same as the basic fork module. -/ -def handshake_fork_in_ui64_out_ui64_ui64 - (instruc : Stream' (wiresStruc 1 3 64)) : - Stream' (wiresStruc 2 3 64) := - register_wrapper_generalized - (inputs := instruc) - (init_regs := {result := #v[], signals := #v[0#1, 0#1]}) - (outops := 2) - (outsigs := 3) - (update_fun := - fun (inp, regs) => - let v2 := regs.signals[0] ^^^ 1#1 -- emitted_0 - let v3 := v2 &&& inp.signals[0] -- in0_valid - let v4 := inp.signals[1] &&& v3 -- out0_ready - let v5 := v4 ||| regs.signals[0] - let v8 := regs.signals[1] ^^^ 1#1 -- emitted_1 - let v9 := v8 &&& inp.signals[0] -- in0_valid - let v10 := inp.signals[2] &&& v9 -- out1_ready - let v11 := v10 ||| regs.signals[1] - let v12 := v5 &&& v11 - let v0 := v12 ^^^ 1#1 - let v1 := v5 &&& v0 - let v6 := v12 ^^^ 1#1 - let v7 := v11 &&& v6 - let updated_reg0 := v1 - let updated_reg1 := v7 - ⟨{result := #v[inp.result[0], inp.result[0]], signals := #v[v12, v3, v9]}, - {result := #v[], signals := #v[updated_reg0, updated_reg1]}⟩ - ) +def handshake_fork_in_ui64_out_ui64_ui64 (ready ready_1 valid : Stream' (BitVec 1)) (in0 : Stream' (BitVec 64)) := + HWComponents.TRY3.hw_fork ready ready_1 valid in0 /-- Second RTL module: @@ -108,23 +86,23 @@ def handshake_fork_in_ui64_out_ui64_ui64 hw.output %1, %1, %2, %0 : i1, i1, i64, i1 } + This circuit is purely combinational. + -/ -def arith_addi_in_ui64_ui64_out_ui64 - (xst : Stream' (wiresStruc 2 3 64)) : - Stream' (wiresStruc 1 3 64) := - register_wrapper_generalized - (inputs := xst) - (init_regs := {result := #v[], signals := #v[]}) - (outops := 1) - (outsigs := 3) - (update_fun := - fun (inp, regs) => - let v0 := inp.signals[0] &&& inp.signals[1] -- in0_valid &&& in1_valid - let v1 := inp.signals[2] &&& v0 -- out0_ready - let v2 := inp.result[0] + inp.result[1] - ⟨{result := #v[v2], signals := #v[v1, v1, v0]}, - {result := #v[], signals := #v[]}⟩ - ) +def arith_addi_in_ui64_ui64_out_ui64 (in0_valid in1_valid out0_ready: Stream' (BitVec 1)) (in0 in1 : Stream' (BitVec 64)) : + Stream' ( + BitVec 1 -- in0_ready + × BitVec 1 -- in1_ready + × BitVec 64 -- out0 + × BitVec 1 -- out0_valid + ) := + Stream'.corec' (α := Nat) (fun i => + let out0_valid := HWComponents.comb_and (in0_valid i) (in1_valid i) + let in0_ready := HWComponents.comb_and (out0_ready i) out0_valid + let out1_ready := HWComponents.comb_and (out0_ready i) out0_valid + let out0 := HWComponents.comb_add (in0 i) (in1 i) + ((in0_ready, out1_ready, out0, out0_valid), (i + 1)) + ) 0 /-- Third RTL module: @@ -148,48 +126,432 @@ def arith_addi_in_ui64_ui64_out_ui64 hw.output %handshake_fork0.in0_ready, %arith_addi1.in1_ready, %out1_ready, %arith_addi1.out0, %arith_addi1.out0_valid, %arg2, %arg2_valid : i1, i1, i1, i64, i1, i0, i1 } + + The composed `@add` module: we need to inline + the two adders' ready/valid equations into the fork's; the only registers are the fork's `emitted_0`/`emitted_1`. + + We also treat the `i0` type as `i1`, since the `BitVec 0` type in lean is degenerate. + +-/ +def add_rtl (arg0_valid arg1_valid arg2 arg2_valid out0_ready out1_ready : Stream' (BitVec 1)) (arg0 arg1 : Stream' (BitVec 64)) : + Stream' ( + BitVec 1 -- arg0_ready + × BitVec 1 -- arg1_ready + × BitVec 1 -- arg2_ready + × BitVec 64 -- out0 + × BitVec 1 -- out0_valid + × BitVec 1 --out1 + × BitVec 1 --out1_valid + ) := + + Stream'.corec' (α := Nat × BitVec 1 × BitVec 1) (fun (i, _emitted_0, _emitted_1) => + /- + %handshake_fork0.in0_ready, %handshake_fork0.out0, %handshake_fork0.out0_valid, %handshake_fork0.out1, %handshake_fork0.out1_valid = + hw.instance "handshake_fork0" @handshake_fork_in_ui64_out_ui64_ui64 + (in0: %arg0: i64, in0_valid: %arg0_valid: i1, clock: %clock: !seq.clock, reset: %reset: i1, out0_ready: %arith_addi0.in0_ready: i1, out1_ready: %arith_addi0.in1_ready: i1) -> + (in0_ready: i1, out0: i64, out0_valid: i1, out1: i64, out1_valid: i1) + -/ + let _true := HWComponents.hw_constant true + let _false := HWComponents.hw_constant false + let _2 := HWComponents.comb_xor _emitted_0 _true + let fork_valid0 := HWComponents.comb_and _2 (arg0_valid i) + let _8 := HWComponents.comb_xor _emitted_1 _true + let fork_valid1 := HWComponents.comb_and _8 (arg0_valid i) + let fork_rawOutput := arg0 i + /- + %arith_addi0.in0_ready, %arith_addi0.in1_ready, %arith_addi0.out0, %arith_addi0.out0_valid = + hw.instance "arith_addi0" @arith_addi_in_ui64_ui64_out_ui64 + (in0: %handshake_fork0.out0: i64, in0_valid: %handshake_fork0.out0_valid: i1, in1: %handshake_fork0.out1: i64, in1_valid: %handshake_fork0.out1_valid: i1, out0_ready: %arith_addi1.in0_ready: i1) -> + (in0_ready: i1, in1_ready: i1, out0: i64, out0_valid: i1) + -/ + let add0_out0_valid := HWComponents.comb_and fork_valid0 fork_valid1 + let add0_out0 := HWComponents.comb_add fork_rawOutput fork_rawOutput + /- + %arith_addi1.in0_ready, %arith_addi1.in1_ready, %arith_addi1.out0, %arith_addi1.out0_valid = + hw.instance "arith_addi1" @arith_addi_in_ui64_ui64_out_ui64 + (in0: %arith_addi0.out0: i64, in0_valid: %arith_addi0.out0_valid: i1, in1: %arg1: i64, in1_valid: %arg1_valid: i1, out0_ready: %out0_ready: i1) -> + (in0_ready: i1, in1_ready: i1, out0: i64, out0_valid: i1) + + -/ + let add1_out0_valid := HWComponents.comb_and add0_out0_valid (arg1_valid i) + let add1_in0_ready := HWComponents.comb_and (out0_ready i) add1_out0_valid + let add1_in1_ready := HWComponents.comb_and (out0_ready i) add1_out0_valid + let add0_in0_ready := HWComponents.comb_and add1_in0_ready add0_out0_valid + let _4 := HWComponents.comb_and add0_in0_ready fork_valid0 + let _5 := HWComponents.comb_or _4 _emitted_0 -- done0 + let add0_in1_ready := HWComponents.comb_and add1_in0_ready add0_out0_valid + let _10 := HWComponents.comb_and add0_in1_ready fork_valid1 + let _11 := HWComponents.comb_or _10 _emitted_1 -- done1 + let fork_ready := HWComponents.comb_and _5 _11 -- allDone + let _0 := HWComponents.comb_xor fork_ready _true + let _6 := HWComponents.comb_xor fork_ready _true + let _7 := HWComponents.comb_and _11 _6 + let _1 := HWComponents.comb_and _5 _0 + let add1_out0 := HWComponents.comb_add add0_out0 (arg1 i) + ((fork_ready, add1_in1_ready, (out1_ready i), add1_out0, add1_out0_valid, (arg2 i), (arg2_valid i)), (i + 1, _1, _7)) + ) (0, 0#1, 0#1) + +/-- The update function of `add_rtl`, extracted verbatim (the analogue of +`fork_corec` for the fork): one combinational cycle of the composed module as +a function of the corec state `(i, emitted_0, emitted_1)`. -/ +def add_rtl_corec (arg0_valid arg1_valid arg2 arg2_valid out0_ready out1_ready : + Stream' (BitVec 1)) (arg0 arg1 : Stream' (BitVec 64)) := + fun ((i, _emitted_0, _emitted_1) : Nat × BitVec 1 × BitVec 1) => + let _true := HWComponents.hw_constant true + let _false := HWComponents.hw_constant false + let _2 := HWComponents.comb_xor _emitted_0 _true + let fork_valid0 := HWComponents.comb_and _2 (arg0_valid i) + let _8 := HWComponents.comb_xor _emitted_1 _true + let fork_valid1 := HWComponents.comb_and _8 (arg0_valid i) + let fork_rawOutput := arg0 i + let add0_out0_valid := HWComponents.comb_and fork_valid0 fork_valid1 + let add0_out0 := HWComponents.comb_add fork_rawOutput fork_rawOutput + let add1_out0_valid := HWComponents.comb_and add0_out0_valid (arg1_valid i) + let add1_in0_ready := HWComponents.comb_and (out0_ready i) add1_out0_valid + let add1_in1_ready := HWComponents.comb_and (out0_ready i) add1_out0_valid + let add0_in0_ready := HWComponents.comb_and add1_in0_ready add0_out0_valid + let _4 := HWComponents.comb_and add0_in0_ready fork_valid0 + let _5 := HWComponents.comb_or _4 _emitted_0 -- done0 + let add0_in1_ready := HWComponents.comb_and add1_in0_ready add0_out0_valid + let _10 := HWComponents.comb_and add0_in1_ready fork_valid1 + let _11 := HWComponents.comb_or _10 _emitted_1 -- done1 + let fork_ready := HWComponents.comb_and _5 _11 -- allDone + let _0 := HWComponents.comb_xor fork_ready _true + let _6 := HWComponents.comb_xor fork_ready _true + let _7 := HWComponents.comb_and _11 _6 + let _1 := HWComponents.comb_and _5 _0 + let add1_out0 := HWComponents.comb_add add0_out0 (arg1 i) + ((fork_ready, add1_in1_ready, (out1_ready i), add1_out0, add1_out0_valid, (arg2 i), (arg2_valid i)), (i + 1, _1, _7)) + +/-- `add_rtl`, re-expressed through the named update function (the analogue of +`hw_fork'`). -/ +def add_rtl' (arg0_valid arg1_valid arg2 arg2_valid out0_ready out1_ready : + Stream' (BitVec 1)) (arg0 arg1 : Stream' (BitVec 64)) : + Stream' ( + BitVec 1 -- arg0_ready + × BitVec 1 -- arg1_ready + × BitVec 1 -- arg2_ready + × BitVec 64 -- out0 + × BitVec 1 -- out0_valid + × BitVec 1 --out1 + × BitVec 1 --out1_valid + ) := + Stream'.corec' (α := Nat × BitVec 1 × BitVec 1) + (add_rtl_corec arg0_valid arg1_valid arg2 arg2_valid out0_ready out1_ready + arg0 arg1) + (0, 0#1, 0#1) + +/-- The transcription and its named-update form agree (the analogue of +`hw_fork_eq`). -/ +theorem add_rtl_eq + {arg0_valid arg1_valid arg2 arg2_valid out0_ready out1_ready : + Stream' (BitVec 1)} {arg0 arg1 : Stream' (BitVec 64)} : + add_rtl arg0_valid arg1_valid arg2 arg2_valid out0_ready out1_ready arg0 arg1 + = add_rtl' arg0_valid arg1_valid arg2 arg2_valid out0_ready out1_ready + arg0 arg1 := by + unfold add_rtl add_rtl' add_rtl_corec + congr 1 + +/-! + ## Reasoning layer + + The composed circuit in the style of `HWForkSampling.lean`: every signal a + pure function of the cycle index, the fork's `emitted` pair as the only + state, and the `Fork` library reused through instantiation. -/ --- def add_rtl - /- - xst.result[0] = arg0 - xst.result[1] = arg1 - xst.signals[0] = arg0_valid - xst.signals[1] = arg1_valid - xst.signals[2] = arg2 - xst.signals[3] = arg2_valid - xst.signals[4] = out0_ready - xst.signals[5] = out1_ready - -/ - -- (inp : Stream' (wiresStruc 2 6 64)) : Stream' (wiresStruc 1 6 64) := - -- let arg0 := inp.resul[0] - -- let arg1 := inp.resut[1] - -- let arg0_valid := inp.signal[0] - -- let arg1_valid := inp.signal[1] - -- let arg2 := inp.signal[2] - -- let arg2_valid := inp.signal[3] - -- let out0_ready := inp.signal[4] - -- let out1_ready := inp.signal[5] - -- let fork_in : wiresStruc 1 3 64 := - -- {result := #v[arg0], - -- /- `out0_ready` and `out1_ready` are incorrect (see above). - -- we need to iteratively compute all the values in the current state of the circuit - -- (until fixed point). -/ - -- signals := #v[arg0_valid, out0_ready, out1_ready]} - -- sorry - - -theorem lowering_correctness - (a b : Stream (BitVec 64)) -- handshake level - (a_readyvalid b_readyvalid : wiresStructStream 1 2 64) -- rtl level - (sig_readyValid : Vector (Stream' (BitVec 1)) 3) -- extra input signal - (hsig : ReadyValid sig_readyValid sig) - (hsig_a : ReadyValidStruc a_readyvalid a) (hsig_b : ReadyValidStruc b_readyvalid b) : - let inp : wiresStructStream 2 6 64 := { - result := #v[a_readyvalid.result[0], b_readyvalid.result[0]] - signals := #v[a_readyvalid.signals[1], b_readyvalid.signals[1], - sig_readyValid[0], sig_readyValid[2], - a_readyvalid.signals[0], b_readyvalid.signals[0]]} - let inp' := streams_to_wires inp - let rtl' := add_rtl inp' - let rtl := wires_to_streams rtl' - (add_handshake a b) ~ rtl.result[0] := by sorry +namespace Add + +open HWComponents + +variable (arg0Vld arg1Vld out0Rdy : Stream' (BitVec 1)) + +/-- The ready signal presented to *each* fork output by the adder chain, as a +pure function of the fork's register state `e` and the current inputs: the +external `out0_ready`, gated backward through `addi1`'s and `addi0`'s joins. +Both fork outputs receive this same signal. -/ +def readyThroughAdders (a0v a1v or0 : BitVec 1) (e : BitVec 1 × BitVec 1) : + BitVec 1 := + let f0v := comb_and (comb_xor e.1 (hw_constant true)) a0v -- fork.out0_valid + let f1v := comb_and (comb_xor e.2 (hw_constant true)) a0v -- fork.out1_valid + let j0 := comb_and f0v f1v -- addi0.out0_valid + let j1 := comb_and j0 a1v -- addi1.out0_valid + comb_and (comb_and or0 j1) j0 + +/-- Trajectory of the composed module's only registers — the fork's `emitted` +pair — under the readies computed by the adder chain. -/ +def regs : Nat → BitVec 1 × BitVec 1 + | 0 => (0#1, 0#1) + | n + 1 => + let rd := readyThroughAdders (arg0Vld n) (arg1Vld n) (out0Rdy n) (regs n) + Fork.stepRegs rd rd (arg0Vld n) (regs n) + +@[simp] theorem regs_zero : regs arg0Vld arg1Vld out0Rdy 0 = (0#1, 0#1) := by rfl + +/-- The ready signal seen by both fork outputs, as a stream. -/ +def forkRdy (n : Nat) : BitVec 1 := + readyThroughAdders (arg0Vld n) (arg1Vld n) (out0Rdy n) + (regs arg0Vld arg1Vld out0Rdy n) + +theorem regs_succ (n : Nat) : + regs arg0Vld arg1Vld out0Rdy (n + 1) + = Fork.stepRegs (forkRdy arg0Vld arg1Vld out0Rdy n) + (forkRdy arg0Vld arg1Vld out0Rdy n) (arg0Vld n) + (regs arg0Vld arg1Vld out0Rdy n) := by rfl + +/-- **Instantiation lemma**: the composed module's registers are exactly the +abstract fork's registers run against the environment `forkRdy` — the +fork-in-context is the abstract fork of `HWForkSampling.lean` applied to the +(self-consistent) readies computed by the adders, so the whole `Fork` library +applies to it. (Induction on `n`; both recursions step by `Fork.stepRegs` from +`(0#1, 0#1)`, and `forkRdy n` depends only on `regs n`, so the induction +hypothesis closes the loop.) -/ +theorem regs_eq_emitted (n : Nat) : + regs arg0Vld arg1Vld out0Rdy n + = Fork.emitted (forkRdy arg0Vld arg1Vld out0Rdy) + (forkRdy arg0Vld arg1Vld out0Rdy) arg0Vld n := by + induction n + · simp [Fork.emitted] + · case _ m ihm => + simp [regs_succ, ihm, Fork.emitted] + + +/-! Named signals of the composed module, defined through the `Fork` +instantiation so that the `Fork` library applies definitionally. -/ + +/-- Fork `out0_valid` inside the composition. -/ +@[bv_normalize] +def fork0Vld (n : Nat) : BitVec 1 := + Fork.vldOut1 (forkRdy arg0Vld arg1Vld out0Rdy) + (forkRdy arg0Vld arg1Vld out0Rdy) arg0Vld n + +/-- Fork `out1_valid` inside the composition. -/ +@[bv_normalize] +def fork1Vld (n : Nat) : BitVec 1 := + Fork.vldOut2 (forkRdy arg0Vld arg1Vld out0Rdy) + (forkRdy arg0Vld arg1Vld out0Rdy) arg0Vld n + +/-- Ready returned to the `arg0` producer (the fork's `in0_ready = allDone`). -/ +@[bv_normalize] +def arg0Rdy (n : Nat) : BitVec 1 := + Fork.allDone (forkRdy arg0Vld arg1Vld out0Rdy) + (forkRdy arg0Vld arg1Vld out0Rdy) arg0Vld n + +/-- `arith_addi0.out0_valid`: the join of the two fork outputs. -/ +@[bv_normalize] +def join0Vld (n : Nat) : BitVec 1 := + comb_and (fork0Vld arg0Vld arg1Vld out0Rdy n) + (fork1Vld arg0Vld arg1Vld out0Rdy n) + +/-- `arith_addi1.out0_valid = out0_valid` of the composed module. -/ +@[bv_normalize] +def out0Vld (n : Nat) : BitVec 1 := + comb_and (join0Vld arg0Vld arg1Vld out0Rdy n) (arg1Vld n) + + +/-- Ready returned to the `arg1` producer (`arith_addi1.in1_ready`). -/ +@[bv_normalize] +def arg1Rdy (n : Nat) : BitVec 1 := + comb_and (out0Rdy n) (out0Vld arg0Vld arg1Vld out0Rdy n) + +variable (arg0 arg1 : Stream' (BitVec 64)) + +/-- Data path of the composed module: combinational, `out0 = (arg0 + arg0) + arg1`. -/ +@[bv_normalize] +def out0Data (n : Nat) : BitVec 64 := (arg0 n + arg0 n) + arg1 n + +/-! ### The transcription computes the named signals -/ + +/-- `add_rtl`'s corec state is `(n, regs n)` — the analogue of +`iterate_eq_emitted`. (Induction on `n`; the register updates of +`add_rtl_corec` are, after zeta-reduction, exactly +`Fork.stepRegs (readyThroughAdders …) (readyThroughAdders …) (arg0Vld n)`.) -/ +theorem add_rtl_iterate {arg2 arg2Vld out1Rdy : Stream' (BitVec 1)} (n : Nat) : + Stream'.iterate + (Prod.snd ∘ add_rtl_corec arg0Vld arg1Vld arg2 arg2Vld out0Rdy out1Rdy + arg0 arg1) + (0, 0#1, 0#1) n + = (n, regs arg0Vld arg1Vld out0Rdy n) := by + induction n + · simp [Stream'.iterate] + · case _ m ihm => + simp [Stream'.iterate, ihm] + unfold add_rtl_corec + simp + simp [regs_succ, Fork.stepRegs] + exact Prod.mk_inj.mp _root_.rfl + + +/-! ### Composition facts -/ + +/-- **The fork never stalls inside this composition**: both fork outputs see +the same ready (`forkRdy`), and from clear registers both outputs are valid +together, so both receivers always accept in the same cycle — `allDone` fires +in the same cycle as the accepts and the registers never latch. (Induction on +`n`; the step is pointwise: `regs_succ`, `Fork.stepRegs`, `bv_decide`.) -/ +theorem regs_eq_zero (n : Nat) : + regs arg0Vld arg1Vld out0Rdy n = (0#1, 0#1) := by + induction n + · simp + · case _ m ihm => + simp [regs_succ, ihm, Fork.stepRegs] + bv_decide + +/-- With the registers identically clear the fork is transparent: `out0_valid` +is the conjunction of the input valids. (Pointwise from `regs_eq_zero`.) -/ +theorem out0Vld_eq (n : Nat) : + out0Vld arg0Vld arg1Vld out0Rdy n + = comb_and (arg0Vld n) (arg1Vld n) := by + have hreg : Fork.emitted (forkRdy arg0Vld arg1Vld out0Rdy) + (forkRdy arg0Vld arg1Vld out0Rdy) arg0Vld n = (0#1, 0#1) := + (regs_eq_emitted arg0Vld arg1Vld out0Rdy n).symm.trans + (regs_eq_zero arg0Vld arg1Vld out0Rdy n) + simp [out0Vld, join0Vld, fork0Vld, fork1Vld, + Fork.vldOut1_def, Fork.vldOut2_def, Fork.e0, Fork.e1, hreg] + bv_decide + +/-- With the registers identically clear, the ready returned to `arg0` is the +external ready gated by both valids: the composed module behaves as one +combinational join. (Pointwise from `regs_eq_zero`.) -/ +theorem arg0Rdy_eq (n : Nat) : + arg0Rdy arg0Vld arg1Vld out0Rdy n + = comb_and (out0Rdy n) (comb_and (arg0Vld n) (arg1Vld n)) := by + have hreg : Fork.emitted (forkRdy arg0Vld arg1Vld out0Rdy) + (forkRdy arg0Vld arg1Vld out0Rdy) arg0Vld n = (0#1, 0#1) := + (regs_eq_emitted arg0Vld arg1Vld out0Rdy n).symm.trans + (regs_eq_zero arg0Vld arg1Vld out0Rdy n) + simp [arg0Rdy, Fork.allDone_def, Fork.done0_def, Fork.fire1_def, Fork.vldOut1_def, Fork.e0, + Fork.done1, Fork.vldOut2_def, Fork.fire2, Fork.e1, hreg, comb_and, comb_or, comb_xor, hw_constant, + forkRdy, readyThroughAdders, regs_eq_zero] + bv_decide + +/-- Pointwise characterization of the composed module — the analogue of +`hw_fork'_get`. With `regs_eq_zero`, the corec state is the literal `(0, 0)` +pair, the transcription's body fully reduces, and the named signals collapse +through `out0Vld_eq`/`arg0Rdy_eq`; every component is then `rfl` or a width-1 +boolean fact. -/ +theorem add_rtl'_get {arg2 arg2Vld out1Rdy : Stream' (BitVec 1)} (n : Nat) : + add_rtl' arg0Vld arg1Vld arg2 arg2Vld out0Rdy out1Rdy arg0 arg1 n + = (arg0Rdy arg0Vld arg1Vld out0Rdy n, + arg1Rdy arg0Vld arg1Vld out0Rdy n, + out1Rdy n, + out0Data arg0 arg1 n, + out0Vld arg0Vld arg1Vld out0Rdy n, + arg2 n, arg2Vld n) := by + unfold add_rtl' Stream'.corec' Stream'.corec Stream'.map Stream'.get + simp only [Function.comp_apply] + rw [add_rtl_iterate, regs_eq_zero] + simp only [add_rtl_corec] + simp only [arg1Rdy, out0Vld_eq, arg0Rdy_eq, out0Data] + simp only [HWComponents.comb_and, HWComponents.comb_or, HWComponents.comb_xor, + HWComponents.hw_constant, HWComponents.comb_add, comb_and, + reduceIte, Prod.mk.injEq] + and_intros <;> first | rfl | bv_decide + +/-! ### Correctness -/ + +/-- Split a stream of `add_rtl`-shaped 7-tuples into its component streams +(mirrors `TRY3.split_stream2` for the fork's 5-tuples). -/ +def split_stream7 {a b c d e f g : Type} : + Stream' (a × b × c × d × e × f × g) → + Stream' a × Stream' b × Stream' c × Stream' d × Stream' e × Stream' f + × Stream' g := fun s => + (fun i => (s i).1, fun i => (s i).2.1, fun i => (s i).2.2.1, + fun i => (s i).2.2.2.1, fun i => (s i).2.2.2.2.1, + fun i => (s i).2.2.2.2.2.1, fun i => (s i).2.2.2.2.2.2) + +/-- The components produced by `add_rtl` are exactly the named signals of this +section — the analogue of `hw_fork_components`. (Route: an +`iterate_eq_emitted`-style lemma identifying `add_rtl`'s corec state with +`(n, regs n)`, then read off each output component pointwise.) -/ +theorem add_rtl_components + {arg2 arg2Vld out1Rdy : Stream' (BitVec 1)} + {arg0Rdy' arg1Rdy' arg2Rdy' out0Vld' out1' out1Vld' : Stream' (BitVec 1)} + {out0' : Stream' (BitVec 64)} + (hadd : (arg0Rdy', arg1Rdy', arg2Rdy', out0', out0Vld', out1', out1Vld') + = split_stream7 (add_rtl arg0Vld arg1Vld arg2 arg2Vld out0Rdy out1Rdy + arg0 arg1)) : + arg0Rdy' = arg0Rdy arg0Vld arg1Vld out0Rdy + ∧ arg1Rdy' = arg1Rdy arg0Vld arg1Vld out0Rdy + ∧ arg2Rdy' = out1Rdy + ∧ out0' = out0Data arg0 arg1 + ∧ out0Vld' = out0Vld arg0Vld arg1Vld out0Rdy + ∧ out1' = arg2 ∧ out1Vld' = arg2Vld := by + simp [add_rtl_eq, split_stream7, Prod.mk.injEq] at hadd + obtain ⟨h1, h2, h3, h4, h5, h6, h7⟩ := hadd + and_intros + · simp [h1, add_rtl'_get] + · simp [h2, add_rtl'_get] + · simp [h3, add_rtl'_get] + · simp [h4, add_rtl'_get] + · simp [h5, add_rtl'_get] + · simp [h6, add_rtl'_get] + · simp [h7, add_rtl'_get] + + +/-- **Lowering correctness for the composed `add` module**: given the RTL +circuit `add_rtl` (via its output streams, bound by `hadd` — the analogue of +the fork equation in `hw_fork_refines_out1`), the handshake-level program +applied to the token streams of the two inputs is bisimilar to the token +stream of the RTL output. + +Proof plan: `add_rtl_components` + `subst` reduce the goal to the named +signals; by `regs_eq_zero` and its corollaries the RTL side is a single +combinational join (`out0Vld_eq`, `arg0Rdy_eq`, data path `out0Data`); the +fork contributes no further proof obligations. What remains is the handshake +side: `HandshakeOp.fork x = (x, x)` and a `syncMap₂_aligned` lemma (when the +two argument streams carry their `some`s at identical positions, `syncMap₂ f` +is the pointwise zip). Both token inputs here fire at the same instants +(`arg0Rdy ∧ arg0Vld` and `arg1Rdy ∧ arg1Vld` both reduce to +`out0Rdy ∧ arg0Vld ∧ arg1Vld`), so the two sides are pointwise *equal* and +`~` follows by reflexivity — the handshake contract hypotheses are not needed: +with the registers identically clear the composed module is memoryless, and +the contracts only existed to tame register skew. -/ +theorem add_lowering_correctness + {arg2 arg2Vld out1Rdy : Stream' (BitVec 1)} + {arg0Rdy' arg1Rdy' arg2Rdy' out0Vld' out1' out1Vld' : Stream' (BitVec 1)} + {out0' : Stream' (BitVec 64)} + (hadd : (arg0Rdy', arg1Rdy', arg2Rdy', out0', out0Vld', out1', out1Vld') + = split_stream7 (add_rtl arg0Vld arg1Vld arg2 arg2Vld out0Rdy out1Rdy + arg0 arg1)) : + add_handshake + (toStream arg0Rdy' arg0Vld arg0) + (toStream arg1Rdy' arg1Vld arg1) + ~ toStream out0Rdy out0Vld' out0' := by + obtain ⟨h1, h2, -, h4, h5, -, -⟩ := + add_rtl_components arg0Vld arg1Vld out0Rdy arg0 arg1 hadd + subst h1 h2 h4 h5 + have hcase : ∀ b : BitVec 1, b = 0#1 ∨ b = 1#1 := by + intro b + by_cases hb : b = 1#1 + · exact Or.inr hb + · exact Or.inl (HWComponents.false_of_width_one _ hb) + have hbisim_of_eq : ∀ {a b : Stream (BitVec 64)}, a = b → a ~ b := by + intro a b heq + rw [heq] + exact HandshakeStream.rfl + unfold add_handshake + rw [HandshakeOp.fork_eq] + dsimp only [] + rw [syncMap₂_aligned (fun _ => Iff.rfl)] + have hal : ∀ n, + ((alignedZip BitVec.add + (toStream (arg0Rdy arg0Vld arg1Vld out0Rdy) arg0Vld arg0) + (toStream (arg0Rdy arg0Vld arg1Vld out0Rdy) arg0Vld arg0)) n).isSome + ↔ (toStream (arg1Rdy arg0Vld arg1Vld out0Rdy) arg1Vld arg1 n).isSome := by + intro n + rcases hcase (arg0Vld n) with h0 | h0 <;> + rcases hcase (arg1Vld n) with ha | ha <;> + rcases hcase (out0Rdy n) with hr | hr <;> + simp [alignedZip, toStream, arg1Rdy, out0Vld_eq, arg0Rdy_eq, h0, ha, hr, + HWComponents.comb_and] + rw [syncMap₂_aligned hal] + apply hbisim_of_eq + funext n + rcases hcase (arg0Vld n) with h0 | h0 <;> + rcases hcase (arg1Vld n) with ha | ha <;> + rcases hcase (out0Rdy n) with hr | hr <;> + simp [alignedZip, toStream, arg1Rdy, out0Vld_eq, arg0Rdy_eq, out0Data, + h0, ha, hr, HWComponents.comb_and, BitVec.add_eq] + +end Add +end HandshakeStream diff --git a/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean new file mode 100644 index 0000000000..acfd80f988 --- /dev/null +++ b/SSA/Projects/CIRCT/HandshakeToHW/fork_lowering.lean @@ -0,0 +1,897 @@ +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) + +/-- + 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, + 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) + +/-- + 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 + + +/-- + 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 + +/-- + 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) + +/-- + 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` -/ + /- *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* 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* 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 → + /- *If* eventually, + a ready signal arrives from both receivers (`rdOut1 i = 1#1`), (`rdOut2 i = 1#1`). -/ + globallyFinallyReady rdOut1 → + globallyFinallyReady rdOut2 → + /- *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 + + +/-- + Define the unfolding of 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)) + +/-- + 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) + × 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_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] + | succ x h => + rw [Stream'.iterate_eq] + dsimp [Stream'.cons] + dsimp [fork_corec] + grind + +/-- + 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 + dsimp [fork_corec, comb_and, comb_xor, hw_constant] + specialize h a + simp [h] + +/-- + 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 + dsimp [fork_corec, comb_and, comb_xor, hw_constant] + specialize h a + simp [h] + +/-- + 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 + induction n generalizing s with + | 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)) + (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] + +/-- + 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 + unfold rtl.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] + +/-- + 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 + simp [project_stream] at h + simp [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 + dsimp [fork_corec] + rw [show a = (a, b, c).1 by rfl, ← h, fork_corec_iter]; rfl + +/-- + 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 + intro n + simp [project_stream] at h + simp [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 + dsimp [fork_corec] + 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 + +/-- Data passes unchanged through the fork's first output channel. -/ +private theorem hw_fork_out0 + (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 := + fork_dataIn_eq_dataOut1 h + +/-- Data passes unchanged through the fork's second output channel. -/ +private theorem hw_fork_out1 + (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 := + fork_dataIn_eq_dataOut2 h + +/-- + 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)) + (hvld : vldOut1 n = 1#1) : vldIn n = 1#1 := by + rw [hw_fork_eq] at h + simp [project_stream] at h + obtain ⟨-, hvldout1, -⟩ := h + have hn := congr_fun hvldout1 n + rw [hvld] 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 + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn + have heq : a = n := by + have := @fork_corec_iter 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 + +/-- + 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)) + (hvld : vldOut2 n = 1#1) : vldIn n = 1#1 := by + rw [hw_fork_eq] at h + simp [project_stream] at h + obtain ⟨-, -, hvldout2, -⟩ := h + have hn := congr_fun hvldout2 n + rw [hvld] 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 + dsimp [fork_corec, comb_and, comb_xor, hw_constant] at hn + have heq : a = n := by + have := @fork_corec_iter 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 + +/-- + 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) + (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] + +/-- + 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)) + /- 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 [project_stream] at hfork + obtain ⟨-, hvldout1, -⟩ := hfork + have hn := congr_fun hvldout1 n + 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 + 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_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] + have hvldk : vldOut1 k = vldIn ak := by + have h := congr_fun hvldout1 k + 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 + 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_corec_iter 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) = + 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) : + 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) = + 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 [project_stream] at hfork + obtain ⟨-, -, hvldout2, -⟩ := hfork + have hn := congr_fun hvldout2 n + 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 + 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_corec_iter 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 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 + 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_corec_iter 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) = + 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)) + 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) = + 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) + 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) = + 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) + 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) = + project_stream (rtl.fork rdOut1 rdOut2 vldIn dataIn)) + (hgv : globallyValidAndData vldIn dataIn) : + globallyValidAndData vldOut1 dataOut1 := by + intro i ⟨hi1, hi2⟩ + have hfork' : (rdIn, vldOut1, vldOut2, dataOut1, dataOut2) = + project_stream (rtl.fork' rdOut1 rdOut2 vldIn dataIn) := by rw [← hw_fork_eq]; exact hfork + 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 + + +end HWComponents diff --git a/SSA/Projects/CIRCT/HandshakeToHW/transitivity.lean b/SSA/Projects/CIRCT/HandshakeToHW/transitivity.lean new file mode 100644 index 0000000000..4d2558c74f --- /dev/null +++ b/SSA/Projects/CIRCT/HandshakeToHW/transitivity.lean @@ -0,0 +1,493 @@ +/- +This file was generated by Aristotle. + +Lean version: leanprover/lean4:v4.24.0 +Mathlib version: f897ebcf72cd16f89ab4577d0c826cd14afaafc7 +This project request had uuid: 7fcea134-cfac-4390-8a80-0d75c6fc938e +-/ + +/- +We define a stream type `MyStream` (as `Stream` is already defined in Mathlib) and a bisimulation relation `Bisim` on it. We prove that `Bisim` is an equivalence relation, specifically proving transitivity in `stream_bisim_trans`. Note that the theorem is named `stream_bisim_trans` because `trans` is a reserved name in Lean/Mathlib. The proof uses coinduction and several helper lemmas handling `none` values and stepping through the streams. +-/ + +import Mathlib + +open scoped BigOperators +open scoped Real +open scoped Nat +open scoped Classical +open scoped Pointwise + +set_option maxHeartbeats 0 +set_option maxRecDepth 4000 +set_option synthInstance.maxHeartbeats 20000 +set_option synthInstance.maxSize 128 + +set_option relaxedAutoImplicit false +set_option autoImplicit false + +noncomputable section + +#check Stream + +#check Stream' +#check Stream'.get +#check Stream'.drop + +def MyStream (β : Type) := Stream' (Option β) + +def BisimGen {α : Type} (R : MyStream α → MyStream α → Prop) (a b : MyStream α) : Prop := + ∃ n m, R (a.drop (n + 1)) (b.drop (m + 1)) ∧ + Stream'.get a n = Stream'.get b m ∧ + (∀ i < n, Stream'.get a i = none) ∧ + (∀ j < m, Stream'.get b j = none) + +lemma BisimGen_mono {α : Type} : Monotone (@BisimGen α) := by + -- To prove monotonicity, we need to show that if $R \subseteq S$, then $\text{BisimGen } R \subseteq \text{BisimGen } S$. + intros R S hRS x y hxy + simp [BisimGen]; + -- Since $R \subseteq S$, the condition for $BisimGen R x y$ implies the same condition for $BisimGen S x y$. + obtain ⟨n, m, hR, hxy⟩ := hxy; + use n, m; + aesop + +def Bisim {α : Type} : MyStream α → MyStream α → Prop := + OrderHom.gfp ⟨@BisimGen α, BisimGen_mono⟩ + +infix:50 " ~ " => Bisim + +theorem Bisim.coinduct {α : Type} {R : MyStream α → MyStream α → Prop} + (h : ∀ a b, R a b → BisimGen R a b) : + ∀ a b, R a b → a ~ b := by + aesop; + refine' ⟨ _, _ ⟩; + exact True; + aesop + +theorem Bisim.step {α : Type} {a b : MyStream α} {n m : Nat} : + Bisim (a.drop (n + 1)) (b.drop (m + 1)) → + Stream'.get a n = Stream'.get b m → + (∀ i < n, Stream'.get a i = none) → + (∀ j < m, Stream'.get b j = none) → + Bisim a b := by + intros h1 h2 h3 h4; + -- By definition of bisimilarity, we need to show that $a \sim b$. + unfold Bisim at *; simp_all +decide [ Stream'.get ] ; + -- Let's unfold the definition of the bisimulation relation. + unfold OrderHom.gfp at *; simp_all +decide [ BisimGen ] ; + -- Let's choose the relation R that includes the pairs (a, b) and (Stream'.drop (n + 1) a, Stream'.drop (m + 1) b). + obtain ⟨R, hR⟩ := h1; + use fun x y => x = a ∧ y = b ∨ R x y; + aesop; + intro x y hxy; aesop; + · constructor <;> aesop; + · have := left _ _ h_1; unfold BisimGen at this; aesop; + constructor <;> aesop + +#check Stream'.cons + +/- +Bisimulation is symmetric. +-/ +lemma Bisim_symm {α : Type} {a b : MyStream α} : a ~ b → b ~ a := by + intro hab; + -- By definition of bisimulation, we need to show that for all `n`, `a.get n = b.get n` and `a.drop n ≤ b.drop n` and `b.drop n ≤ a.drop n`. + apply Bisim.coinduct; + swap; + tauto; + intro a b hab; + obtain ⟨ n, m, hnm ⟩ := hab; + obtain ⟨ f, hf ⟩ := m; + aesop; + obtain ⟨ n, m, hnm ⟩ := left _ _ hnm; + refine' ⟨ m, n, _, _, _, _ ⟩ <;> aesop; + exact? + +/- +If two streams are bisimilar via witnesses n and m, then dropping any prefix of the first stream (up to n) preserves bisimilarity to the second stream. +-/ +lemma Bisim_drop_of_witness {α : Type} {a b : MyStream α} {n m : Nat} : + Bisim (a.drop (n + 1)) (b.drop (m + 1)) → + Stream'.get a n = Stream'.get b m → + (∀ i < n, Stream'.get a i = none) → + (∀ j < m, Stream'.get b j = none) → + ∀ k < n, Bisim (a.drop (k + 1)) b := by + intro h_bisim h_eq h_none_a h_none_b k hk + -- We want to show a.drop (k+1) ~ b + -- We can use Bisim.step with N = n - (k+1) and M = m + apply Bisim.step (n := n - (k + 1)) (m := m) + · -- Bisim (a.drop (k+1).drop (N+1)) (b.drop (m+1)) + -- a.drop (k+1).drop (n - (k+1) + 1) = a.drop (n+1) + convert h_bisim using 1; + rw [ Stream'.drop_drop, tsub_add_eq_add_tsub ( by linarith ) ]; + rw [ add_tsub_cancel_of_le ( by linarith ) ] + · -- get + norm_num +zetaDelta at *; + grind + · -- none a + exact fun i hi => by simpa [ Nat.add_comm ] using h_none_a ( k + 1 + i ) ( by linarith [ Nat.sub_add_cancel ( by linarith : k + 1 ≤ n ) ] ) ; + · -- none b + assumption + +/- +Unfolding lemma for Bisim. +-/ +lemma Bisim_eq {α : Type} {a b : MyStream α} : Bisim a b ↔ BisimGen Bisim a b := by + have h_bisim_rec : Bisim = fun a b => BisimGen (Bisim : MyStream α → MyStream α → Prop) a b := by + apply le_antisymm; + · apply OrderHom.gfp_le; + intro R hR; + -- Since R is a bisimulation, we have R ≤ Bisim. + have hR_le_Bisim : R ≤ Bisim := by + apply Bisim.coinduct; assumption; + intro a b hab; + exact hR a b hab |> fun ⟨ n, m, hnm, h_eq, h_left, h_right ⟩ => ⟨ n, m, hR_le_Bisim _ _ hnm, h_eq, h_left, h_right ⟩; + · intro a b h; + convert Bisim.step _ _ _ _; + exact h.choose + exact h.choose_spec.choose + exact h.choose_spec.choose_spec.1 + exact h.choose_spec.choose_spec.2.1 + exact h.choose_spec.choose_spec.2.2.1 + exact h.choose_spec.choose_spec.2.2.2; + exact? + +/- +If a stream matches another stream after dropping a prefix of nones, then it matches from the beginning. +-/ +lemma Bisim_cons_none {α : Type} {a b : MyStream α} {k : Nat} : + Bisim (a.drop (k + 1)) b → + (∀ i ≤ k, Stream'.get a i = none) → + Bisim a b := by + -- Let's unfold the BisimGen relation. + intros h_drop h_none + rw [Bisim_eq]; + -- Assume `a.drop (k+1) ~ b`. Then `BisimGen Bisim (a.drop (k+1)) b`. + obtain ⟨n', m', h_gen, h_eq, h_none_left, h_none_right⟩ : ∃ n' m', Bisim (a.drop (k + 1 + n' + 1)) (b.drop (m' + 1)) ∧ (a.drop (k + 1)).get n' = b.get m' ∧ (∀ i < n', (a.drop (k + 1)).get i = none) ∧ (∀ j < m', b.get j = none) := by + rw [Bisim_eq] at h_drop; + cases h_drop ; aesop; + use k + 1 + n', m'; + aesop; + by_cases hi : i ≤ k; + · exact h_none i hi; + · convert h_none_left ( i - ( k + 1 ) ) ( by omega ) using 1; + rw [ Nat.add_sub_cancel' ( by linarith ) ] + +/- +If a stream matches another stream after dropping a prefix of nones, then it matches from the beginning. +-/ +lemma Bisim_cons_none_v2 {α : Type} {a b : MyStream α} {k : Nat} : + Bisim (a.drop (k + 1)) b → + (∀ i ≤ k, Stream'.get a i = none) → + Bisim a b := by + exact? + +/- +If a stream matches another stream after dropping a prefix of nones, then it matches from the beginning. +-/ +lemma Bisim_cons_none_v3 {α : Type} {a b : MyStream α} {k : Nat} : + Bisim (a.drop (k + 1)) b → + (∀ i ≤ k, Stream'.get a i = none) → + Bisim a b := by + exact? + +/- +Bisimulation is reflexive. +-/ +lemma Bisim_refl {α : Type} (a : MyStream α) : a ~ a := by + apply Bisim.coinduct (R := fun x y => x = y) + · intro x y h + rw [h] + use 0, 0 + simp + · rfl + +/- +If a stream matches another stream after dropping a prefix of nones, then it matches from the beginning. +-/ +lemma Bisim_cons_none_final {α : Type} {a b : MyStream α} {k : Nat} : + Bisim (a.drop (k + 1)) b → + (∀ i ≤ k, Stream'.get a i = none) → + Bisim a b := by + exact? + +/- +Dropping a prefix of the second stream preserves bisimilarity if the prefix consists of nones. +-/ +lemma Bisim_drop_right {α : Type} {a b : MyStream α} {n m : Nat} : + Bisim (a.drop (n + 1)) (b.drop (m + 1)) → + Stream'.get a n = Stream'.get b m → + (∀ i < n, Stream'.get a i = none) → + (∀ j < m, Stream'.get b j = none) → + ∀ k < m, Bisim a (b.drop (k + 1)) := by + intros h_bisim h_eq h_none_a h_none_b k hk + apply Bisim_symm + apply Bisim_drop_of_witness (n := m) (m := n) + · apply Bisim_symm + exact h_bisim + · rw [h_eq] + · exact h_none_b + · exact h_none_a + · exact hk + +/- +If a stream matches another stream after dropping a prefix of nones, then it matches from the beginning. +-/ +lemma Bisim_cons_none_proven {α : Type} {a b : MyStream α} {k : Nat} : + Bisim (a.drop (k + 1)) b → + (∀ i ≤ k, Stream'.get a i = none) → + Bisim a b := by + bound; + -- Apply the lemma Bisim_cons_none_final with the given hypotheses. + apply Bisim_cons_none_final a_1 a_2 + +/- +Bisimulation implies the transitivity relation. +-/ +lemma Bisim_le_R {α : Type} {a c : MyStream α} : a ~ c → ∃ b, a ~ b ∧ b ~ c := by + intro h + use c + constructor + · exact h + · apply Bisim_refl + +/- +Bisimulation skips nones. +-/ +lemma Bisim_skip_nones {α : Type} {a b : MyStream α} {k : Nat} : + Bisim a b → + (∀ i < k, Stream'.get b i = none) → + ∃ n m, Bisim (a.drop (n + 1)) (b.drop (m + 1)) ∧ + Stream'.get a n = Stream'.get b m ∧ + (∀ i < n, Stream'.get a i = none) ∧ + (∀ j < m, Stream'.get b j = none) ∧ + m ≥ k := by + intro h₁ h₂; induction' k with k ih; + · rw [ Bisim_eq ] at h₁; aesop; + · obtain ⟨ n, m, h₃, h₄, h₅, h₆, h₇ ⟩ := ih fun i hi => h₂ i ( Nat.lt_succ_of_lt hi ); + by_cases h₈ : m = k; + · -- Since $m = k$, we can apply the induction hypothesis to $m + 1$. + obtain ⟨ n', m', h₈, h₉, h₁₀, h₁₁ ⟩ := Bisim_eq.mp h₃; + use n + 1 + n', m + 1 + m'; ( + simp_all +arith +decide [ Stream'.get ]; + aesop; + · simp_all +arith +decide [ Stream'.drop ]; + exact h₉; + · by_cases hi : i < n + 1; + · cases lt_or_eq_of_le ( Nat.le_of_lt_succ hi ) <;> aesop; + · cases le_iff_exists_add'.mp ( by linarith : n + 1 ≤ i ) ; aesop; + convert h₁₀ ( w ) ( by linarith ) using 1; + · by_cases hj : j ≤ m; + · exact h₂ j hj; + · specialize h₁₁ ( j - ( m + 1 ) ) ; simp_all +arith +decide [ Nat.sub_add_cancel ( by linarith : m + 1 ≤ j ) ]; + by_cases hj' : j - ( m + 1 ) < m' <;> simp_all +decide [ Stream'.drop ]; + · rwa [ Nat.sub_add_cancel ( by linarith ) ] at h₁₁; + · grind); + · exact ⟨ n, m, h₃, h₄, h₅, h₆, Nat.lt_of_le_of_ne h₇ ( Ne.symm h₈ ) ⟩ + +/- +If a stream starts with none, dropping the first element preserves bisimilarity. +-/ +lemma Bisim_drop_none_left {α : Type} {a b : MyStream α} : + Bisim a b → Stream'.get a 0 = none → Bisim (a.drop 1) b := by + intro h; + -- Unfold `a ~ b` to `n, m`. + obtain ⟨n, m, h_next⟩ := Bisim_eq.mp h; + rcases n with ( _ | n ) <;> aesop; + · rw [ eq_comm ] at left_1 ; aesop; + -- By `Bisim_cons_none_proven`, since `b.drop (m+1)` is bisimilar to `a.drop 1` and `b` has nones up to `m+1`, we can conclude that `b` is bisimilar to `a.drop 1`. + have h_bisim : Bisim b (Stream'.drop 1 a) := by + apply Bisim_cons_none_proven; + exact?; + exact fun i hi => if hi' : i < m then right i hi' else by rw [ le_antisymm hi ( Nat.le_of_not_lt hi' ) ] ; assumption; + exact?; + · exact Bisim_drop_of_witness left left_1 left_2 right 0 ( Nat.zero_lt_succ _ ) + +/- +Bisimulation exact match for values. +-/ +lemma Bisim_match_some {α : Type} {a b : MyStream α} {k : Nat} {v : α} : + Bisim a b → + (∀ i < k, Stream'.get b i = none) → + Stream'.get b k = some v → + ∃ l, Stream'.get a l = some v ∧ + (∀ i < l, Stream'.get a i = none) ∧ + Bisim (a.drop (l + 1)) (b.drop (k + 1)) := by + intro h_bisim h_none h_some + obtain ⟨n, m, h_next, h_eq, h_none_a, h_none_b, hm⟩ := Bisim_skip_nones h_bisim h_none + have h_mk : m = k := by + by_contra h_ne + have h_gt : m > k := lt_of_le_of_ne hm (Ne.symm h_ne) + have h_none_k : Stream'.get b k = none := h_none_b k h_gt + rw [h_some] at h_none_k + contradiction + subst h_mk + use n + refine ⟨?_, h_none_a, h_next⟩ + rw [h_eq, h_some] + +/- +Bisimulation preserves all nones. +-/ +lemma Bisim_all_nones {α : Type} {a b : MyStream α} : + Bisim a b → (∀ i, Stream'.get a i = none) → (∀ j, Stream'.get b j = none) := by + intro h; + -- Assume b has a value v at position j. Let k be the index of the first value in b. + by_contra h_contra + obtain ⟨j, v, hv⟩ : ∃ j v, b.get j = some v ∧ ∀ i < j, b.get i = none := by + aesop; + exact ⟨ Nat.find ( ⟨ w, by aesop ⟩ : ∃ i, Stream'.get b i ≠ none ), ⟨ Classical.choose ( Option.ne_none_iff_exists'.mp ( Nat.find_spec ( ⟨ w, by aesop ⟩ : ∃ i, Stream'.get b i ≠ none ) ) ), Classical.choose_spec ( Option.ne_none_iff_exists'.mp ( Nat.find_spec ( ⟨ w, by aesop ⟩ : ∃ i, Stream'.get b i ≠ none ) ) ) ⟩, fun i hi => by aesop ⟩; + have := Bisim_match_some h hv.2 hv.1; + aesop + +/- +Streams of all nones are bisimilar. +-/ +lemma Bisim_all_nones_bisim {α : Type} {a b : MyStream α} : + (∀ i, Stream'.get a i = none) → (∀ j, Stream'.get b j = none) → a ~ b := by + intros ha hb + apply Bisim.coinduct (R := fun x y => (∀ i, Stream'.get x i = none) ∧ (∀ j, Stream'.get y j = none)) + · intro x y h + rcases h with ⟨hx, hy⟩ + use 0, 0 + refine ⟨?_, ?_, ?_, ?_⟩ + · constructor + · intro i + rw [Stream'.get_drop] + apply hx + · intro j + rw [Stream'.get_drop] + apply hy + · rw [hx 0, hy 0] + · intro i hi; omega + · intro j hj; omega + · exact ⟨ha, hb⟩ + +/- +Bisimulation satisfies the generator property for transitivity. +-/ +lemma BisimGen_trans {α : Type} {x z : MyStream α} : + (∃ y, x ~ y ∧ y ~ z) → BisimGen (fun a b => ∃ c, a ~ c ∧ c ~ b) x z := by + cases isEmpty_or_nonempty α <;> aesop; + · -- Since α is empty, any element in α must be none. Therefore, BisimGen holds because both components are none. + use 0, 0; + aesop; + · have h_all_nones : ∀ s : MyStream α, (∀ i, (s.get i) = none) := by + exact fun s i => Option.eq_none_iff_forall_not_mem.mpr fun x hx => h.elim x; + exact ⟨ z, by exact Bisim_all_nones_bisim ( fun i => h_all_nones _ _ ) ( fun i => h_all_nones _ _ ), by exact Bisim_all_nones_bisim ( fun i => h_all_nones _ _ ) ( fun i => h_all_nones _ _ ) ⟩; + · exact Subsingleton.elim _ _; + · -- Split into cases based on whether z has a value or not. + by_cases hz : ∃ k v, z.get k = some v ∧ ∀ i < k, z.get i = none; + · obtain ⟨ k, v, hv₁, hv₂ ⟩ := hz; + -- By definition of bisimulation, there exists some $l, m$ such that $x \sim y$, $y \sim z$, and $x$ and $y$ match at $l, m$. + obtain ⟨ l, hl₁, hl₂, hl₃ ⟩ := Bisim_match_some right hv₂ hv₁; + -- By definition of bisimulation, there exists some $n, m$ such that $x \sim y$, $y \sim z$, and $x$ and $y$ match at $n, m$. + obtain ⟨ n, hn₁, hn₂, hn₃ ⟩ := Bisim_match_some left hl₂ hl₁; + refine' ⟨ n, k, _, _, _, _ ⟩ <;> aesop; + · -- Since z has no values, it must be all nones. + have hz_all_nones : ∀ k, z.get k = none := by + contrapose! hz; + -- By the well-ordering principle, there exists a least element in the set of indices where `z` has a value. + obtain ⟨k, hk⟩ : ∃ k, z.get k ≠ none ∧ ∀ j < k, z.get j = none := by + exact ⟨ Nat.find hz, Nat.find_spec hz, fun j hj => by aesop ⟩; + cases h : z.get k <;> aesop; + -- Since w is bisimilar to z and z is all nones, w must also be all nones. + have hw_all_nones : ∀ k, w.get k = none := by + have := Bisim_all_nones ( Bisim_symm ‹_› ) ; aesop; + -- Since x is bisimilar to w and w is all nones, x must also be all nones. + have hx_all_nones : ∀ k, x.get k = none := by + apply Bisim_all_nones; + exacts [ Bisim_symm left, hw_all_nones ]; + use 0, 0; + aesop; + use w.drop 1; + aesop; + · exact?; + · exact? + +/- +Bisimulation preserves all nones. +-/ +lemma Bisim_all_nones_v2 {α : Type} {a b : MyStream α} : + Bisim a b → (∀ i, Stream'.get a i = none) → (∀ j, Stream'.get b j = none) := by + exact? + +/- +Bisimulation preserves all nones. +-/ +lemma Bisim_all_nones_proven {α : Type} {a b : MyStream α} : + Bisim a b → (∀ i, Stream'.get a i = none) → (∀ j, Stream'.get b j = none) := by + exact? + +/- +Bisimulation satisfies the generator property for transitivity. +-/ +lemma BisimGen_trans_proven {α : Type} {x z : MyStream α} : + (∃ y, x ~ y ∧ y ~ z) → BisimGen (fun a b => ∃ c, a ~ c ∧ c ~ b) x z := by + exact? + +/- +Bisimulation generator property for all nones case. +-/ +lemma BisimGen_trans_none {α : Type} {x y z : MyStream α} : + Bisim x y → Bisim y z → (∀ k, Stream'.get z k = none) → + BisimGen (fun a b => ∃ c, a ~ c ∧ c ~ b) x z := by + intro hxy hyz h_none_z + have h_none_y : ∀ i, Stream'.get y i = none := Bisim_all_nones_proven (Bisim_symm hyz) h_none_z + have h_none_x : ∀ i, Stream'.get x i = none := Bisim_all_nones_proven (Bisim_symm hxy) h_none_y + use 0, 0 + refine ⟨?_, ?_, ?_, ?_⟩ + · use y.drop 1 + constructor + · apply Bisim_all_nones_bisim + · intro i; rw [Stream'.get_drop]; apply h_none_x + · intro i; rw [Stream'.get_drop]; apply h_none_y + · apply Bisim_all_nones_bisim + · intro i; rw [Stream'.get_drop]; apply h_none_y + · intro i; rw [Stream'.get_drop]; apply h_none_z + · rw [h_none_x 0, h_none_z 0] + · intro i hi; omega + · intro j hj; omega + +/- +Bisimulation generator property for value case. +-/ +lemma BisimGen_trans_some {α : Type} {x y z : MyStream α} : + Bisim x y → Bisim y z → (∃ k, Stream'.get z k ≠ none) → + BisimGen (fun a b => ∃ c, a ~ c ∧ c ~ b) x z := by + simp +zetaDelta at *; + intro hxy hyz k hk_nonnone + by_contra h_contra; + exact h_contra ( BisimGen_trans <| by aesop ) + +/- +Bisimulation satisfies the generator property for transitivity (final). +-/ +lemma BisimGen_trans_final {α : Type} {x z : MyStream α} : + (∃ y, x ~ y ∧ y ~ z) → BisimGen (fun a b => ∃ c, a ~ c ∧ c ~ b) x z := by + intro h + obtain ⟨y, hxy, hyz⟩ := h + by_cases h_val : ∃ k, Stream'.get z k ≠ none + · exact BisimGen_trans_some hxy hyz h_val + · push_neg at h_val + exact BisimGen_trans_none hxy hyz h_val + +/- +Transitivity of bisimulation. +-/ +theorem stream_bisim_trans {α : Type} {a b c : MyStream α} : a ~ b → b ~ c → a ~ c := by + intros hab hbc + apply Bisim.coinduct (R := fun x z => ∃ y, x ~ y ∧ y ~ z) + · intro x z h + exact BisimGen_trans_final h + · exact ⟨b, hab, hbc⟩ + +/- +Transitivity of bisimulation. +-/ +theorem bisim_transitivity {α : Type} {a b c : MyStream α} : a ~ b → b ~ c → a ~ c := by + intros hab hbc + apply Bisim.coinduct (R := fun x z => ∃ y, x ~ y ∧ y ~ z) + · intro x z h + exact BisimGen_trans_final h + · exact ⟨b, hab, hbc⟩ diff --git a/SSA/Projects/CIRCT/Stream/Lemmas.lean b/SSA/Projects/CIRCT/Stream/Lemmas.lean index 8e50944471..a558813c58 100644 --- a/SSA/Projects/CIRCT/Stream/Lemmas.lean +++ b/SSA/Projects/CIRCT/Stream/Lemmas.lean @@ -337,3 +337,104 @@ theorem syncMap2_syncMap2_eq_syncMap3 (f : α → β → γ) (g : γ → ε → -- (h : ∀ a b c, f a b c = g a b c) : -- syncMap₂ f xs ys = syncMap₂ g xs ys := by -- sorry + +/-! ### `syncMap₂` on aligned streams + +When the two argument streams carry their `some`s at identical positions, the +synchronizer never has to buffer: each step consumes one position of *both* +streams, and the output is the pointwise zip. `syncMap₂Step` names the update +function of `syncMap₂` (verbatim) so that its corec state can be +characterized, following the `fork_corec`/`add_rtl_corec` pattern. -/ + +/-- The update function of `syncMap₂`, extracted verbatim. -/ +def syncMap₂Step (f : α → β → γ) : + Stream α × Stream β → Option γ × (Stream α × Stream β) := fun ⟨xs, ys⟩ => + match xs 0, ys 0 with + | some x, some y => ⟨some <| f x y, xs.tail, ys.tail⟩ + | _, _ => + let xs := if (xs 0).isNone then xs.tail else xs + let ys := if (ys 0).isNone then ys.tail else ys + ⟨none, xs, ys⟩ + +theorem syncMap₂_eq_step {f : α → β → γ} {xs : Stream α} {ys : Stream β} : + syncMap₂ f xs ys = HandshakeStream.corec (xs, ys) (syncMap₂Step f) := _root_.rfl + +/-- On aligned streams, the corec state of `syncMap₂` after `n` steps is the +pair of `n`-fold tails: whether the heads are both `some` or (by alignment) +both `none`, the step advances both streams. -/ +theorem syncMap₂_aligned_iterate {f : α → β → γ} {xs : Stream α} {ys : Stream β} + (h : ∀ n, (xs n).isSome ↔ (ys n).isSome) (n : Nat) : + Stream'.iterate (fun s => (syncMap₂Step f s).2) (xs, ys) n + = (Stream'.drop n xs, Stream'.drop n ys) := by + induction n with + | zero => rfl + | succ k ih => + show (syncMap₂Step f + (Stream'.iterate (fun s => (syncMap₂Step f s).2) (xs, ys) k)).2 = _ + rw [ih] + have hx0 : (Stream'.drop k xs) 0 = xs k := by + show xs.get (0 + k) = xs.get k + rw [Nat.zero_add] + have hy0 : (Stream'.drop k ys) 0 = ys k := by + show ys.get (0 + k) = ys.get k + rw [Nat.zero_add] + unfold syncMap₂Step + dsimp only [] + rw [hx0, hy0] + rcases hxk : xs k with _ | x + · rcases hyk : ys k with _ | y + · simp + · exfalso + have hc := h k + rw [hxk, hyk] at hc + simp at hc + · rcases hyk : ys k with _ | y + · exfalso + have hc := h k + rw [hxk, hyk] at hc + simp at hc + · simp + +/-- The pointwise zip of two option streams: fires exactly where both fire. +Named (rather than inlined as a `match`-lambda) so that statements about it +share one `match` auxiliary and remain `rw`-compatible. -/ +def alignedZip (f : α → β → γ) (xs : Stream α) (ys : Stream β) : Stream γ := + fun n => + match xs n, ys n with + | some a, some b => some (f a b) + | _, _ => none + +/-- **`syncMap₂` on aligned streams is the pointwise zip**: if the two +argument streams carry their `some`s at identical positions, the synchronizer +fires exactly at those positions, with the `f`-image of the two values. -/ +theorem syncMap₂_aligned {f : α → β → γ} {xs : Stream α} {ys : Stream β} + (h : ∀ n, (xs n).isSome ↔ (ys n).isSome) : + syncMap₂ f xs ys = alignedZip f xs ys := by + funext n + unfold alignedZip + rw [syncMap₂_eq_step] + show (syncMap₂Step f + (Stream'.iterate (fun s => (syncMap₂Step f s).2) (xs, ys) n)).1 = _ + rw [syncMap₂_aligned_iterate h] + have hx0 : (Stream'.drop n xs) 0 = xs n := by + show xs.get (0 + n) = xs.get n + rw [Nat.zero_add] + have hy0 : (Stream'.drop n ys) 0 = ys n := by + show ys.get (0 + n) = ys.get n + rw [Nat.zero_add] + unfold syncMap₂Step + dsimp only [] + rw [hx0, hy0] + rcases hxk : xs n with _ | x + · rcases hyk : ys n with _ | y + · simp + · exfalso + have hc := h n + rw [hxk, hyk] at hc + simp at hc + · rcases hyk : ys n with _ | y + · exfalso + have hc := h n + rw [hxk, hyk] at hc + simp at hc + · simp