Skip to content

Commit ca7b038

Browse files
hero78119Wu Sung-Ming
hero78119
and
Wu Sung-Ming
authored
load store opcode in limb constraint & refresh memory layout (#1030)
To close #1013 ### change scope - [x] limit max address to 2^30 (~1G Byte) on linker script & platform to fit field < u32::MAX - [x] separate heap/stack into different region and avoid overlap - [x] migrate load/store opcode into limb based constraint. ### circuit stats the cost for limb based circuit - add one witness `imm_sign` - main sumcheck got tiny effort as some constrain moving from degree 1 to degree 2 ```diff +---------------+---------------+---------+-------+-----------+--------+------------+---------------------+ | opcode_name | num_instances | lookups | reads | witnesses | writes | 0_expr_deg | 0_expr_sumcheck_deg | +---------------+---------------+---------+-------+-----------+--------+------------+---------------------+ -| LB | 0 | 9 | 4 | 28 | 4 | [1: 4] | [2: 5] | +| LB | 0 | 9 | 4 | 29 | 4 | [1: 3] | [2: 7] | -| LBU | 0 | 8 | 4 | 27 | 4 | [1: 4] | [2: 4] | +| LBU | 0 | 8 | 4 | 28 | 4 | [1: 3] | [2: 6] | -| LH | 0 | 7 | 4 | 25 | 4 | [1: 4] | [2: 3] | +| LH | 0 | 7 | 4 | 26 | 4 | [1: 3] | [2: 5] | -| LHU | 0 | 6 | 4 | 24 | 4 | [1: 4] | [2: 2] | +| LHU | 0 | 6 | 4 | 25 | 4 | [1: 3] | [2: 4] | -| LW | 0 | 6 | 4 | 22 | 4 | [1: 4] | [] | +| LW | 0 | 6 | 4 | 23 | 4 | [1: 3] | [2: 2] | -| SB | 0 | 12 | 4 | 28 | 4 | [1: 4] | [2: 4] | +| SB | 0 | 12 | 4 | 29 | 4 | [1: 3] | [2: 6] | -| SH | 0 | 8 | 4 | 23 | 4 | [1: 4] | [2: 1] | +| SH | 0 | 8 | 4 | 24 | 4 | [1: 3] | [2: 3] | -| SW | 0 | 8 | 4 | 22 | 4 | [1: 4] | [] | +| SW | 0 | 8 | 4 | 23 | 4 | [1: 3] | [2: 2] | ``` ### new memory layout ``` /// alined with [`memory.x`] // ┌───────────────────────────── 0x4000_0000 (end of _sheap, or heap) // │ // │ HEAP (128 MB, grows upward) // │ 0x3800_0000 .. 0x4000_0000 // │ // ├───────────────────────────── 0x3800_0000 (_sheap, align 0x800_0000) // │ RAM (128 MB) // │ 0x3000_0000 .. 0x3800_0000 // ├───────────────────────────── 0x3000_0000 (RAM base / hints end) // │ // │ HINTS (128 MB) // │ 0x2800_0000 .. 0x3000_0000 // │ // │───────────────────────────── 0x2800_0000 (hint base / gap end) // │ // │ [Reserved gap: 128 MB for debug I/O] // │ 0x2000_0000 .. 0x2800_0000 // │───────────────────────────── 0x2000_0000 (gap / stack end) // │ // │ STACK (≈128 MB, grows downward) // │ 0x1800_0000 .. 0x2000_0000 // │ // ├───────────────────────────── 0x1800_0000 (stack base / pubio end) // │ // │ PUBLIC I/O (128 MB) // │ 0x1000_0000 .. 0x1800_0000 // │ // ├───────────────────────────── 0x1000_0000 (pubio base / rom end) // │ // │ ROM / TEXT / RODATA (128 MB) // │ 0x0800_0000 .. 0x1000_0000 // │ // └───────────────────────────── 0x8000_0000 (rom base) ``` --------- Co-authored-by: Wu Sung-Ming <[email protected]>
1 parent dc5a22a commit ca7b038

File tree

20 files changed

+278
-120
lines changed

20 files changed

+278
-120
lines changed

‎ceno_emul/src/elf.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -239,7 +239,7 @@ impl Program {
239239
));
240240
}
241241

