Example Walkthrough
This walkthrough shows how to use a combination of DAMFaware edge systems to verify and subsequently publish the following assertion:
Theorem. For \(n \in \mathbb{N}\), \(\kop{fib}(n) = n^2\) if and only if \(n \in \{0, 1, 12\}\), where \(\kop{fib}(n)\) stands for the \(n\)th Fibonacci number defined as: \(\kop{fib}(0) \triangleq 0\), \(\kop{fib}(1) \triangleq 1\), and \(\kop{fib}(n + 2) \triangleq \kop{fib}(n + 1) + \kop{fib}(n)\).
In the if direction, the assertion is fairly easy to prove in any system that can support inductive definitions such as \(\kop{fib}\) in the first place: one just has to compute \(\kop{fib}(0)\), \(\kop{fib}(1)\), and \(\kop{fib}(12)\) and verify that they are indeed \(0\), \(1\), and \(144\), respectively. The only if direction, on the other hand, requires the ability to reason about the growth of the Fibonacci function with respect to the quadratic function \(n \mapsto n^2\). In particular, one needs the following lemma:
Lemma. For \(n \in \mathbb{N}\), if \(n \ge 13\), then \(\kop{fib}(n) > n^2\).
This walkthrough will perform this verification task using the following heterogeneous collection of systems:
 Abella DAMF for the overall theorem
 Coq to prove the lemma
 λProlog to illustrate how to incorporate logic programming
