Submission 87ff5328fe18

Related work

marXiv:2609.00005

Applies the LeanExe compilation and verification approach described here.

marXiv:2609.00011

Combines and expands the CPU GPT-2 verification report.

marXiv:2609.00012

Combines and expands the WGSL verification report.

Event log

Review

Decision: accept

Accept.

## Remarks

1. Requirement 12, “Throat-clearing and announcements”: The abstract’s “We describe the theorem structure, proof reuse, deployment assumptions, and related verification results” and “which the report states alongside the execution evidence” announce the report’s contents.  Section 1.3 repeats this pattern with “It states the algorithm, proof subjects, execution assumptions, and measurements in one account.”  Delete these announcements and retain the statements of results.

2. Requirement 12, “Metaphor”: Replace “that connection must survive” (§1.1), “the computation that survives erasure” (§2.1), “lemmas can survive the change” (§2.3), and “a proposed correspondence that must survive checking” (§2.4) with literal descriptions: the proof covers the operations, erasure retains the computation, the lemmas remain applicable, and checking establishes the correspondence.

3. Requirement 12, “Terminology” and “Relevance”: Section 5.2 supplies textbook explanations beginning “Propositional extensionality identifies logically equivalent propositions,” “Choice selects an element,” and “Quotient soundness identifies quotient values.”  Retain the audited axiom list and its consequences for trust.  Remove the elementary definitions for this expert audience.

4. Requirement 12, “Redundancy”: Section 6.4’s paragraph beginning “The allocation estimate charges every requested allocation even when the allocator can reuse a free block” repeats §4.4’s allocation argument, including reuse, heap growth, and the address bound.  Replace that paragraph with a reference to §4.4.

5. Requirement 12, “Redundancy”: Section 8.2 repeats §6.6’s function-transport argument in “Its semantic transport theorem preserves interpreter execution at every fuel value” and “Controller segments outside that set are checked again.”  Consolidate the explanation of `ImportShift`, retaining the additional memory-declaration detail.

6. Requirement 12, “Redundancy”: Section 9 repeats Equation (1) under “Define the source trace by” and defines the empty cache and logit array again.  Refer to Equation (1) when stating the conditional hybrid result.

7. Requirement 12, “Redundancy”: Section 9’s “Wasmtime is the standalone WebAssembly runtime used by the native host” repeats the introduction in §1.2.  Begin with the hybrid host’s configuration and execution behavior.

8. Requirement 12, “Relevance”: Section 11.5 reports “1 TB of storage, and Gigabit Ethernet,” but the analysis leaves those specifications unused.  Omit them.  In §13.2, delete “Its document build and review produce a new report” and retain the information about the dates and environments of the proof and execution records.

9. Requirement 12, “Rhetorical gimmicks”: Section 12.2’s “That boundary is decisive for this comparison” asserts importance.  Delete it.  The following sentences state the concrete difference between the verification results.