242-
// retrieve sheap from elf
242+
// retrieve _sheap from elf
243243
let sheap = symbols
244244
.iter()
245245
.find(|(_, v)| *v == "_sheap")

‎ceno_emul/src/platform.rs‎

Lines changed: 45 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -57,15 +57,53 @@ impl Display for Platform {
5757
}
5858
}
5959

60-
// alined with [`memory.x`]
60+
/// alined with [`memory.x`]
61+
// ┌───────────────────────────── 0x4000_0000 (end of _sheap, or heap)
62+
// │
63+
// │ HEAP (128 MB, grows upward)
64+
// │ 0x3800_0000 .. 0x4000_0000
65+
// │
66+
// ├───────────────────────────── 0x3800_0000 (_sheap, align 0x800_0000)
67+
// │ RAM (128 MB)
68+
// │ 0x3000_0000 .. 0x3800_0000
69+
// ├───────────────────────────── 0x3000_0000 (RAM base / hints end)
70+
// │
71+
// │ HINTS (128 MB)
72+
// │ 0x2800_0000 .. 0x3000_0000
73+
// │
74+
// │───────────────────────────── 0x2800_0000 (hint base / gap end)
75+
// │
76+
// │ [Reserved gap: 128 MB for debug I/O]
77+
// │ 0x2000_0000 .. 0x2800_0000
78+
// │───────────────────────────── 0x2000_0000 (gap / stack end)
79+
// │
80+
// │ STACK (≈128 MB, grows downward)
81+
// │ 0x1800_0000 .. 0x2000_0000
82+
// │
83+
// ├───────────────────────────── 0x1800_0000 (stack base / pubio end)
84+
// │
85+
// │ PUBLIC I/O (128 MB)
86+
// │ 0x1000_0000 .. 0x1800_0000
87+
// │
88+
// ├───────────────────────────── 0x1000_0000 (pubio base / rom end)
89+
// │
90+
// │ ROM / TEXT / RODATA (128 MB)
91+
// │ 0x0800_0000 .. 0x1000_0000
92+
// │
93+
// └───────────────────────────── 0x8000_0000 (rom base)
6194
pub const CENO_PLATFORM: Platform = Platform {
62-
rom: 0x2000_0000..0x2800_0000, // 128 MB
63-
prog_data: BTreeSet::new(),
64-
stack: 0xB0000000..0xC0000000, // stack grows downward
65-
heap: 0x8000_0000..0xFFFF_0000,
66-
public_io: 0x3000_0000..0x3004_0000,
67-
hints: 0x4000_0000..0x5000_0000, // 256 MB
95+
rom: 0x0800_0000..0x1000_0000, // 128 MB
96+
public_io: 0x1000_0000..0x1800_0000, // 128 MB
97+
stack: 0x1800_0000..0x2000_4000, // stack grows downward 128MB, 0x4000 reserved for debug io.
98+
// we make hints start from 0x2800_0000 thus reserve a 128MB gap for debug io
99+
// at the end of stack
100+
hints: 0x2800_0000..0x3000_0000, // 128 MB
101+
// heap grows upward, reserved 128 MB for it
102+
// the beginning of heap address got bss/sbss data
103+
// and the real heap start from 0x3800_0000
104+
heap: 0x3000_0000..0x4000_0000,
68105
unsafe_ecall_nop: false,
106+
prog_data: BTreeSet::new(),
69107
is_debug: false,
70108
};
71109

‎ceno_host/tests/test_elf.rs‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,10 +54,11 @@ fn test_ceno_rt_mem() -> Result<()> {
5454
prog_data: program.image.keys().copied().collect(),
5555
..CENO_PLATFORM
5656
};
57-
let mut state = VMState::new(platform.clone(), Arc::new(program));
57+
let sheap = program.sheap.into();
58+
let mut state = VMState::new(platform, Arc::new(program.clone()));
5859
let _steps = run(&mut state)?;
5960

60-
let value = state.peek_memory(platform.heap.start.into());
61+
let value = state.peek_memory(sheap);
6162
assert_eq!(value, 6765, "Expected Fibonacci 20, got {}", value);
6263
Ok(())
6364
}

