		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.... By `validator' we mean not only one in the committee, but any possible validator that may be in a committee; in fact, the committee is dynamic.

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.

In our model, addresses are also used to represent signatures: see our model of certificates.

Subtopics

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