Invariant in the proof of AllGoodAlg
Recall
assert AllGoodAlg = ∀ alg . GoodAlg alg
property GoodAlg =
{| alg | ∀ ws . ∀ regf .
StateIndependent {doPacket alg ws regf} |}
property StateIndependent =
{| m | ∀ s1 . ∀ s2 .
{fst (runS m s1)} === {fst (runS m s2)} |}
doPacket :: Alg → Data → RegFile → StateM Memory (Data,RegFile)
doPacket
as a whole is completely state (Memory) independent.
- The steps that comprise
doPacket
work on a packet stored in
memory, and can thus not be completely state independent.
- The invariant needs to capture that the algorithm only touches the part
of the memory where the packet is stored.