Build and run a program

Publish the SHA-256 specification and its entry points, then test, build and run them from an execution manifest.

The program in this tutorial computes the SHA-256 digests of nine test messages with Lema’s own SHA-256 specification, and prints each digest followed by ok or FAIL. By the end you will have tested it, built it and run it twice: once under lean --run and once as a native executable.

You need:

• Start a store and a server done, with the server running (the objects from tutorials 3 and 4 can stay in the store);
• a terminal at the root of your checkout, with ~/.lema/env and ~/lema-tutorial/env loaded, and the server’s terminal.

Read the manifest

An execution manifest describes a program built from accepted code. This one is committed in the repository:

{
  "schema": "lema.exec/v1",
  "doc": "Std.Sha256Spec's built-in vectors (lean/std/Sha256Exec.lean, report): one line per vector, the computed digest in hex and ok or FAIL. Sha256Spec.primes is a root because the whole specification is compiled and a native executable evaluates that constant at startup. Tested, not checked.",
  "entry": {"kind": "vectors", "root": "LemaDraft.Std.Sha256Exec.report"},
  "roots": {
    "LemaDraft.Std.Sha256Exec.report": "bb7485939d39dc8491500e529c17159333d7055132d8f5f461834b16ed96d200",
    "LemaDraft.Std.Sha256Spec.digest": "6e10cfbfa300ad372e777214525edc422c8a062a394de671aa3a1e36fbc6771b",
    "LemaDraft.Std.Sha256Spec.primes": "5af750af67badf65e8d41aea064c540384befe257742db3009d7c37d38871f4d"
  },
  "seeds": {"LemaDraft.Std.Sha256Spec.State": "5fef29f8204bdec70dbab76b393c5ed1d2dfddf25f67b495bc4823dc743c27bf"},
  "pieces": [
    {"source": "std/Sha256Spec.lean", "whole": true},
    {"source": "std/Sha256Exec.lean", "whole": true}
  ],
  "received": {
    "digest": "LemaDraft.Std.Sha256Spec.digest",
    "msg448": "LemaDraft.Std.Sha256Spec.msg448"
  },
  "profiles": {
    "NoCopySliceCall": [
      "LemaDraft.Std.Sha256Exec.report",
      "LemaDraft.Std.Sha256Spec.digest",
      "LemaDraft.Std.Sha256Spec.primes"
    ]
  },
  "backends": ["lean", "lean-native"],
  "seconds": 300,
  "expect": {"output_sha256": "5d56254e114e8d5bad83c62e6dc89b43b4bdaf9a93df60a2298162dbe62547dc"}
}

The main fields:

• entry is the program’s entry point. A vectors entry is a ByteArray constant, and its bytes are the program’s output.
• roots name the accepted objects the program is built from, by ID.
• pieces are the source files, under lean/, that are compiled to build them. received says which name each Received.* name in the pieces stands for.
• profiles asks the build to show a property of the compiled code. NoCopySliceCall says that no code the roots reach calls lean_byte_array_copy_slice, the copy behind extract and ++ on byte arrays.
• backends lists the two ways to build the program, and expect pins the SHA-256 of its output.

Execution manifests describes every field.

A build refuses any root that the store has not accepted. So before anything runs, your store must hold the three roots with exactly these IDs. You get them by publishing lean/std/Sha256Spec.lean and then lean/std/Sha256Exec.lean.

Publish the specification

The specification declares a structure, State, so its request carries a seed_salt. Every inductive type or structure gets a seed made from the salt and its name, and the seed is part of its identity. The salt lean/std/Sha256Spec gives the seed listed in the manifest’s seeds.

This publish takes longer than the earlier ones. The specification’s known-answer theorems, such as digest_abc, are proved by decide +kernel, so the pinned Lean 4.34.1 kernel computes each digest while it checks them.

jq -n --rawfile source lean/std/Sha256Spec.lean '{
  source: $source,
  prefix: "LemaDraft",
  seed_salt: "lean/std/Sha256Spec"
}' > ~/lema-tutorial/spec.json
lema --socket $SOCK call publish --params-file ~/lema-tutorial/spec.json > ~/lema-tutorial/spec-published.json
jq '.names["LemaDraft.Std.Sha256Spec.digest"], .names["LemaDraft.Std.Sha256Spec.msg448"]' ~/lema-tutorial/spec-published.json

{
  "id": "6e10cfbfa300ad372e777214525edc422c8a062a394de671aa3a1e36fbc6771b"
}
{
  "id": "eef2d043fe97973710a217e8c06f9cfc308c17b71a4d4424f6e0f97e1c9a2cfb"
}

These are the IDs of digest and msg448, which the next file receives. digest is also one of the manifest’s roots, with the same ID.

Publish the entry points

lean/std/Sha256Exec.lean receives digest and msg448 from the specification and defines the report:

/-- A vector's line: the digest in hex, then ` ok` or ` FAIL`, then a newline. -/
def line (digest expected : List UInt8) : List UInt8 :=
  hex digest ++ (if digest = expected then [0x20, 0x6f, 0x6b] else [0x20, 0x46, 0x41, 0x49, 0x4c]) ++ [0x0a]

/-- The `vectors` entry point: one line per built-in vector. -/
def report : ByteArray :=
  ⟨(vectors.flatMap fun v => line (Received.digest v.1) v.2).toArray⟩

