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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
|
# Real RE demo - what the GSP does between entry and the first fault
* schema: `greeneye-re-demo/1`
* script: `harness/re_demo.py` (stdlib-only, no hardware/guest/module)
* firmware: `gsp-570.144.fwimage.bin` sha256 `2d1bb5c60b208cfd...`
* verdict: **PASS**
## Scenario
> What happens on the real GSP image between entry and the first fault/milestone, and what does the state tell us about boot?
## Answer
**q1_first_touch: the first MMIO is a 4-byte read of PA 0x2000000000000a00 at fw PC 0x4009014; it is the QEMU-documented first fault**
**q2_path: entry state is all-zero (no bootloader handoff modelled); the bootstrap builds the device PA with 5 arithmetic instructions (li/slli/addi/slli/addi), reads it, then runs the chip-ID comparison chain: 25 instructions recorded from entry until the halt at fw 0x4009070**
**q3_id_field: the read value's bits [28:20] are extracted (srli 20, andi 0x1ff) and compared against 354..360 (Turing) and 368 (Ampere); the image itself defines this as a chip-ID field**
**q4_dispatch: ID 354..360 dispatches to .tu10x_text at 0x4007000; ID 368 dispatches to .ga100_text at 0x4005000; any other value (including the lenient zero) falls to the fail-closed `j .` loop at 0x4009070**
**q5_next_blocker: with a Turing ID served, .tu10x_text programs CSRs 0x7c8-0x7cc (region descriptors) and enables mstatus FP/SIMD state, then builds the absolute link-time address 0x40070f8 and jumps to it; because the loader relocates segments but not absolute immediates, that jump lands outside RAM and faults - a relocation artifact, so the next rung needs a chip-ID device model plus load-at-link-address/alias translation**
## Baseline vs emulator (measured)
| side | method | wall s | what it answers |
|---|---|---:|---|
| baseline | `python3 -m greeneye.cli probe <image> --duration 1.0 (here run via harness.run_qemu_baseline, 0.5 s bound)` | 0.9495 | first fault only |
| baseline | manual static reading (estimate, floor estimate: ~90 instructions across .bootstrap + .tu10x_text + .ga100_text read by hand, dispatch table identified and correlated with the QEMU first-fault report; not measured in this run) | 600.0 | entry->fault path, by hand |
| baseline | total (conservative) | 600.9495 | full question |
| emulator | three recorded native sessions | 0.1251 | full question + evidence |
Per-session `wall_s` in the milestone table is the recorded run only; the emulator total includes session launch, repeat and report writing.
## Rung / milestone table
| run | first touch | stop/milestone | instructions | wall s | evidence |
|---|---|---|---:|---:|---|
| QEMU probe | 0x2000000000000a00 (fault) | fault, then mtvec=0 loop | - | 0.9495 | `harness/re_demo/sessions/qemu-probe` |
| native lenient (B0) | 0x2000000000000a00 | halt loop fw 0x4009070 | 25 | 0.0006 | `harness/re_demo/sessions/native-lenient` |
| native modeled chip-ID (B1 candidate) | 0x2000000000000a00 | instruction fault at fw 0x40070f8 (outside RAM) | 74 | 0.0004 | `harness/re_demo/sessions/native-modeled-id` |
## Frozen thresholds
| check | pass |
|---|---|
| answers_complete | True |
| deterministic_lenient_runs | True |
| emulator_wall_s | True |
| milestone_past_qemu | True |
| baseline_beat | True |
| pass | True |
Thresholds frozen 2026-10-03 before the run: emulator wall <= 120.0 s; 2 identical lenient runs; all 5 answers present; milestone past the QEMU point. Failure signal: any check false -> the run is a failed experiment and the feature is not claimed.
## Sessions (evidence)
| session | file | sha256 |
|---|---|---|
| qemu-probe | events.jsonl | `8c4dba8006a496d853c81ce9e2b16944cd27b8d6171c01777daa6e5738be02bc` |
| qemu-probe | session.json | `c7bf5e4d29f534160d660dadb81f81942faa17cbfb1941587c60dcf78180f56c` |
| qemu-probe | summary.md | `d141fa06d3e2d0603f3b99ad7603758e1fc14627aed74c6fe8a6ad22c56eb14b` |
| native-lenient | events.jsonl | `ccb568588738c0609071ee542c9b04f7bb2868ee8fae12c28b2bfc5d9343721b` |
| native-lenient | session.json | `ec5944adce4b823a3d6fd7d5aa6385fb5b61c2f9542c7221f46f328601c12c66` |
| native-lenient | summary.md | `b50820afa60c35da0d4701e54f9907d4b7090c52721e1ecf656942a41bcf44db` |
| native-lenient-repeat | events.jsonl | `2cd28b4da009447d70505cfbba59e9c1bf8bd277e3a7ea696e2690f54f66f756` |
| native-lenient-repeat | session.json | `fe21ed52c05436d0f7886dfeb0886ec1a11b25678e4d827db3b9e4009d2187e4` |
| native-lenient-repeat | summary.md | `357d95a664e33128a2a48da7ecfc058bdbbea56fae130557593fd59ff2efa597` |
| native-modeled-id | events.jsonl | `fdf0756c3543741b74c9267dc9e4d22156f43a4b54463ffbfb1671c327444515` |
| native-modeled-id | session.json | `5ae7eeff56a19ed7eea093a164a3a3738965b56c39f35a563db3ee93a2c90d39` |
| native-modeled-id | summary.md | `bd670d207d23079173b494a9be9f9a0e7d31a10a11f9dc48fb8a134888442d0b` |
## Disassembly of the entry prologue (from the lenient session memory read)
```
0x84009000: 0010029b addiw t0,zero,1
0x84009004: 03129293 slli t0,t0,49
0x84009008: 00128293 addi t0,t0,1
0x8400900c: 00c29293 slli t0,t0,12
0x84009010: a0028293 addi t0,t0,-1536
0x84009014: 0002a283 lw t0,0(t0)
0x84009018: 0142d293 srli t0,t0,20
0x8400901c: 1ff2f293 andi t0,t0,511
```
### Turing dispatch tail (from the modeled session memory read)
```
0x840070e4: 1e0002b7 lui t0,0x1e000
0x840070e8: 3002a073 csrs mstatus,t0
0x840070ec: 040072b7 lui t0,0x4007
0x840070f0: 0f828293 addi t0,t0,248
0x840070f4: 00028067 jalr zero,0(t0)
```
## Not verified (honest limits)
* the modeled chip-ID value is an assumption (the QEMU baseline faults before reading it); only the field position and the compared IDs are firmware evidence
* no timing/cycle claim: cycles are modeled (L2 not modelled, docs/06) and none are used in this answer
* L3 device environment is absent: the register's on-silicon semantics are inferred from firmware comparisons, not from a device model
* load-at-link-address and absolute-immediate relocation behaviour are not implemented; the B1 candidate fault is a relocation artifact of this harness
* watchpoints are not exercised on this path: the bootstrap performs no RAM data access before the fault (RAM watchpoints are exercised by harness/sim_qemu_line.py on the demo firmware)
* no hardware, GPU, mdev, module, guest or network involvement by design
## Reproduce
```bash
cd open-iov/debug/risc-v-gsp-rm-vm
python3 harness/re_demo.py
```
## Re-run contract
* thresholds live in harness/re_demo.py (FROZEN_THRESHOLDS) and are not moved after the run
* the QEMU baseline needs qemu-system-riscv64; without it the emulator columns still reproduce and the baseline is marked unverified
* sessions are under harness/re_demo/sessions/ (hash-stamped); the report regenerates with the same command
|
