Develop basic seq/par correctness combinators
Created by: joaopizani
From @joaopizani on March 28, 2015 18:28
If a certain circuit c₁ is correct with regards to functional specification f₁ and another circuit c₂ is correct with regards to specification f₂, then c₁ ⟫ c₂ is correct with regards to f₂ ∘ f₁.
Similarly with c₁ ∥ c₂, but with the parallel interpretation.
Maybe we can find other interesting "basic" proof combinators for correctness, too.
Copied from original issue: joaopizani/piware#35