Bind the two received names to the IDs that the specification’s publication returned, and publish:

jq -n --rawfile source lean/std/Sha256Exec.lean \
  --slurpfile spec ~/lema-tutorial/spec-published.json '$spec[0].names as $n | {
  source: $source,
  prefix: "LemaDraft",
  bindings: {
    "Received.digest": $n["LemaDraft.Std.Sha256Spec.digest"],
    "Received.msg448": $n["LemaDraft.Std.Sha256Spec.msg448"]
  }
}' > ~/lema-tutorial/exec.json
lema --socket $SOCK call publish --params-file ~/lema-tutorial/exec.json > ~/lema-tutorial/exec-published.json

The answer goes to exec-published.json, which the next step reads.

Check the IDs against the manifest

Compare the ID of the report you published with the root that the manifest names:

jq -r '.names["LemaDraft.Std.Sha256Exec.report"].id' ~/lema-tutorial/exec-published.json
jq -r '.roots["LemaDraft.Std.Sha256Exec.report"]' lean/exec/sha256-vectors.json

bb7485939d39dc8491500e529c17159333d7055132d8f5f461834b16ed96d200
bb7485939d39dc8491500e529c17159333d7055132d8f5f461834b16ed96d200

They match, so the entry you published is the object the manifest names. The other two roots, digest and primes, came from the specification.

Stop the server

lema test and lema build open the store themselves and need its lock, so stop the server first: press Ctrl-C in the server’s terminal. The store keeps everything you published. While the server runs, both commands refuse with the store at … is in use.

Test the program

lema test builds the program once for each backend the manifest lists, runs each build in the sandbox, and compares the outputs:

lema test --manifest lean/exec/sha256-vectors.json --store $STORE --runtime $CONFIG --name sha-test > ~/lema-tutorial/test-report.json
jq '{status, agree, expected, claim}' ~/lema-tutorial/test-report.json

{
  "status": "passed",
  "agree": true,
  "expected": "matched",
  "claim": "tested: the outputs of one manifest's accepted closure, compiled for each backend and run in the sandbox, compared byte for byte (and with the manifest's expected output, if any); the compilers, interpreter, linker, runtime and OS are assumed; nothing here is a proof"
}

The two backends are lean, a compiled module run by lean --run (its code is interpreted), and lean-native, an executable linked by the pinned distribution’s leanc. agree says that their outputs were the same, byte for byte, and expected says that they matched the manifest’s expected digest. If either comparison had failed, lema test would print the report as an error and exit with status 1. The claim says what the result means, in the words Lema uses for evidence.

The two artifacts are sha-test-lean and sha-test-lean-native, in the artifacts directory of your output. Artifact names must be new each time, so choose another --name if you run the test again.

The report holds the program’s output too:

jq -r .output ~/lema-tutorial/test-report.json

e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855 ok
ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad ok
248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1 ok
cf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1 ok
9f4390f8d30c2dd92ec9f095b65e2b9ae9b0a925a5258e241c9f1e910f734318 ok
7d3e74a05d7db15bce4ad9ec0658ea98e3f06eeecf16b4c6fff2da457ddc2f34 ok
ffe054fe7ae0cb6dc65c3af9b61d5209f439851db43d0ba5997337df154668eb ok
31eba51c313a5c08226adf18d4a359cfdfd8d2e816b13f4af952f7ea6584dcfb ok
2f3d335432c70b580af0e8e1b3674a7c020d683aa5f73aaaedfdc55af904c21c ok

The lines are the digests of the empty message, abc, NIST’s 448-bit and 896-bit messages, and runs of 55, 63, 64, 119 and 120 as.

Build and run it

lema build makes one artifact, by default with the first backend the manifest lists, lean:

lema build --manifest lean/exec/sha256-vectors.json --store $STORE --runtime $CONFIG --name sha-vectors | jq '{status, backend, guarantees}'

{
  "status": "built",
  "backend": "lean",
  "guarantees": [
    {
      "profile": "NoCopySliceCall",
      "verdict": "holds"
    }
  ]
}

Before it writes the artifact, lema build makes sure that the roots compile to exactly the objects the store accepted. The compiled code they reach must also follow Lema’s rules for executables (no panic, for example) and hold every requested profile, which guarantees reports. Build a native executable has the details.

Run the artifact:

lema run --runtime $CONFIG --artifact sha-vectors

lema run first makes sure that every file of the artifact still has its recorded hash. Then it runs the program in the sandbox, with no network, and prints its output: the same nine lines as above. A summary line ending in (tested execution) goes to standard error.

Now run the native executable that lema test built. It prints the same nine lines:

lema run --runtime $CONFIG --artifact sha-test-lean-native

Tested, not checked

Two kinds of evidence meet here. The specification’s theorems are checked: kernel replay accepted them, and for eight of the nine vectors (all but the 896-bit message) the kernel itself computed digest and confirmed the expected digest. The program’s output is tested. Lean’s compiler, and for the native build leanc with its C compiler and linker, turned the accepted code into something that runs, and what it printed was observed and compared. The compilers are assumed, so the nine ok lines are a test result, not a proof.

Checked, tested and assumed explains where each kind of evidence comes from.

Next

You have now published accepted code, reused a proof by its identity, and run a program built from accepted code. From here the how-to guides take one job at a time, such as building a native executable or releasing an artifact.