The MMB file format

April 28, 2022 · View on GitHub

Warning: This spec has not yet stabilized. If you are interested in writing a verifier for this spec you should stay appraised for changes to the spec.

The .mmb file format is a binary format for compactly expressing proofs that can be verified by checkers like mm0-c. The details of this format will eventually become part of the formal proof of correctness of a verifier based on mm0-c. This verifier reads an .mm0 file (using the MM0 file format) and a companion .mmb file, and checks that the proofs in the .mmb file are correct and align with the .mm0 theorem statements.

Encoding and types

All numbers are expressed in little endian fixed width types. Some tables require 4 or 8 byte alignment, but the proof stream is 1 byte aligned.

u8: a 1 byte unsigned integer
u16: a 2 byte unsigned integer
u32: a 4 byte unsigned integer
u64: an 8 byte unsigned integer
u1: a bit, used in bit packing descriptions
u7: sorts are 7 bits, so the high bit is used to encode additional information.
[T; n]: a list of exactly n elements of type T
p32<T>: a 32 bit pointer to T, relative to the start of the file
p64<T>: a 64 bit pointer to T, relative to the start of the file
p32?<T> / p64?<T>: a nullable pointer. If the value is zero then it is null, else it is a pointer to T
str4: a fixed length 4 byte string
cstr: a UTF-8 null terminated string
(cmd, data): see below

Command pairs are denoted (cmd, data) and use a variable length encoding, from 1 to 5 bytes. The low six bits of the first byte are cmd, while the high two bits give the number of data bytes:

00xxxxxx: cmd = x, data = 0
01xxxxxx yyyyyyyy: cmd = x, data = y (1 byte data field)
10xxxxxx yyyyyyyy yyyyyyyy: cmd = x, data = y (2 byte data field)
11xxxxxx yyyyyyyy yyyyyyyy yyyyyyyy yyyyyyyy: cmd = x, data = y (4 byte data field)

The file header contains basic information about the format and pointers to the other tables in the file, and starts at the first byte of the file.

sizeof(header) = 40; align(header) = 8; header =

Field	Type	Description
`magic`	`str4 = "MM0B" = 0x42304D4D`	Indicates that this file uses MMB format
`version`	`u8 = 1`	Indicates the version of the MMB format in use; this document details version `1`.
`num_sorts`	`u8`	The number of sorts in the file.
`reserved`	`u16`	Reserved, should be set to `0`.
`num_terms`	`u32`	The number of `term` and `def` in the file.
`num_thms`	`u32`	The number of `axiom` and `theorem` in the file.
`p_terms`	`p32<[term; num_terms]>`	The pointer to the term table.
`p_thms`	`p32<[thm; num_thms]>`	The pointer to the theorem table.
`p_proof`	`p32<proof_stream>`	The pointer to the proof stream.
`reserved2`	`u32`	Reserved, should be set to `0`.
`p_index`	`p64?<index>`	The pointer to the index.
`sorts` (*)	`[sort_data; num_sorts]`	The sort table.

(*) The sorts field is not included in the header for the purpose of sizeof(header).

Sort Table

The sort table comes directly at the end of the header, and is a list of sort_data = u8 items that give the sort modifiers for each of the sorts.

Bit	Modifier
0	`pure`
1	`strict`
2	`provable`
3	`free`
4-7	unused, set to 0

See mm0.md for a description of the sort modifiers.

Term Table

The term table is an array [term; num_terms] where term is as follows:

sizeof(term) = 8; align(term) = 8; term =

Field	Type	Description
`num_args`	`u16`	The number of arguments of the term constructor
`ret_sort`	`u7`	The sort of the return type.
`is_def`	`u1`	The high bit of `ret_sort` is `1` if this is a `def`.
`reserved`	`u8`	Reserved, should be set to `0`.
`p_data`	`p32<term_data>`	Pointer to additional information.

The p_data field points to additional data term_data for a term that cannot fit in these 8 bytes. Note that this data structure depends on the num_args and is_def fields of the relevant entry in the term table.

sizeof(term_data) varies; align(term_data) = 8; term_data =

