-r--r--r-- 7103 holtrace-20250617/doc/html/verify.html raw
<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1">
<style type="text/css">
html{overflow-y:scroll;background-color:#505050}
body{font-family:"Noto Sans","Droid Sans","DejaVu Sans","Arial",sans-serif;line-height:1.5}
tt,code{background-color:#f0f0f0;font-family:"Noto Sans Mono","Droid Sans Mono","DejaVu Sans Mono","Courier New",monospace,sans-serif;font-size:1em;}
pre{margin-left:3em}
p,ul,ol,blockquote,pre{font-size:1.0em;line-height:1.6}
li p{font-size:1.0em}
blockquote p{font-size:1.0em}
h1{font-size:1.5em}
h2{font-size:1.3em}
h3{font-size:1.0em}
h1 a{text-decoration:none}
table{border-collapse:collapse}
th,td{border:1px solid black}
table a{text-decoration:none}
table tr{font-size:1.0em;line-height:1.6em}
table tr{font-size:1.0em;line-height:1.5}
tbody tr:nth-child(12n+1){background-color:#f0ffff}
tbody tr:nth-child(12n+2){background-color:#f0ffff}
tbody tr:nth-child(12n+3){background-color:#f0ffff}
tbody tr:nth-child(12n+4){background-color:#f0ffff}
tbody tr:nth-child(12n+5){background-color:#f0ffff}
tbody tr:nth-child(12n+6){background-color:#f0ffff}
tbody tr:nth-child(12n+7){background-color:#fffff0}
tbody tr:nth-child(12n+8){background-color:#fffff0}
tbody tr:nth-child(12n+9){background-color:#fffff0}
tbody tr:nth-child(12n+10){background-color:#fffff0}
tbody tr:nth-child(12n+11){background-color:#fffff0}
tbody tr:nth-child(12n+12){background-color:#fffff0}
.headline{padding:0;font-weight:bold;font-size:1.0em;vertical-align:top;padding-bottom:0.5em;color:#ffffff;background-color:#505050}
.navt{display:block;box-sizing:border-box;-moz-box-sizing:border-box;-webkit-box-sizing:border-box;margin:0;padding:0;vertical-align:center;font-size:1.0em}
.here{background-color:#505050}
.here{color:#ffffff}
.away{background-color:#505050}
.away a{text-decoration:none;display:block;color:#ffffff}
.away a:hover,.away a:active{text-decoration:underline}
.main{padding:5px}
.main{background-color:#ffffff}
.pagetitle{font-size:1.4em;font-weight:bold}
@media only screen and (min-width:512px) {
.fixed{margin:0;padding:0;width:160px;height:100%;position:fixed;overflow:auto}
.main{margin-left:170px}
}
</style>
<title>
HOLTrace: Verify</title>
</head>
<body>
<div class=fixed>
<div class=headline>
HOLTrace</div>
<div class="navt away"><a href=index.html>Intro</a>
</div><div class="navt away"><a href=download.html>Download</a>
</div><div class="navt away"><a href=install.html>Install</a>
</div><div class="navt away"><a href=test.html>Test</a>
</div><div class="navt away"><a href=save.html>Save</a>
</div><div class="navt away"><a href=prune.html>Prune</a>
</div><div class="navt here">Verify
</div><div class="navt away"><a href=tex.html>TeX</a>
</div><div class="navt away"><a href=ml.html>ML REPL</a>
</div><div class="navt away"><a href=prooftrace.html>ProofTrace</a>
</div><div class="navt away"><a href=format.html>Format</a>
</div><div class="navt away"><a href=license.html>License</a>
</div></div>
<div class=main>
<div class=pagetitle>HOLTrace: Verify</div>
<p>The recommended tool for verifying HOLTrace files
is <code>holtrace_restore</code>.
There are also some <a href="#experimental">experimental</a> tools.</p>
<p><code>holtrace_restore</code> is a command available in a new HOL Light session
after HOLTrace is <a href="install.html">installed</a>.
Running</p>
<pre><code>holtrace_restore !theorems "holtrace-12345.50"
</code></pre>
<p>will read and verify a trace file <code>holtrace-12345.50</code>,
while checking that the file matches
any preexisting name-theorem pairs
listed in HOL Light's built-in <code>!theorems</code> database.</p>
<p>On <a href="install.html"><code>rome1</code></a>,
restoring the pruned 37.5MB trace from <code>hol.ml</code>
takes 48 seconds, using about 400MB extra RAM.</p>
<p>Verification remembers named theorems from the file
(whether or not those are listed in <code>!theorems</code>),
and you can inspect those theorems
until they are erased by the next <code>holtrace_restore</code> run:</p>
<pre><code>holtrace_restore_name2thm "ONE_OR_PRIME";;
</code></pre>
<p>Verification uses the HOL Light kernel to apply inferences.
Verification checks constant definitions in the trace
against the kernel's <code>definitions()</code> list,
and checks type definitions in the trace
against the <code>holtrace_typedef_thms()</code> 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).</p>
<p>With more work to add bindings for new names and any related syntax,
it should be possible to use <code>holtrace_restore</code>
as a faster replacement for the normal loading of <code>hol.ml</code>
or of other HOL Light libraries.
There is also an even faster variant <code>holtrace_restore_skipthmchecks</code>
that should be suitable in this context,
taking only 24 seconds for <code>hol.ml</code>:
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.</p>
<h2 id="experimental">Experimental tools</h2>
<p>There are currently two experimental command-line tools for verifying traces.
First,
<code>holtrace-verify-simple</code> <em>tries</em> 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.</p>
<p>This tool is written in Python.
On <a href="install.html"><code>rome1</code></a>,
<code>holtrace-verify-simple</code>
takes 58.27 seconds and 821MB RAM
given the 37.5MB pruned <code>hol.ml</code> trace as input.
It takes 6.15 seconds and 125MB RAM
given the 2.4MB pruned <code>ONE_OR_PRIME</code> trace as input.</p>
<p>Second,
<code>holtrace-verify</code> <em>tries</em> to verify traces
and is more efficient than the HOL Light kernel.
Beware that this tool is even more likely than <code>holtrace-verify-simple</code>
to have soundness bugs
that let it accept false theorems:
the tool has had vastly less review than the HOL Light kernel
<em>and</em> is more complicated than <code>holtrace-verify-simple</code>.
Also, this tool currently rejects any substitution
producing multiple hypotheses that are different but alpha-equivalent.
Furthermore, unlike <code>holtrace-verify-simple</code>,
this tool currently does not check whether a name refers to multiple theorems.</p>
<p><code>holtrace-verify</code> is written in C
and is not necessarily safe to run on untrusted input.
A VM is recommended.</p>
<p>On <a href="install.html"><code>rome1</code></a>,
<code>holtrace-verify</code>
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 <code>ONE_OR_PRIME</code> pruned HOLTrace file as input.</p><hr><font size=1><b>Version:</b>
This is version 2025.06.16 of the "Verify" web page.
</font>
</div>
</body>
</html>