		Search-engine friendly clone of the ACL2 documentation.

States

Addresses

Addresses.

Each validator has a unique address, which is an Aleo blockchain address of the form aleo1.... An address is essentially a public key; the validator uses the associated private key to sign data.

In our model, the details of these addresses are irrelevant, so we treat addresses as abstract entities. Our model only needs to compare addresses for equality.

Subtopics

Address-option: Fixtype of optional addresses.
Address: Fixtype of addresses.
Address-set: Fixtype of sets of addresses.