Field	Type	Description
`args`	`[arg; num_args]`	The arguments
`ret`	`arg`	The return type
`unify` (optional)	`p32<unify_stream>`	The unify stream, only present if `is_def = 1`

The type arg = u64 contains a bit array for storing the dependencies of a sort.

sizeof(arg) = 8; align(arg) = 8; arg =

Field	Type	Description
`deps`	`[u1; 55]`	Bit `i` is 1 if this arg depends on the `i`th bound variable
`reserved`	`u1`	Must be `0`. (reserved for extensions to allow >55 deps)
`sort`	`u7`	The sort of the type
`bound`	`u1`	True if this is a bound variable

Note that bound variables must depend only on themselves in deps, i.e. the ith bound variable should have deps = 1 << i. Also, the indexing of bound variables in deps skips non-bound variables, but otherwise matches the ordering of the args array. A non-bound variable cannot depend on bound variables that are declared later in the list.

The ret field of the term_data does not use bound and sets it to 0; also ret_sort must agree with ret.sort.

Theorem Table

The theorem table is an array [thm; num_thms] where thm is as follows:

sizeof(thm) = 8; align(thm) = 8; thm =

Field	Type	Description
`num_args`	`u16`	The number of (expression) arguments of the theorem
`reserved`	`u16`	Reserved, should be set to `0`.
`p_data`	`p32<thm_data>`	Pointer to additional information.

The p_data field points to additional data thm_data for a theorem that cannot fit in these 8 bytes. Note that this data structure depends on the num_args field of the relevant entry in the theorem table.

sizeof(thm_data) varies; align(thm_data) = 8; thm_data =

Field	Type	Description
`args`	`[arg; num_args]`	The arguments
`unify`	`p32<unify_stream>`	The unify stream

The interpretation of args is the same as in the term table.

Unify Stream

Definitions, axioms, and theorems contain a pointer to unify_stream, which is an unaligned list of (cmd, data) pairs (see Encoding and types) which continues until cmd = END = 0. The valid commands in a unify stream (which are 6 bit opcodes) are:

Name	Value	`data`	Summary (*)
`UTerm`	`0x30`	`term_id`	Apply term `term_id`
`UTermSave`	`0x31`	`term_id`	Apply term `term_id`, and save this subterm to the heap
`URef`	`0x32`	`heap_id`	Refer to heap element `heap_id`
`UDummy`	`0x33`	`sort_id`	Create a new dummy with sort `sort_id`, apply and save it (only in `def`)
`UHyp`	`0x36`	`0`	Start reading a new hypothesis (only in `theorem`/`axiom`)
`END`	`0x00`	`0`	Not a command, signals the end of the stream

(*) The summary column is not a complete description of the behavior of the command. See Unification for the full stack machine semantics.

The operations are written in "polish notation", where a term constructor like UTerm t comes before the subterms. At the beginning of the unify stream, the heap is initialized with the variables in the order of declaration at indexes 0..num_args, but the heap grows every time a UTermSave or UDummy operation is encountered, and is assigned the next available index.

Since a term is "saved" before the contents of the term are read, cyclic terms are representable in this encoding; for example UTermSave 0, URef 0 is the term x = (t0 x). Cyclic terms are not legal in MMB files.

For definitions, the unify stream encodes the value of the definition. For theorems and axioms, the unify stream has the pattern UHyp, <h1>, UHyp, <h2>, ..., UHyp, <hn>, <concl> for a theorem with n hypotheses, where each <hi> is the encoding of the hypothesis expression and <concl> is the encoding of the conclusion expression.

The END terminator is redundant because it is possible to predict the end of the stream, since each UTerm[Save] must be followed by num_args subexpressions, URef and UDummy have no subexpressions, and UHyp has two subexpressions (the first hypothesis and the remainder of the hypotheses and conclusion). A unify stream that terminates too early or too late is malformed.

To permit read-ahead, the END terminator must begin at least 5 bytes prior to the end of the file. This is generally not a problem since unify streams are usually in the middle of the file.

Proof Stream

The proof stream contains the proofs of all the theorems that have been declared in the term and theorem tables. It is an unaligned stream of (cmd, data) pairs like the unify stream, but it has a two-level structure to enable fast scanning through the file.

