Lean's equivalence of TLA+'s CONSTANT

Stream: Program verification

[Ethan Hong]

What is the best way to express TLA+'s CONSTANTS in Lean 4?

The definition of CONSTANTS from Summary of TLA+:

CONSTANTS C1, . . . , Cn (1) Declares the Cj to be constant parameters (rigid variables). Each Cj is either an identifier or has the form C (_, . . . , _), the latter form indicating that C is an operator with the indicated number of arguments.

I found that there's a constant keyword in Lean 3, but seems like in Lean 4 it's just def (or axiom?) Specifically I was writing the proof for basic paxos and don't know how to best translate this line (e.g. Acceptors) from TLA+ to Lean.

From the TLA+ semantics, I think it might correspond more closely to 2 in the following:

import Mathlib
open Set

-- 1
variable (Acceptor : Type)
variable (Acceptors : Set Acceptor)

-- 2
variable (Acceptor1 : Type)
def Acceptors1 : Set Acceptor1 := {a: Acceptor1 | true}

However, I feel declaring it as a type variable would suffice, like the first code block in sec 2.1 of https://protocols-made-fun.com/lean/2025/04/25/lean-two-phase.html.

Thanks!

[Shreyas Srinivas]

You want to start with a DSL inside lean that supports this style of specification

[Shreyas Srinivas]

I suggest checking out Veil

[Ethan Hong]

Thanks, I saw Veil a while ago actually. I am more asking about if one was to write this in Lean, what would be the best way to do it?

I translated the proof for basic paxos from TLAPS to Lean, but wasn't so sure how to correctly write TLA+'s CONSTANT.
https://github.com/xinhong3/PaxosProofLean/blob/main/Paxos/Spec.lean#L14

[George Pîrlea]

@Ethan Hong The issue is that TLA+ is untyped, whereas Lean is typed, so it's non-trivial to encode the former into the latter.

If you want to be faithful, you can check how TLAPS encodes TLA+ into many-sorted first-order logic, as explained in Encoding TLA+ into unsorted and many-sorted first-order logic.

An alternative encoding is provided by the Apalache model checker. See TLA+ model checking made symbolic and follow-up papers for details on that.

[George Pîrlea]

This is quite a bit of effort that you'd only want to do if your goal is to embed TLA+ in Lean.

If you only care about verifying a specific protocol, it will definitely be easier to use a typed encoding specific for that protocol, or use a tool like Veil.

[Mario Carneiro]

embedding untyped into typed is easy, you just have everything in one type

[Mario Carneiro]

from what I know of TLA+'s axiomatics it should embed faithfully in lean

[Ethan Hong]

Appreciate all the help! I should clarify my question since the title is too generic.

Currently, the problem is protocol-specific. I am only looking at Basic Paxos.
I want to know (since there could be many ways) how to encode things such as (CONSTANT Acceptors) in Lean that's faithful to the TLA+ semantics. The TLA+ spec I am referring to is this.
So given the following in TLA+:

CONSTANT Acceptors

Would the following be a "good" translation in Lean that's faithful to the TLA+ semantics?

import Mathlib

variable (Acceptor : Type)
variable (Acceptors: Set Acceptor)

---

however, since Acceptors is a constant, should I use def instead of variable?

[George Pîrlea]

@Ethan Hong variable in Lean means that it's a parameter, not that it can be mutated, so that's a perfectly fine encoding.