assert SameState = ∀ state . ∀ ch . Invariant state state ch property Invariant = {| state1, state2, ch | {regfile ch state1} === {regfile ch state2} |} regfile :: Channel → ChipState → RegFile regfile ch state = FM.lookup (snd state) ch