The first command in the stream is a statement, and the data field is a relative pointer that gives the number of bytes from the start of this statement to the start of the following statement.

The valid statements are:

Name	Value	Has proof stream?	Description
`Sort`	`0x04`	No	Declares a new `sort`
`Term`	`0x05`	No	Declares a new `term`
`Def`	`0x05`	Yes	Declares a new `pub def` (*)
`LocalDef`	`0x0D`	Yes	Declares a new `def`
`Axiom`	`0x02`	Yes	Declares a new `axiom`
`Thm`	`0x06`	Yes	Declares a new `theorem`
`LocalThm`	`0x0E`	Yes	Declares a new `local theorem`
`END`	`0x00`		Not a statement, signals the end of the stream

(*) Note that Term and Def have the same value; this is because the actual indication of whether this is a term or def is by looking at the is_def field in the term table.

The verifier keeps track of how many sort, term/def, and axiom/theorem items have been encountered, and each occurrence of a statement from each of these classes increments the respective counter, with the new index being the index into the sort, term, or theorem tables, respectively. All references to terms with an ID larger than the running count (i.e. forward references) are considered to be invalid.

For statements that do not have a proof stream, the next command will be the next statement (and the data field for the statement will be the byte length of that single command). For statements that do have a proof stream, the next command will be a sequence of proof commands ending at END, and the data field will point immediately following the END.

To permit read-ahead, the END terminator denoting the end of the last statement must begin at least 5 bytes prior to the end of the file. This is potentially an issue if the file has no debugging index, since then the proof stream will be the last thing in the file and 4 bytes of padding need to be added.

The valid proof commands are:

Name	Value	`data`	Summary (*)
`Term`	`0x10`	`term_id`	Apply term `term_id`
`TermSave`	`0x11`	`term_id`	Apply term `term_id`, and save this subterm to the heap
`Ref`	`0x12`	`heap_id`	Put heap element `heap_id` on the stack
`Dummy`	`0x13`	`sort_id`	Create a new dummy with sort `sort_id`, apply and save it
`Thm`	`0x14`	`thm_id`	Apply theorem `thm_id`
`ThmSave`	`0x15`	`thm_id`	Apply theorem `thm_id`, and save it to the heap
`Hyp`	`0x16`	`0`	Add the expression just constructed as a hypothesis
`Conv`	`0x17`	`0`	Apply the conversion rule `e1 = e2 /\ proof e2 -> proof e1`
`Refl`	`0x18`	`0`	Reflexivity conversion `e = e`
`Sym`	`0x19`	`0`	Symmetry of conversion `e1 = e2 -> e2 = e1`
`Cong`	`0x1A`	`0`	Congruence `e1 = e1' /\ ... /\ en = en' -> t es = t es'`
`Unfold`	`0x1B`	`0`	Unfolding: `e = e' -> D es = e'` if `D es` unfolds to `e`
`ConvCut`	`0x1C`	`0`	Prove a conversion `e1 = e2`
`ConvSave`	`0x1E`	`0`	Save a conversion `e1 = e2` to the heap
`Save`	`0x1F`	`0`	Save an element on the stack to the heap without popping it
`Sorry`	`0x20`	`0`	Push a proof of anything, or a conversion (**)
`END`	`0x00`	`0`	Not a command, signals the end of the stream

(*) The summary column is not a complete description of the behavior of the command. See Proof checking for the full stack machine semantics.

(**) The Sorry command is not a valid proof command, but is useful for generating partial proofs. Verifiers are permitted to not recognize its existence.

The proof commands construct a proof in reverse polish notation (meaning that constructors follow their arguments) as follows:

Definitions construct the value of the definition expr e on the stack. (This is redundant with the unify stream encoded in the term table, but by checking one against the other we can ensure no cyclic terms.)
Axioms and theorems first construct each hypothesis and then use Hyp to add them to the hypothesis list, and then axioms construct expr concl and theorems construct proof concl.

There is no difference between local and public theorems/defs in terms of verification, but sorts, terms, axioms, public theorems, and public defs require reading the next statement in the MM0 file and ensuring that it matches the current statement in the MMB file. Local theorems and local defs do not require any corresponding statement in the MM0 file.

