An example of content addressing Universes

As described on the Home page, one of the goals of this repository is to content-address every Lean 4 environment, declaration, expression, and universe level.

The use-cases and motivation for this procedure are described elsewhere, but in particular one would hope to be able to run ipfs dag get #bafyasdlalksdjcaoiweasdf... where #bafy... is some CID for a Lean constant, expression, etc. Then proceed to run radiya check #bafy... to type check the definition.

In particular, we want to encode Lean programs (and all that they constitute) into CIDs and assembled data structure that can be stored in an IPLD format. In order to achieve this we must in particular assign a unique CID to the universes that appear in a particular Lean environment.

In essence then we could define a datastructure

structure UnivCid where
  Cid : CID

and an associated tree of such CIDs:

inductive UnivCidDag where
  | Zero
  | Succ  : UnivCid → UnivCidDag
  | Max   : UnivCid → UnivCid → UnivCidDag
  | IMax  : UnivCid → UnivCid → UnivCidDag
  | Param : Name → Nat → UnivCidDag

The actual implementation is a little more complicated though. There are actually two separate data structures

inductive UnivAnon where
  | Zero
  | Succ  : UnivAnonCid → UnivAnon 
  | Max   : UnivAnonCid → UnivAnonCid → UnivAnon 
  | IMax  : UnivAnonCid → UnivAnonCid → UnivAnon 
  | Param : Nat → UnivAnon

which contains the computational content of the Lean program (here the Nat represents the De Bruijn index of the "bound" universe parameter) and

inductive UnivMeta where
  | Zero
  | Succ  : UnivMetaCid → UnivMeta 
  | Max   : UnivMetaCid → UnivCid → UnivMeta 
  | IMax  : UnivMetaCid → UnivMetaCid → UnivMeta 
  | Param : Name → UnivMeta

which is used for pretty-printing, and assembling the Lean environment.

An example of a situation where the distinction between UnivMeta and UnivAnon are important is that the two functions

universe u
def id (A : Sort (u + 1)) (x : A) : A := x

universe v
def id (A : Sort (v + 1)) (x : A) : A := x

will have the same UnivAnonCids, but importantly different UnivMetaCids if u and v elaborate to different values in an environment.