‎ceno_rt/ceno_link.x‎

Lines changed: 28 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,14 @@
11

2-
_stack_start = ORIGIN(REGION_STACK) + 1024M;
3-
_hints_start = ORIGIN(REGION_HINTS);
4-
_hints_length = LENGTH(REGION_HINTS);
5-
_lengths_of_hints_start = ORIGIN(REGION_HINTS);
6-
_pubio_start = ORIGIN(REGION_PUBIO);
7-
_pubio_length = LENGTH(REGION_PUBIO);
2+
/* start to use hint with 128MB offset */
3+
_hints_start = ORIGIN(REGION_HINTS) + 128M;
4+
_hints_length = 128M;
5+
_lengths_of_hints_start = ORIGIN(REGION_HINTS) + 128M;
6+
87
_lengths_of_pubio_start = ORIGIN(REGION_PUBIO);
8+
_pubio_start = ORIGIN(REGION_PUBIO); /* 0x20000000 */
9+
_pubio_end = ORIGIN(REGION_PUBIO) + 128M; /* PUBIO grows upward */
10+
_pubio_length = 128M;
11+
_stack_start = ORIGIN(REGION_PUBIO) + 256M; /* stack grows downward */
912

1013
SECTIONS
1114
{
@@ -22,6 +25,22 @@ SECTIONS
2225
*(.rodata .rodata.*);
2326
} > ROM
2427

28+
.pubio (NOLOAD): ALIGN(4)
29+
{
30+
*(.pubio .pubio.*);
31+
} > STACK_PUBIO
32+
33+
.stack (NOLOAD) : ALIGN(4)
34+
{
35+
*(.stack .stack.*)
36+
} > STACK_PUBIO
37+
38+
/* Define a section for runtime-populated EEPROM-like HINTS data */
39+
.hints (NOLOAD) : ALIGN(4)
40+
{
41+
*(.hints .hints.*);
42+
} > HINTS
43+
2544
.data : ALIGN(4)
2645
{
2746
/* Must be called __global_pointer$ for linker relaxations to work. */
@@ -37,23 +56,11 @@ SECTIONS
3756
*(.sbss .sbss.*);
3857
*(.bss .bss.*);
3958

40-
/* align to 256Mb boundary to ensure proper memory layout. */
59+
/* align to 128Mb boundary to ensure proper memory layout. */
4160
/* this reserves some padding up to the next power of 2 for .text, .sdata, .bss sections, ensuring there is no overlap with the heap. */
42-
/* NOTE 1: This works correctly **only** if the total size of .text + .rodata + .data + .bss does not exceed 256MB. */
61+
/* NOTE 1: This works correctly **only** if the total size of .text + .rodata + .data + .bss does not exceed 128MB. */
4362
/* NOTE 2: This alignment **does not** affect the binary size. */
44-
. = ALIGN(0x10000000);
63+
. = ALIGN(0x8000000);
4564
_sheap = .;
4665
} > RAM
47-
48-
/* Define a section for runtime-populated EEPROM-like HINTS data */
49-
.hints (NOLOAD) : ALIGN(4)
50-
{
51-
*(.hints .hints.*);
52-
} > HINTS
53-
54-
/* Define a section for public io data */
55-
.pubio (NOLOAD) : ALIGN(4)
56-
{
57-
*(.pubio .pubio.*);
58-
} > PUBIO
5966
}

‎ceno_rt/memory.x‎

Lines changed: 9 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,17 +1,18 @@
11
MEMORY
22
{
3-
RAM (rw) : ORIGIN = 0x80000000, LENGTH = 0x40040000 /* 1024M heap/stack + 256k reserved for io */
4-
ROM (rx) : ORIGIN = 0x20000000, LENGTH = 128M
5-
HINTS (r) : ORIGIN = 0x40000000, LENGTH = 256M
6-
PUBIO (r) : ORIGIN = 0x30000000, LENGTH = 1K
3+
ROM (rx) : ORIGIN = 0x08000000, LENGTH = 128M
4+
STACK_PUBIO (rw) : ORIGIN = 0x10000000, LENGTH = 256M /* PUBIO first 128M, Stack second 128M */
5+
HINTS (r) : ORIGIN = 0x20000000, LENGTH = 256M /* will shift hint to 0x28000000 with 128M to reserve gap*/
6+
RAM (rw) : ORIGIN = 0x30000000, LENGTH = 256M /* heap/data/bss */
77
}
88

