New Code Proofs

def pairwiseDistinct (r₁ r₂ r₃ r₄ : UInt64) : Prop

Whether four register indices are pairwise distinct; a convenience predicate used to avoid repetition while writing the example Hoare triples.

Equations

• pairwiseDistinct r₁ r₂ r₃ r₄ = (r₁ ≠ r₂ ∧ r₁ ≠ r₃ ∧ r₁ ≠ r₄ ∧ r₂ ≠ r₃ ∧ r₂ ≠ r₄ ∧ r₃ ≠ r₄)

def code : Code

An example program of type Code, used to demonstrate referring to a named Code value inside a Hoare triple.

Equations

• code = mriscx first: li x 0, 2 li x 1, 0 la x 2, 291 end