Proof Checking

The proof stream is a sequence of commands that are designed to operate on a stack machine with the following components:

S: The (main) stack, which starts empty and on which most commands operate. The valid stack elements are:
- expr e or e: e is an expression
- proof e or |- e: e is a proven expression
- e1 = e2: A conversion proof
- e1 =?= e2: A conversion obligation
H: The heap, which is initialized to the list of all the variables, and can contain all kinds of stack elements except e1 =?= e2.
HS: The list of hypotheses to the current theorem, which starts empty and grows on Hyp commands.
next_bv: The number of active bound variables, which is initialized to the number of bound variables in the declaration and is incremented on Dummy calls

The backing store is not mentioned explicitly in the description but holds the memory for all constructed s-expressions. In particular, operations like Term that allocate a new expression are considered distinct from any previously constructed expression, so equality testing, such as is required by the Refl command and in unification, is pointer equality, not structural equality. For example, Term 0, Term 0 constructs t0, t0' on the stack, but if these ended up in a reflexivity obligation t0 =?= t0' then a proof that applied Refl would not be valid. To actually get the same term twice it is required to use Save and Ref, as in TermSave(0), Ref(0) which puts t0, t0 on the stack.

During operation, we pre-calculate certain metadata about allocated expressions:

bound(e) is true if e is a bound variable (a variable with args[i].bound = true), or a dummy variable. All composite expressions have bound(t ...) = false.
sort(e) is the sort of the expression
V(e) is the set of variables in e
- V(xi) is {xi} if xi is a variable with bound(x)
- V(xi) is args[i].deps if xi is a variable
- V(t e1 ... en) is V(e1) ∪ ... ∪ V(en)
FV(e) is the set of free variables in e
- FV(xi) is the same as V(xi) on variables
- FV(t e1 ... en) is S1 ∪ ... ∪ Sn ∪ T where
  - if term[t].args[i].bound, Si = FV(ei)
  - otherwise Si is FV(ei) minus the union of FV(e[bv[j]]) over all j such that term[t].args[i].deps[j], and bv[j] is the j'th bound variable
  - T is the union of FV(e[bv[j]]) over all j such that term[t].ret.deps[j]

Because V is used only in theorem proofs and BV only in definitions, mm0-c will cache one or the other depending on which kind of statement is being proven.

The proof opcodes have the following operation on the state:

