Grammar of Constraints x

$⟨ v t er m ⟩ ::= ∣ ∣ ∣ ⟨ co n s t r ⟩ ::= ∣ ∣ ∣ ∣ ∣ ⟨ v a r ⟩ ⟨ v t er m ⟩ + ⟨ v t er m ⟩ ⟨ v t er m ⟩ - ⟨ v t er m ⟩ ⟨ v t er m ⟩ \times ⟨ v t er m ⟩ ⟨ v t er m ⟩ = ⟨ v t er m ⟩ ⟨ v t er m ⟩ \leq ⟨ v t er m ⟩ ⟨ v t er m ⟩ < ⟨ v t er m ⟩ \neg ⟨ co n s t r ⟩ ⟨ co n s t r ⟩ \land ⟨ co n s t r ⟩ ⟨ co n s t r ⟩ \lor ⟨ co n s t r ⟩$

where $⟨ v a r ⟩$ is a variable or a constant as described previously.

When a non-empty set of constraints is provided as part of a scenario, matching of messages, and thus variables, is done modulo these constraints.

For messages to match, the substitutions that result from the matching must keep the constraints set satisfiable, in which case we say the step is matched modulo this set of constraints.

Info

Deductions that can be made straightforwardly are propagated automatically, but there is no real solver at the moment (for instance there is no union-find structure for equalities). This is something that can be improved later on if these constraints turn out to be important for describing some scenarios.

Mitten - MITM proxy for the Tezos P2P network.

Grammar of Constraints x