Skip to content

Commit 7de60ad

Browse files
committed
feat!: derive uarch cycle overflow from machine state
Regenerate the Solidity uarch transition and constants to make cycle overflow a state-preserving fixed point derived from uarch.cycle. Check overflow before halt, remove the encoded halt-reason constants, and update tests and replay artifacts for the new access order and break-reason precedence. Update emulator tag.
1 parent a2946b4 commit 7de60ad

7 files changed

Lines changed: 59 additions & 44 deletions

File tree

‎CHANGELOG.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,10 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
66

77
## [Unreleased]
88

9+
### Changed
10+
- Changed microarchitecture cycle overflow into a state-preserving fixed point derived from `uarch.cycle`
11+
- Changed microarchitecture cycle overflow to take precedence over halt
12+
913
## [0.14.0] - 2026-04-13
1014
### Added
1115
- Added `advanceStatus` to return advance status (accepted, rejected, exception)

‎Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ DOWNLOADDIR := downloads
44
SRC_DIR := src
55

66
EMULATOR_VERSION ?= v0.21.0
7-
EMULATOR_TAG ?= -test4
7+
EMULATOR_TAG ?= -test5
88

99
SOLIDITY_VERSION ?= 0.8.30
1010

‎helper_scripts/generate_EmulatorConstants.lua‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -28,8 +28,6 @@ out:write(' uint64 constant ROLLUP_LOG2_MAX_ADVANCE_STATES_PER_EPOCH = ' ..
2828
cartesi.ROLLUP_LOG2_MAX_ADVANCE_STATES_PER_EPOCH .. ';\n')
2929
out:write(' uint64 constant UARCH_HALT_ADDRESS = 0x' ..
3030
hex(cartesi.machine:get_reg_address("uarch_halt")) .. ';\n')
31-
out:write(' uint64 constant UARCH_HALT_HALTED = ' .. cartesi.UARCH_HALT_HALTED .. ';\n')
32-
out:write(' uint64 constant UARCH_HALT_CYCLE_OVERFLOW = ' .. cartesi.UARCH_HALT_CYCLE_OVERFLOW .. ';\n')
3331
out:write(' uint64 constant UARCH_PC_ADDRESS = 0x' .. hex(cartesi.machine:get_reg_address("uarch_pc")) .. ';\n')
3432
out:write(' uint64 constant UARCH_X0_ADDRESS = 0x' .. hex(cartesi.machine:get_reg_address("uarch_x0")) .. ';\n')
3533
out:write(' uint64 constant UARCH_SHADOW_START_ADDRESS = 0x' .. hex(cartesi.UARCH_SHADOW_START_ADDRESS) .. ';\n')

‎shasum-download‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,2 @@
1-
fc0090028ceed1e3e7d30e953a20b7d77708b3df705ea8ef9aba1e343997a32b downloads/machine-emulator-tests-data.deb
2-
f07140bbd5f1e1279d95fbe6fa31e7a9fc7e00c39eee7205aff9d4abae40fa33 downloads/uarch-riscv-tests-json-logs.tar.gz
1+
182c7a57481daa4076a488b1c3f0b8ba01d0271c267f79c9f5ecb947cac6bd50 downloads/machine-emulator-tests-data.deb
2+
79e0797c4a30c6a3f2523353006db0b8b99b6a6cdf17670634c6befa024905bf downloads/uarch-riscv-tests-json-logs.tar.gz