99
REGION_ALIAS("REGION_TEXT", ROM);
1010
REGION_ALIAS("REGION_RODATA", ROM);
11+
12+
REGION_ALIAS("REGION_PUBIO", STACK_PUBIO);
13+
REGION_ALIAS("REGION_STACK", STACK_PUBIO);
14+
15+
REGION_ALIAS("REGION_HINTS", HINTS);
1116
REGION_ALIAS("REGION_DATA", RAM);
1217
REGION_ALIAS("REGION_BSS", RAM);
1318
REGION_ALIAS("REGION_HEAP", RAM);
14-
REGION_ALIAS("REGION_STACK", RAM);
15-
16-
REGION_ALIAS("REGION_HINTS", HINTS);
17-
REGION_ALIAS("REGION_PUBIO", PUBIO);

‎ceno_rt/src/params.rs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
pub const WORD_SIZE: usize = 4;
22

33
/// address defined in `memory.x` under RAM section.
4-
pub const INFO_OUT_ADDR: u32 = 0xC000_0000;
4+
pub const INFO_OUT_ADDR: u32 = 0x2000_0000;

‎ceno_zkvm/src/e2e.rs‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -328,11 +328,10 @@ fn setup_platform_inner(
328328
let prog_data = program.image.keys().copied().collect::<BTreeSet<_>>();
329329

330330
let stack = if preset.is_debug {
331-
// reserve some extra space for io
332-
// thus memory consistent check could be satisfied
333-
preset.stack.end - stack_size..(preset.stack.end + 0x4000)
331+
(preset.stack.end - 0x4000 - stack_size)..(preset.stack.end)
334332
} else {
335-
preset.stack.end - stack_size..preset.stack.end
333+
// remove extra space for io for non-debug mode
334+
(preset.stack.end - 0x4000 - stack_size)..(preset.stack.end - 0x4000)
336335
};
337336

338337
let heap = {

‎ceno_zkvm/src/instructions/riscv/constants.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ pub const LIMB_MASK: u32 = 0xFFFF;
1717
pub const BIT_WIDTH: usize = 32usize;
1818

1919
pub const PC_BITS: usize = 30;
20+
pub const MEM_BITS: usize = 30;
2021

2122
pub type UInt<E> = UIntLimbs<BIT_WIDTH, LIMB_BITS, E>;
2223
pub type UIntMul<E> = UIntLimbs<{ 2 * BIT_WIDTH }, LIMB_BITS, E>;

‎ceno_zkvm/src/instructions/riscv/im_insn.rs‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,7 @@ impl<E: ExtensionField> IMInstructionConfig<E> {
2727
circuit_builder: &mut CircuitBuilder<E>,
2828
insn_kind: InsnKind,
2929
imm: &Expression<E>,
30+
#[cfg(feature = "u16limb_circuit")] imm_sign: &Expression<E>,
3031
rs1_read: RegisterExpr<E>,
3132
memory_read: MemoryExpr<E>,
3233
memory_addr: AddressExpr<E>,
@@ -51,7 +52,7 @@ impl<E: ExtensionField> IMInstructionConfig<E> {
5152
0.into(),
5253
imm.clone(),
5354
#[cfg(feature = "u16limb_circuit")]
54-
0.into(),
55+
imm_sign.expr(),
5556
))?;
5657

5758
Ok(IMInstructionConfig {

‎ceno_zkvm/src/instructions/riscv/memory/load.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,8 @@ impl<E: ExtensionField, I: RIVInstruction> Instruction<E> for LoadInstruction<E,
143143
circuit_builder,
144144
I::INST_KIND,
145145
&imm.expr(),
146+
#[cfg(feature = "u16limb_circuit")]
147+
0.into(),
146148
rs1_read.register_expr(),
147149
memory_read.memory_expr(),
148150
memory_addr.expr_align4(),

0 commit comments

Comments
 (0)