1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
;;; Copyright (c) 2026 Nicholas Vermeulen
;;; SPDX-License-Identifier: AGPL-3.0-or-later
;; proc.lisp — Phase B: replay-verified process runs over the proc-eval builtin
;; (Phase A). A run RECORD is data: (proc-run <code> <timeout> <result>).
;;
;; The audit: because a child is a fresh, isolated, deterministic interpreter,
;; re-executing the recorded code MUST reproduce the recorded result. Replay IS
;; the audit — now across a process boundary (mingjian's thesis for deterministic
;; plants, applied to isolated computations). A record that does NOT reproduce
;; is the honest signal that the run was non-deterministic (it read the clock,
;; the network, a changing file) and so cannot be replay-audited — never a false
;; 'verified.
;;
;; HONEST SCOPE (the caveat is the crack): replay proves the recorded CODE
;; produces the recorded RESULT. It does NOT prove the code is the code you
;; meant to run — forge both code and result together and the forgery replays
;; clean (the same limit mingjian names: replay needs an out-of-band anchor to
;; say "this is the run I kept", it can only say "this run is self-consistent").
;; Run code in an isolated child and KEEP the record (input + output as data).
;; Replay: re-execute the recorded code in a fresh child and compare.
;; 'verified | (diverged (claimed …) (got …))