-rw-r--r-- 3398 holtrace-20250617/doc/verify.md raw
The recommended tool for verifying HOLTrace files
is `holtrace_restore`.
There are also some [experimental](#experimental) tools.

`holtrace_restore` is a command available in a new HOL Light session
after HOLTrace is [installed](install.html).
Running

    holtrace_restore !theorems "holtrace-12345.50"

will read and verify a trace file `holtrace-12345.50`,
while checking that the file matches
any preexisting name-theorem pairs
listed in HOL Light's built-in `!theorems` database.

On [`rome1`](install.html),
restoring the pruned 37.5MB trace from `hol.ml`
takes 48 seconds, using about 400MB extra RAM.

Verification remembers named theorems from the file
(whether or not those are listed in `!theorems`),
and you can inspect those theorems
until they are erased by the next `holtrace_restore` run:

    holtrace_restore_name2thm "ONE_OR_PRIME";;

Verification uses the HOL Light kernel to apply inferences.
Verification checks constant definitions in the trace
against the kernel's `definitions()` list,
and checks type definitions in the trace
against the `holtrace_typedef_thms()` list
(which is maintained by HOLTrace whether or not traces are being saved).
For a new definition,
verification checks whether the definition can be added to the kernel
(so verification is not stateless).

With more work to add bindings for new names and any related syntax,
it should be possible to use `holtrace_restore`
as a faster replacement for the normal loading of `hol.ml`
or of other HOL Light libraries.
There is also an even faster variant `holtrace_restore_skipthmchecks`
that should be suitable in this context,
taking only 24 seconds for `hol.ml`:
this variant skips checking whether the theorem statements
match the theorem statements in the trace,
but still runs all of the same inferences through HOL Light.

## Experimental tools {#experimental}

There are currently two experimental command-line tools for verifying traces.
First,
`holtrace-verify-simple` _tries_ to verify traces
in essentially the same way that the HOL Light kernel does.
Beware that this tool is likely to have soundness bugs
that let it accept false theorems:
the tool has had vastly less review than the HOL Light kernel.

This tool is written in Python.
On [`rome1`](install.html),
`holtrace-verify-simple`
takes 58.27 seconds and 821MB RAM
given the 37.5MB pruned `hol.ml` trace as input.
It takes 6.15 seconds and 125MB RAM
given the 2.4MB pruned `ONE_OR_PRIME` trace as input.

Second,
`holtrace-verify` _tries_ to verify traces
and is more efficient than the HOL Light kernel.
Beware that this tool is even more likely than `holtrace-verify-simple`
to have soundness bugs
that let it accept false theorems:
the tool has had vastly less review than the HOL Light kernel
_and_ is more complicated than `holtrace-verify-simple`.
Also, this tool currently rejects any substitution
producing multiple hypotheses that are different but alpha-equivalent.
Furthermore, unlike `holtrace-verify-simple`,
this tool currently does not check whether a name refers to multiple theorems.

`holtrace-verify` is written in C
and is not necessarily safe to run on untrusted input.
A VM is recommended.

On [`rome1`](install.html),
`holtrace-verify`
takes 1.12 seconds and 271MB RAM
given the 37.5MB pruned HOLTrace file as input.
It takes 0.08 seconds and 20MB RAM
given the 2.4MB `ONE_OR_PRIME` pruned HOLTrace file as input.