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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
[]
= "sprawling-runtime"
= true
= true
= true
= true
= true
= true
= true
= "One run of a sprawling resident, from dispatch to freeze: turns, tools, replay and the sandbox that executes code."
[]
= "runtime"
[]
# An MCP image block carries its picture base64-encoded, and the
# connector step decodes it once to store the bytes (8-27-10).
= true
# Every process exec starts is configured by `child::command`: off the
# city's console, in a process group of its own, without the city's
# secrets (`crates/runtime/spec/Tools/Exec.lean` D96).
= { = true }
= { = true }
= { = true }
# A picture a tool answers with travels only if its sides are read from
# its own bytes; the same decoder the browser's screenshots are measured
# with (8-27-10).
= true
# File identity (volume and file index on Windows, device and inode
# elsewhere): `read` compares the handle it opened with the file now at
# the judged location, which std exposes only on unstable APIs.
= "1"
= true
= true
# The sieve's filter table is a TOML file in the reserved
# subtree, and its shape has one reader.
= true
# Execution boundary, on the 48 LTS line (upstream supports every twelfth
# release for 24 months and the others for two), no older than 48.0.6:
# 48.0.3 cleared RUSTSEC-2026-0314, -0315 and -0316, and 48.0.6 clears the
# advisories RustSec published on 2026-10-16 against the 48 line; the line
# already carries the path_open TRUNCATE bypass fix (GHSA-2r75-cxrj-cmph)
# and the hard-link/rename FilePerms bypass fix (CVE-2026-58494). The
# floor is stated here rather than left to the lockfile, so no update can
# step back below it (`crates/runtime/Spec.lean` §8-13). wasip1 only - there is no
# socket host implementation, which is the Python arm's mechanical proof
# that it cannot reach the network.
= { = "48.0.6", = true, = false, = ["cranelift", "runtime", "std"] }
= { = "48.0.6", = true }
# One Job Object per run, so a run's whole process tree can be read
# (`crates/runtime/Spec.lean` §8-13-3); the crate's public surface is safe.
[]
= { = true }
# Each run's job takes a weighted CPU share through the one FFI seam
# (`crates/runtime/spec/Tools/Exec.lean` D29).
= { = true }
# The MSVC discovery rustc and cc use, run outside the AppContainer that
# cannot read Visual Studio's instance state; already in the lock beneath
# cc (`crates/runtime/spec/Tools/Exec/NativeWindows.lean` D60).
= "0.1.14"
[]
= ["dep:wasmtime", "dep:wasmtime-wasi"]
= ["kernel/conformance"]
[]
= true
= true
= true
= true
# A10's three assertions are pinned with hand-written WAT so the gate
# needs no CPython artifact to run.
= "1"
[]
= true