Setup
1. Local IPFS client
DAMF is built on top of IPFS and IPLD, so you will need an IPFS client. For
this walkthrough we will use the Dispatch intermediary, which
requires the Kubo desktop program accessed via
the command ipfs
.
You will also need to create your local IPFS repository, usually stored under
$HOME/.ipfs
or a similar folder. This is done by issuing the following
command: ipfs init
.
$ ipfs init
generating ED25519 keypair...done
peer identity: 12D3KooWNEsJFEp4FM14o9zedmFpBohUA4jPH77WYex75YP6mNHk
initializing IPFS node at /home/ExampleUser/.ipfs
to get started, enter:
ipfs cat /ipfs/QmQPeNsJPyVWPFDVHb77w8G42Fvo15z4bG2X8D2GhfbSXc/readme
IPFS Daemon
Running the IPFS daemon is optional for this walkthrough. You only need the daemon if you want to disseminate the assertions you publish into the IPFS network so that other people may use them. If you leave the daemon off, you will only be able to share assertions between programs that can access your local IPFS repository.
2. Dispatch, agent profile
In DAMF, all assertions are signed by exactly one agent. Concretely, an agent is a publicprivate key pair; the name of the agent is just its public key.
The Dispatch intermediate tool can be used to create an agent profile, which is just a humanreadable string that stands for an agent. Agent profile names are not globally shared using IPFS. Indeed, DAMF is completely unaware of agent profiles.
In this walkthrough, we will create an agent profile called
exampleAgent
. Install Dispatch by following the
instructions. In the rest of this tutorial,
we will use the command dispatch
to stand for whichever Dispatch executable is
relevant to your system. Next, run dispatch createagent
.
$ dispatch createagent exampleAgent
Agent profile exampleAgent created successfully!
$ dispatch listconfig  grep exampleAgent # (1)!
exampleAgent: {
name: 'exampleAgent',
 Just to verify that it worked.
Lemma in Coq
In order to follow along with this walkthrough, you should install Coq version 8.16.1.
3. Full proof
We begin with a traditional (autarkic) mode of usage of Coq, unmodified, without any connection to DAMF assertions.
As usual, we begin with importing the Arith
module to fix the interpretation
of numerals using the nat
type, and then capture \(\kop{fib}\) as the recursive
fixed point function fib
.
FibLemma.v  

1 2 3 4 5 6 7 8 9 10 11 

We will prove our lemma of interest using the lia
tactic of Coq, which is
enabled by the Lia
module. We will also pervasively use rewriting modulo
linear arithmetic identities, so we define a Ltac named liarw
for convenience.
FibLemma.v  

12 13 14 15 16 

Finally, here is our full proof of the lemma, which is named fib_square_above
here. This lemma itself makes use of a different lemma called fib_square_lemma
.
FibLemma.v  

17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 

4. Language and Tool objects
Let’s move on to representng fib_square_lemma
and fib_square_above
as DAMF
assertions.
To get there, we first have to turn Coq propositions into DAMF formula objects,
for which we will need to supply a suitable language
field. As there isn’t
(yet!) a universally agreed upon DAMF object to represent this language, we will
create one for the purposes of this walkthrough.
We start by creating a JSON object to represent the content
of what a “Coq
version 8.16.1” language object might contain. Here we could in principle link
to the reference manual that is distributed as part of the Coq 8.16.1
release. We could alternatively, or in addition, place the source or exceutable
code of a Coq parser. In this walkthrough, to simplify matters, we will
represent this language as the following JSON object that just links to the Coq
website.
Coq.language.content.json  

1 2 3 4 5 

We can then use dispatch createlanguage
to make the DAMF language object and
simultaneously give it a local humanreadable name, coq8.16.1
.
$ dispatch createlanguage coq8.16.1 json Coq.language.content.json
Language record coq8.16.1 created successfully!
If we want to see the DAMF object that was created by Dispatch, we can read its
languages.json
configuration file to get its CID, and then use ipfs dag get
to explore the contents of the linked objects in IPLD starting from that CID.
$ cat $HOME/.config/dispatch/languages.json
{"coq8.16.1":{"name":"coq8.16.1","language":"bafyreiayvr5klyi25dq2wrjqg2dwlgmxwsoxg2tcv7tdy675h5u7wtrxxy"}}
$ ipfs dag get bafyreiayvr5klyi25dq2wrjqg2dwlgmxwsoxg2tcv7tdy675h5u7wtrxxy # (1)!
{"content":{"/":"bafyreidmf3nxeigvi7mfklzu2wr7oapa7fodqdeajbxtngy5ax7cccmj5u"},"format":"language"}
$ ipfs dag get bafyreiayvr5klyi25dq2wrjqg2dwlgmxwsoxg2tcv7tdy675h5u7wtrxxy/content # (2)!
{"name":"Coq","url":"https://coq.inria.fr","version":"8.16.1"}
 This is the CID found in
languages.json
.  This is isomorphic to our
Coq.language.content.json
object.
We can record that we used Coq v.8.16.1 to verify our proofs of the assertions
by referencing a DAMF tool object in the mode
field of the corresponding
production. Like with the language object above, there isn’t currently a
standard DAMF tool object to represent this version of the Coq
implementation. Therefore, like with languages above, we will create the content
of such a tool object ourselves for the purposes of this walkthrough.
coq8.16.1.tool.content.json  

1 2 3 4 5 6 

To create the DAMF tool object, we use dispatch createtool
.
$ dispatch createtool coq8.16.1 json coq8.16.1.tool.content.json
Tool profile coq8.16.1 created successfully!
5. The DAMF assertions
There is currently no software that can transform the theorems we have just proved in Coq into DAMF assertions. We will do this manually. To cause the least breakage, we will reuse the text of the Coq development as much as possible.
Consider the first lemma, fib_square_lemma
. The formula content of this
lemma is the string "forall n, 2 * n + 27 <= fib (n + 12)"
. This string,
however, only makes sense in a context where the symbols *
, +
, <=
,
fib
, etc. are defined. These symbols come from the Coq standard prelude with
some additional support from the Arith
module, except fib
which we defined
ourselves. Thus, the DAMF context object for this formula can be built with the
following input for Dispatch:
1 2 3 4 5 6 7 8 

 This is the local name we picked using
dispatch createlanguage
in step 4.  Lines 3–11 of
FibLemma.v
.
In order to build the assertion that corresponds to fib_square_lemma
, Dispatch
expects the formulas and contexts to be laid out using local names. Here, we can
use the name fib_square_lemma
as the local name of the formula, and
fib_square_lemma!context
as the local name of its context. Then, in the
production underlying the assertion we use the local name coq8.16.1
for the
mode field, which is the local name of the DAMF tool object we created in step 4.
The complete assertion is as follows, again as a Dispatch input.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 

 We made this with
dispatch createagent
in step 2.  This defines a possible name for the assertion, but it only serves as a hint for consumers. The actual global name is the CID of the DAMF assertion object that Dispatch will create. This annotation object can have other metadata besides this name himt, such as the Coq proof script. Its structure is not prescribed by DAMF.
 This is the local name we picked using
dispatch createtool
in step 4.  This points to the formula object defined in the
"formulas"
section below (lines 16–20).  This points to the context object defined in the
"contexts"
section below (lines 23–29).
We can of course ask Dispatch to publish only this assertion. However, since we have two assertions in this file, it is more convenient for Dispatch to publish both assertions together as a DAMF collection. Here is what it looks like:
FibLemma.v.assertions.json  

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 

We can now use Dispatch to publish the entire collection at once.
$ dispatch publish FibLemma.v.assertions.json local # (1)!
Published DAMF collection object to local with cid: bafyreigdthmeok6gwsdulovqrgvzz4tbad2ifjxpa74dlpbfbt7ehnkyha
local
means that it is being published to the local IPFS repository we set up in step 1.
This CID can be explored in IPLD explorer. It can also be locally
explored with ipfs dag get
:
$ ipfs dag get bafyreigdthmeok6gwsdulovqrgvzz4tbad2ifjxpa74dlpbfbt7ehnkyha  python m json.tool # (1)!
{
"elements": [
{
"/": "bafyreicpwpxl3xe4nefsqc3f2rdxiedxjbmekh25m5cgqkriwp3qsivope"
},
{
"/": "bafyreigscd65tb2rabcpjxbep7h4lklbyfenmj32ioond7ouhh7qpvkh7a"
}
],
"format": "collection",
"name": "FibLemma.v"
}
$ ipfs dag get bafyreic53degjxdfn7e2l3spleevftr5pxemr7ydspkvwimr4smhjqjzuy/elements/0/claim/production/sequent/conclusion/content
"forall n, 2 * n + 27 <= fib (n + 12)"
python m json.tool
is being used to prettyprint the JSON
Computations with λProlog
Another way of building assertions is by means of a computational engine. Here we will give the example of using λProlog to perform computations on natural numbers. Coq is of course more than capable of doing these computations by itself, so the purpose of this section is mainly to illustrate how we can incorporate assertions from different sources.
6. Logic programming
Like with Coq earlier, let us quickly sketch how we are going to represent and
compute with natural numbers in λProlog. We declare nat
as a new type with the
kind
keyword in the signature, then declare two constants z
and s
as the
constructors of nat
. Note that λProlog operates under the open world
assumption, so there is no way to declare that these are the only two
constructors for nat
. The signature also declares three predicates, which
are constants with target type o
, which is the type of λProlog formulas.
Here are the signature (fib.sig
) and module (fib.mod
) files.
fib.sig  

1 2 3 4 5 6 7 

fib.mod  

1 2 3 4 5 6 7 8 

We will use the Teyjus implementation of
λProlog, which compiles a module (a .sig
/.mod
pair) to bytecode that can be
executed using a bytecode interpreter. To compile the above module fib
, we run:
$ tjcc fib && tjlink fib
Then, we can execute queries against fib
by using tjsim
.
$ tjsim fib
Welcome to Teyjus
⋮
[fib] ? fib (s (s (s (s (s (s z)))))) X.
The answer substitution:
X = s (s (s (s (s (s (s (s z)))))))
More solutions (y/n)? n
yes
[fib] ?
It is also possible to run tjsim
in batch (noninteractive) mode, where the
query is specified in the command line.
$ tjsim b m 1 s 'fib (s (s (s (s (s (s z)))))) X.' fib # (1)!
The answer substitution:
X = s (s (s (s (s (s (s (s z)))))))
 batch mode, maximum one solution, solve query
7. Exporting to DAMF
We use the following language and tool descriptions for λProlog and Teyjus (version 2.1.1):
lprolog.language.content.json  

1 2 3 4 

teyjus2.1.1.tool.content.json  

1 2 3 4 5 6 

$ dispatch createlanguage lprolog json lprolog.language.content.json
Language record lprolog created successfully!
$ dispatch createtool teyjus2.1.1 json teyjus2.1.1.tool.content.json
Tool profile teyjus2.1.1 created successfully!
To build the DAMF assertions, we can use the following harness module:
harness.sig and
harness.mod. The purpose of the harness
module is to turn a sequence of goals for a module FILE
, written in a file
FILE.goals
, into a JSON file FILE.json
that can be given to dispatch
publish
. Note that the agent, language, and tool names that we chose with
dispath createagent
, dispatch createlanguage
, and dispatch createtool
respectively, are directly written in the harness module.
To use the harness, we define a module main
that accumulates and compiles the
fib
and harness
modules.
main.sig  

1 2 3 4 

main.mod  

1 2 3 4 

The file fib.goals
is a list of goals, with each goal wrapped in a name using
the name
predicate. For our purposes, we can just list goals that compute
\(\kop{fib}(n)\) and \(n^2\) for \(n\) between 1 and 13.
fib.goals  

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 

Finally, here’s how we can run harness
, and subsequently Dispatch:
$ tjcc fib && tjcc harness && tjcc main && tjlink main
$ tjsim b s 'damf_export.' m 1 main
Wrote fib.json.
$ dispatch publish fib.json local # (1)!
Published DAMF collection object to local with cid: bafyreickai4hsl3aht53hz3veen5xlzvx7njy7sudsfpns3ikxtnuzpjha
 Can take a few dozen seconds to finish.
This CID can be explored on IPLD explorer or locally with ipfs dag get
.
Theorem in Abella DAMF
The assertions generated by Coq and λProlog will be used to prove the main theorem in Abella DAMF, which is a variant of the Abella theorem prover that can accept and publish DAMF assertions.
Abella is simply typed and its type system does not have any reasoning principles that yield theorems. Reasoning in Abella is done with its reasoning logic known as \(\mathcal{G}\), which is an extension of firstorder intuitionistic logic over \(\lambda\)terms that supports inductive and coinductive definitions, generic quantification (using \(\nabla\)), and nominal abstraction (a generalization of \(\alpha\beta\eta\) equality on \(\lambda\)terms).
8. Setting the stage
We will write the overall theorem in the Abella file
FibTheorem.thm. It begins by defining
the type nat
of natural numbers, its constructors z
and s
, and then some
comparison relations and computations. Note that all definitions in Abella are
relational: unlike Coq, we don’t define +
as a binary function on natural
numbers but as a ternary relation plus
that relates its first two arguments to
its third.
FibTheorem.thm  

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 

Because all inductive definitions are relational in Abella, we often need additional lemmas to establish that the relations behave like functions. In our theorem we will need the following lemmas of this kind.
FibTheorem.thm  

30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 

9. Importing DAMF assertions
Abella can import any DAMF assertion using the following statement:
Import "damf:<cid>".
Here, <cid>
can be the CID of an individual DAMF assertion object or a DAMF
collection object containing assertions. If these assertion objects are in
Abella’s own language, they can be used as is. For reference, Abella’s DAMF
language object has the following CID:
bafyreic7eqwwwbjtrbcz4fj33wdoyt6qext6ji46vggwjjliznyzvaymoy
What about the case of DAMF assertions in a different language? In this case,
Abella will need to use an adapter sequent as explained in the DAMF technical
design paper. In the future, such adapter
sequents will be built using language translation tools. For now, we will write
the adapter sequents ourselves and sign the resulting assertions using a mode
field of null
, which stands for an assertion for which the signing agent is
wholly responsible.
To create such adapter sequents, Abella has a modified form of the Import
... as
statement that allows the user to restate the theorem in Abella’s own
language. For example, the theorem fib_square_above
from Coq that was
exported in step 5 can be imported in Abella as follows:
FibTheorem.thm  

63 64 65 66 67 

The statement of this theorem needs to be comprehensible in the local context of
the Abella development, using the type nat
, constants s
and z
, and the
relations times
, fib
, lt
, etc. defined in lines 1–29 of
FibTheorem.thm.
Iterated application notation
The term s^13 z
stands for the term
(s (s (s (s (s (s (s (s (s (s (s (s (s z)))))))))))))
,
which is 13 in the unary representation of nat
. For any unary term
constant k
and literal number n
(\(\ge 0\)), the notation (k^n t)
stands for the n
times iterated application of k
to t
.
After typechecking the statement of the theorem, Abella uses this Import
... as
statement first to build the adapter sequent that has the following DAMF
structure:
{ "format": "assertion",
"claim": {
"format": "annotatedproduction",
"annotation": {
"name": "fib_square_above!adapter"
"generator": "damf:bafyreiegwjyj5f2lpw3ck35pqeqt45bwl57c7n7xfpbtxm6ym3sfsixixq" // (1)!
},
"production": {
"mode": null,
"sequent": {
"conclusion": "fib_square_above",
"dependencies": [
"damf:bafyreigscd65tb2rabcpjxbep7h4lklbyfenmj32ioond7ouhh7qpvkh7a/claim/production/sequent/conclusion" // (2)!
] } }
"formulas": {
"fib_square_above": {
"language": "damf:bafyreic7eqwwwbjtrbcz4fj33wdoyt6qext6ji46vggwjjliznyzvaymoy", // (3)!
"content": "forall x, nat x > … > lt y u",
"context": "fib_square_above!context"
} },
"contexts": {
"fib_square_above!context": {
"language": "damf:bafyreic7eqwwwbjtrbcz4fj33wdoyt6qext6ji46vggwjjliznyzvaymoy",
"content": [
"Kind nat type", "Type z nat", "Type s nat > nat",
"Define nat : …", "Define leq : …", "Define lt : …",
"Define times : …", "Define fib : …"
] } } }
 This field links to the DAMF tool object for this version of Abella. Because
it is part of an annotation, DAMF prescribes no particular meaning to the
"generator"
key or its value. Its purpose in this walkthrough is purely documentary in nature.  This uses IPLD paths to refer to the CID of the
conclusion
of the assertion object that was imported. It corresponds to the theorem namedfib_square_above
that we proved in Coq.  This is the Abella language’s identifier
This adapter sequent, which has a dependency on an external formula in a
different language (Coq) to the conclusion (Abella), will be published using
Dispatch. For the rest of the file, Abella then continues as if
fib_square_lemma
was indeed stated and proved in Abella.
The assertions produced using λProlog in step 7 are similarly imported using a
sequence of Import ... as
statements.
FibTheorem.thm  

68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 

10. Finishing the theorem
Assembling the final theorem in Abella is now straightforward. In the only if
direction (forward), we repeatedly make use of the computation assertions from
λProlog for \(n \in 0..12\), and then the fib_square_above
assertion for \(n \ge
13\). In the if direction, we just verify that the computations (again, pulled
from λProlog) have the right values.
FibTheorem.thm  

142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 

Verifying this in Abella requires the damfimports
command line
flag. Publishing the assertions also requires the damfpublish <location>
flag, where <location>
is either local
or cloud
.
$ abella damfimports damfpublish local FibTheorem.thm
Published as damf:bafyreifg3cosrvpidfmepwsjjt6kwvrlb2iobe5wo27sqsbu5uzbrdlvhm
As usual, this can be browsed in IPLD explorer.