```
Term t: H; S, e1, ..., en --> H; S, (t e1 ... en)
```
Term t does the following:
- Look up term[t], which must be a valid term or def.
- Let n = term[t].num_args
- Pop e1, ..., en in reverse order (so e1 is deepest on the stack before the operation)
- For each argument ei, check that sort(ei) = term[t].args[i].sort, and if term[t].args[i].bound then bound(ei).
- Allocate (t e1 ... en) with sort(t e1 ... en) = term[t].ret_sort
- Push (t e1 ... en) on the stack
```
TermSave t = Term t, Save
TermSave t: H; S, e1, ..., en --> H, (t e1 ... en); S, (t e1 ... en)
```
TermSave t has exactly the same effect as Term t, Save. Specifically, it constructs the expression (t e1 ... en), and puts it on both the stack and on the heap.
```
Ref i: H; S, e1 =?= e2 --> H; S    (if H[i] = (e1 = e2))
Ref i: H; S --> H; S, H[i]         (otherwise)
```
Ref i does the following:
- Look up H[i], which should be in range of the heap.
- If H[i] = e or |- e, push it to the stack.
- If H[i] = (e1 = e2), pop e1 =?= e2 and ensure that the expressions match.
```
Dummy s: H; S --> H, x; S, x
```
Dummy s does the following:
- Look up sort[s], which must be a valid sort such that !sort[s].strict.
- Let x = var(next_bv) be a new bound variable, and increment next_bv
- Allocate x with sort(x) = s
- Push x on the stack and the heap
```
Thm T: H; S, e1, ..., en, e --> H; S', |- e
where Unify(T): S; e1, ..., en; e --> S'; H'; .
```
Thm T is only valid in proofs of axiom and theorem. Thm T does the following:
- Look up thm[T], which must be a valid axiom or theorem.
- Let n = thm[T].num_args
- Pop expression e
- Pop e1, ..., en in reverse order (so e1 is deepest on the stack before the operation)
- Initialize uheap := []
- For each argument ei:
  - check that sort(ei) = thm[T].args[i].sort
  - If thm[T].args[i].bound:
    - check that bound(ei).
    - check that FV(e') ∩ FV(ei) = {} for all e' in uheap
    - push FV(ei) to deps
  - Otherwise:
    - For each j such that thm[T].args[i].deps[j]:
      - check that deps[j] ∩ FV(ei) = {}
  - Push ei to uheap
- Run unification for thm[T].unify, with uheap as the original unification heap and with [e] on the unification stack. The unifier also has access to the main stack and may pop theorem hypotheses as necessary.
- Push |- e to the stack.
```
ThmSave T = Thm T, Save
```
ThmSave T has exactly the same effect as Thm T, Save. Specifically, it applies theorem T and puts the conclusion |- e on both the stack and on the heap.
```
Hyp: HS; H; S, e --> HS, e; H, |- e; S
```
Hyp is only valid in proofs of axiom and theorem. Hyp does the following:
- Pop e.
- Ensure that sorts[sort(e)].provable.
- Push e to the hypothesis list.
- Push |- e to the heap.

Conv: S, e1, |- e2 --> S, |- e1, e1 =?= e2

Pop |- e2, pop e1, push |- e1, push e1 =?= e2.

```
Refl: S, e =?= e --> S
```
- Pop e1 =?= e2, ensure that e1 and e2 are equal. (Reminder: this is O(1) pointer equality)
```
Symm: S, e1 =?= e2 --> S, e2 =?= e1
```
- Pop e1 =?= e2, push e2 =?= e1.
```
Cong: S, (t e1 ... en) =?= (t e1' ... en') --> S, en =?= en', ..., e1 =?= e1'
```
- Pop (t e1 ... en) =?= (t e1' ... en').
- Ensure that both expressions are term constructors for the same t.
- Push en =?= en, ..., e1 =?= e1. (Note that the obligations are pushed in reverse order.)
```
Unfold: S, (t e1 ... en) =?= e', e --> S, e =?= e'
where Unify(t): e1, ..., en; e --> H'; .
```
- Pop e.
- Pop (t e1 ... en) =?= e'.
- Ensure that t is a term constructor such that term[t].is_def.
- Run unification for term[t].unify, with [e1, ..., en] as the original unification heap and with [e] on the unification stack.
- Push e =?= e'.

ConvCut: S, e1 =?= e2 --> S, e1 = e2, e1 =?= e2

Pop e1 =?= e2, push e1 = e2, push e1 =?= e2.

ConvSave: H; S, e1 = e2 --> H, e1 = e2; S

Pop e1 = e2, push e1 = e2 to the heap.

```
Save: H; S, s --> H, s; S, s
```
- Pop any stack element s.
- Ensure s is not a convertibility obligation e1 =?= e2
- Push s to the heap and the stack.
```
Sorry: S, e -> S, |- e
Sorry: S, e1 =?= e2 -> S
```
Pop a stack element s:
- If s = e, push |- e to the stack.
- If s = (e1 =?= e2), do nothing.
- Record that Sorry was used. Verifiers that signal successful verification using exit codes are required to report failure for proofs using Sorry, although they can use implementation-defined printing to distinguish proofs-modulo-Sorry from malformed proofs.

Unification

Unification is called during proof checking, in the Unfold and Thm rules, as well as when verifying Def statements. The unifier uses the following state:

MS: The main stack (which was called S in the previous section) is consulted to get hypotheses, but is not otherwise used.
S: The unify stack, which contains expressions that have yet to be unified. Unification starts with a single expression on the unify stack, and it should be empty when unification is done.
H: The unify heap, which contains substitutions, and is extended by UDummy and UTermSave steps. It is initialized to the list of substitutions to the variables in the theorem or def.

The action of the unify commands is as follows:

```
URef i: H; S, H[i] --> H; S
```
- Pop e, ensure that e = H[i]. (Reminder: this is O(1) pointer equality)
```
UTerm t: S, (t e1 ... en) --> S, en, ..., e1
```
- Pop e.
- Ensure that e = (t e1 ... en) is a term constructor with head t.
- Push en, ..., e1. (Note that the expressions are pushed in reverse order.)
```
UTermSave t = USave, UTerm t
UTermSave t: H; S, (t e1 ... en) --> H, (t e1 ... en); S, en, ..., e1
```
UTermSave t has exactly the same effect as USave, UTerm t. Specifically, it pops the expression (t e1 ... en), puts it on the heap, and puts the subexpressions on the stack in reverse order.
```
UDummy s: H; S, x --> H, x; S
```
UDummy is only allowed in def declarations.
- Pop x.
- Ensure that x is a variable and sort(x) = s.
- Ensure that V(e) ∩ V(x) = {} for all e in H.
- Push x to the unify heap.
```
UHyp: MS, |- e; S --> MS; S, e
```
UHyp is only allowed in theorem declarations.
- Pop |- e from the main stack.
- Push e to the unify stack.
```
USave: H; S, e --> H, e; S, e
```
(USave is not an available opcode but is used to describe the operation of UTermSave.)
- Pop e, push e to the heap and the stack.

Debugging Index

The p_index field in the header points to an index which contains a list of index entries.

sizeof(index) varies; align(index) = 8; index =

Field	Type	Description
`num_entries`	`u64`	The number of index entries
`entries`	`[index_entry; num_entries]`	The index entries

Each index entry has a type which determines the meaning of the fields.

sizeof(index_entry) = 16; align(index_entry) = 8; index_entry =

Field	Type	Description
`type`	`str4`	The type of table
`data`	`u32`	Varies
`ptr`	`u64`	Varies

The collection of valid type settings is open-ended, but extensions should coordinate in order to avoid overlaps. The following table types are defined:

`type`	`data`	`ptr`	Description
`"Name" = 0x656D614E`	`0`	`p64<names>`	String names for sorts, terms, and theorems
`"VarN" = 0x4E726156`	`0`	`p64<var_names>`	String names for variables
`"HypN" = 0x4E726156`	`0`	`p64<hyp_names>`	String names for hypotheses

The `Name` table: names for statements

align(names) = 8; names =

Field	Type	Description
`sorts`	`[name_entry; num_sorts]`	The names of sorts
`terms`	`[name_entry; num_terms]`	The names of terms
`thms`	`[name_entry; num_thms]`	The names of theorems

Each name entry consists of a pointer to the statement in the proof stream where it was introduced, and a UTF-8 C string with the name. (MM0 itself doesn't support non-ASCII names, but the names listed here are allowed to include arbitrary unicode.)

sizeof(name_entry) = 16; align(name_entry) = 8; name_entry =

Field	Type	Description
`proof`	`p64?<proof_stream>`	A pointer to this statement in the proof stream
`name`	`p64?<cstr>`	A pointer to the name string

The `VarN` table: names for variables

align(var_names) = 8; var_names =

Field	Type	Description
`term_vars`	`[p64?<str_list>; num_terms]`	The list of variables in a `term`/`def`
`thm_vars`	`[p64?<str_list>; num_thms]`	The list of variables in a `axiom`/`theorem`

The str_list type is just a list of pointers to UTF-8 null-terminated strings:

sizeof(str_list) varies; align(str_list) = 8; str_list =

Field	Type	Description
`num_strs`	`u64`	The number of strings in the list
`strs`	`[p64?<cstr>; num_strs]`	A list of string pointers

The list term_vars[t] is the list of variable names in term[t] in the order of declaration, but the list continues past num_args to include the dummies, named by order of appearance of Dummy steps in the proof stream, which happens to coincide with the order of UDummy steps in the unify stream version. Similarly, the thm_vars[T] list gives the variable names in thm[T], including the dummy variables.

The `HypN` table: names for hypotheses

align(hyp_names) = 8; hyp_names =

Field	Type	Description
`thm_hyps`	`[p64?<str_list>; num_thms]`	The list of hypotheses in a `axiom`/`theorem`

The hyp_names table is similar to var_names, and reuses the str_list type. The list gives the names of hypotheses in the order of Hyp commands in the statement.