Hash, freeze commit, and axiom-source hashes recorded alongside the commit,
since the file cannot contain its own hash. Also corrects the log's standing
claim that soundness cannot be known by construction — unconditioned soundness
cannot; operational soundness relative to a declared kernel can, which is what
proof assistants have always done.
Next arm named and not begun: reduction before generation, because reduction is
the only arm that can falsify the kernel.
David F Glidden
899d157026