An invariant of the Tree Evaluation read machine

The invariant of Cslib.TreeEval.Reader.machine follows each phase separately: the header phases bound the parameters read so far, and the search phase bounds the candidate prime. After initialization, the machine has the correct parameters, well-formed registers, at most h frames with bounded rounds, and bounded counters. RunInv records bounds on the modulus p, not primality; the chosen prime is at most 4ℓ + 2.

Main definitions

• Cslib.TreeEval.Reader.Inv: the invariant.

Main results

• Cslib.TreeEval.Reader.primeFor_le: by Bertrand's postulate, the prime is at most 4ℓ + 2.
• Cslib.TreeEval.Reader.inv_run: every state reached on the encoding satisfies the invariant.

theorem Cslib.TreeEval.Reader.primeFor_le (ℓ : ℕ) : primeFor ℓ ≤ 4 * ℓ + 2

Bertrand's postulate bounds the prime: primeFor ℓ ≤ 4ℓ + 2.

def Cslib.TreeEval.Reader.RunInv (ℓ H : ℕ) (s : State) : Prop

The invariant of the procedure: the parameters read, a bounded modulus, well-formed registers, a stack of bounded depth with rounds below the modulus, and bounded counters.

def Cslib.TreeEval.Reader.Inv (ℓ H : ℕ) (s : State) : Prop

The invariant of the machine on an instance of value length ℓ and height H.

theorem Cslib.TreeEval.Reader.inv_run {ℓ H : ℕ} (T : Tree ℓ H) (j : ℕ) : Inv ℓ H (machine.run T.encode j).state

Every state reached on the encoding satisfies the invariant.