exOS/commit.txt at main · umpolungfish/exOS · GitHub

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
41
42
43
44
45
46
Moved ancillary documents to ig-docs (2026-06-14)

3 files moved: POTENTIALITY.md → applications/os-kernel/,
SEFIROT_13_IMPLEMENTATION.md → applications/os-kernel/,
tex/manuscript.md → manuscripts/.
Kept: README.md, USAGE.md, all images/*.pdf, tex/exOS.pdf,
tex/ALEPH_ARCHITECTURE.pdf, markdown/*.md, all source code.

---

SNS_PRIME.md notation migration: O_inf→O_∞, O_0→O₀, O_1→O₁, O_2→O₂ (11 files)

---

ParaWASM engine: parser hardening + O(1) verify + clean-slate attestation (2026-05-30)
======================================================================================

Three operationalizations of observed session behaviors:

1. Parser hardening — malformed input → tag [N], not [T]
   - WasmInstr::I32Const(u64) / I64Const(u64) → parameterized with B4 tag
   - Command handler parses first whitespace-token only; parse failure → B4::N
   - [N]-tagged push increments non_designated_count; next verify → frob_invariant=F
   - Prevents injection-style multi-token payloads from contaminating [T] stack

2. O(1) verify fast-path — incremental non_designated_count
   - WasmState gains non_designated_count: usize (maintained on push and drop)
   - Verify short-circuits: if non_designated_count == 0, skip full O(n) scan
   - Proves lemma: Verified(s) ∧ Tag(v)=T ⟹ Verified(s·v) at zero runtime cost
   - Matches monotonic fixed-point preservation observed in session log

3. Clean-slate attestation — context-switch boundary gate
   - attest_clean_state(s: &WasmState) -> B4: B iff stack empty and invariant=B
   - WasmInstr::AttestClean + wasm attest shell command
   - WasmState.attest_result field records last attestation
   - WasmRuntime::format_attest() prints result for shell display
   - Operationalizes vacuous empty-stack verification as a formal cleanliness proof

Files changed:
  src/para_wasm.rs          — WasmInstr, WasmState, exec_one, attest_clean_state,
                              format_attest, demo updated
  src/para_wasm_commands.rs — parse hardening, attest command, help text

cargo build: clean

Author: Lando ⊗ ⊙perator