‎src/EmulatorConstants.sol‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -25,16 +25,14 @@ library EmulatorConstants {
2525
// START OF AUTO-GENERATED CODE
2626

2727
bytes32 constant UARCH_PRISTINE_STATE_HASH =
28-
0x05dda45cb12872b018f3857a528439b1d1100bcd3fa019a9745ad436de9a4698;
28+
0xfecd1447b18725c91ba909a13b3d059d3628a625f668ce991e6ab7c901a65d2c;
2929
uint64 constant UARCH_CYCLE_ADDRESS = 0x400008;
3030
uint64 constant UARCH_CYCLE_MAX = 0xfffff;
3131
uint64 constant ROLLUP_LOG2_MAX_MCYCLES_PER_ADVANCE_STATE = 48;
3232
uint64 constant ROLLUP_LOG2_MAX_UARCH_CYCLES_PER_MCYCLE = 20;
3333
uint64 constant ROLLUP_LOG2_MAX_OUTPUT_COUNT = 63;
3434
uint64 constant ROLLUP_LOG2_MAX_ADVANCE_STATES_PER_EPOCH = 24;
3535
uint64 constant UARCH_HALT_ADDRESS = 0x400000;
36-
uint64 constant UARCH_HALT_HALTED = 1;
37-
uint64 constant UARCH_HALT_CYCLE_OVERFLOW = 3;
3836
uint64 constant UARCH_PC_ADDRESS = 0x400010;
3937
uint64 constant UARCH_X0_ADDRESS = 0x400018;
4038
uint64 constant UARCH_SHADOW_START_ADDRESS = 0x400000;

‎src/UArchStep.sol‎

Lines changed: 10 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -32,16 +32,6 @@ library UArchStep {
3232
UArchHalted // microarchitecture reached or was already at its halted fixed point
3333
}
3434

35-
function uarch_halt_to_step_status(uint64 halt)
36-
private
37-
pure
38-
returns (UArchStepStatus)
39-
{
40-
return halt == EmulatorConstants.UARCH_HALT_CYCLE_OVERFLOW
41-
? UArchStepStatus.UArchCycleOverflow
42-
: UArchStepStatus.UArchHalted;
43-
}
44-
4535
// Memory read/write access
4636

4737
function readUint64(AccessLogs.Context memory a, uint64 paddr)
@@ -1082,8 +1072,7 @@ library UArchStep {
10821072
// return value is in a0 (and maybe also in a1)
10831073
uint64 fn = EmulatorCompat.readX(a, 17); // a7 contains the function number
10841074
if (fn == EmulatorConstants.UARCH_ECALL_FN_HALT) {
1085-
return
1086-
EmulatorCompat.writeHalt(a, EmulatorConstants.UARCH_HALT_HALTED);
1075+
return EmulatorCompat.writeHalt(a, 1);
10871076
}
10881077
if (fn == EmulatorConstants.UARCH_ECALL_FN_PUTCHAR) {
10891078
uint64 c = EmulatorCompat.readX(a, 10); // a0 contains the character to print
@@ -1328,38 +1317,29 @@ library UArchStep {
13281317
pure
13291318
returns (UArchStepStatus)
13301319
{
1331-
// Report existing halt fixed point
1332-
uint64 halt = EmulatorCompat.readHalt(a);
1333-
if (halt != 0) {
1334-
return uarch_halt_to_step_status(halt);
1335-
}
1336-
// Report existing overflow fixed point if the cycle is at or beyond its limit
1320+
// Report the derived overflow fixed point before all other break reasons.
13371321
uint64 cycle = EmulatorCompat.readCycle(a);
13381322
if (cycle >= EmulatorConstants.UARCH_CYCLE_MAX) {
1339-
EmulatorCompat.writeHalt(
1340-
a, EmulatorConstants.UARCH_HALT_CYCLE_OVERFLOW
1341-
);
13421323
return UArchStepStatus.UArchCycleOverflow;
13431324
}
1325+
// Report an existing ordinary halt fixed point.
1326+
if (EmulatorCompat.readHalt(a) != 0) {
1327+
return UArchStepStatus.UArchHalted;
1328+
}
13441329
// Execute next instruction
13451330
uint64 pc = EmulatorCompat.readPc(a);
13461331
uint32 insn = readUint32(a, pc);
13471332
executeInsn(a, insn, pc);
13481333
cycle = cycle + 1;
13491334
EmulatorCompat.writeCycle(a, cycle);
1350-
// Materialize overflow immediately when this step reaches the cycle limit
1335+
// Overflow has precedence when this step reaches the cycle limit.
13511336
if (cycle >= EmulatorConstants.UARCH_CYCLE_MAX) {
1352-
EmulatorCompat.writeHalt(
1353-
a, EmulatorConstants.UARCH_HALT_CYCLE_OVERFLOW
1354-
);
13551337
return UArchStepStatus.UArchCycleOverflow;
13561338
}
1357-
// ECALL is the only instruction that can halt the uarch. Overflow was handled above,
1358-
// so a non-zero halt value here can only report a normal halt.
1339+
// ECALL is the only instruction that can halt the uarch.
13591340
if (insn == uint32(0x73)) {
1360-
halt = EmulatorCompat.readHalt(a);
1361-
if (halt != 0) {
1362-
return uarch_halt_to_step_status(halt);
1341+
if (EmulatorCompat.readHalt(a) != 0) {
1342+
return UArchStepStatus.UArchHalted;
13631343
}
13641344
}
13651345
return UArchStepStatus.Success;

‎test/UArchInterpret.t.sol‎

Lines changed: 41 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -115,23 +115,30 @@ contract UArchInterpretTest is Test {
115115
EmulatorConstants.UARCH_CYCLE_MAX,
116116
"step should not advance when cycle is at its maximum"
117117
);
118-
assertEq(
119-
EmulatorCompat.readHalt(a),
120-
EmulatorConstants.UARCH_HALT_CYCLE_OVERFLOW,
121-
"halt flag should record cycle overflow"
122-
);
118+
assertEq(EmulatorCompat.readHalt(a), 0, "overflow should preserve halt");
123119

124120
// reset cycle to 0
125121
EmulatorCompat.writeCycle(a, 0);
126122
// set machine to halt
127-
EmulatorCompat.writeHalt(a, EmulatorConstants.UARCH_HALT_HALTED);
123+
EmulatorCompat.writeHalt(a, 1);
128124

129125
status = UArchInterpret.interpret(a);
130126

131127
assertTrue(
132128
status == UArchStep.UArchStepStatus.UArchHalted,
133129
"machine should halt"
134130
);
131+
132+
// overflow takes precedence over halt
133+
EmulatorCompat.writeCycle(a, EmulatorConstants.UARCH_CYCLE_MAX);
134+
135+
status = UArchInterpret.interpret(a);
136+
137+
assertTrue(
138+
status == UArchStep.UArchStepStatus.UArchCycleOverflow,
139+
"machine should be cycle overflow"
140+
);
141+
assertEq(EmulatorCompat.readHalt(a), 1, "overflow should preserve halt");
135142
}
136143

137144
function testIllegalInstruction() public {
@@ -146,6 +153,34 @@ contract UArchInterpretTest is Test {
146153
ExternalUArchInterpret.interpret(a);
147154
}
148155

156+
function testHaltEcallReachesCycleLimit() public {
157+
AccessLogs.Context memory a = newAccessLogsContext();
158+
a.buffer.data = bytes.concat(a.buffer.data, new bytes(8));
159+
160+
EmulatorCompat.writePc(a, EmulatorConstants.UARCH_RAM_START_ADDRESS);
161+
EmulatorCompat.writeWord(
162+
a, EmulatorConstants.UARCH_RAM_START_ADDRESS, 0x73
163+
);
164+
EmulatorCompat.writeX(a, 17, EmulatorConstants.UARCH_ECALL_FN_HALT);
165+
EmulatorCompat.writeCycle(a, EmulatorConstants.UARCH_CYCLE_MAX - 1);
166+
167+
UArchStep.UArchStepStatus status = UArchStep.step(a);
168+
169+
assertTrue(
170+
status == UArchStep.UArchStepStatus.UArchCycleOverflow,
171+
"cycle overflow should take precedence over halt"
172+
);
173+
assertEq(
174+
EmulatorCompat.readCycle(a),
175+
EmulatorConstants.UARCH_CYCLE_MAX,
176+
"step should reach the cycle limit"
177+
);
178+
assertTrue(
179+
EmulatorCompat.readHalt(a) != 0,
180+
"halt ECALL should set a non-zero halt value"
181+
);
182+
}
183+
149184
function testRemovedMarkDirtyPageEcall() public {
150185
// function code 3 was the mark_dirty_page ecall and has been removed, so the
151186
// binary that issues it must now revert as an unsupported ecall

0 commit comments

Comments
 (0)