Mathematical Contract

Mathematical Contract

The Mathematical Contract in Svalinn is a formal specification that dictates system behaviour under all possible conditions.

Contract Definition

A contract C is defined as a tuple (S, I, T), where:

• S is the set of all possible system states.
• I is the set of invariant properties that must hold true in all states s in S.
• T is the state transition function T(s, a) -> s'.

Core Invariants

1. Non-Interference: High-security data must never influence low-security observable behaviour.
2. Provenance: Every state transition must be accompanied by a valid zero-knowledge proof of authorization.
3. Immutability of Audit: The append-only log cannot be modified or truncated.

Enforcement

These contracts are not merely documentation; they are translated into machine-readable specifications in the .machine_readable directory and enforced by the compiler plugin. Any code change that violates these invariants will fail to compile.