nx_rv64_snapshot_gate.nx source

1// nx_rv64_snapshot_gate.nx -- prove DETERMINISTIC snapshot/restore (F107i). Runs a compute program to halt 2// (reference hash A). Then on a second sim: run PARTWAY, snapshot, run to halt -> hash B (== A proves the 3// snapshot is non-disturbing + the continuation is deterministic); RESTORE the snapshot, run to halt -> hash 4// B2 (== A proves restore rewinds + continues byte-identically). Exact because the sim is bit-deterministic 5// (no float) -- the sovereign determinism exceed bet. Self-checking. expect_exit:0 6import "nx_syscalls.nx" 7import "nishi_hdl_primitives.nx" 8import "rv64im_min_decoder.nx" 9import "rv64im_min_alu.nx" 10import "rv64im_min_regfile.nx" 11import "rv64im_min_csr.nx" 12import "rv64im_min_clint.nx" 13import "rv64im_min_uart.nx" 14import "rv64im_min_virtio.nx" 15import "rv64im_min_sim.nx" 16import "nx_rv64_asm.nx" 17 18func g_puts(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 } 19func g_ph(v: i64) -> i64 { 20 let b: *u8=sys_mmap(19); b[0]=48; b[1]=120; var i: i64=0 21 while i<16 { let n: i64=(v>>((15-i)*4))&15; if n<10 { b[2+i]=(48+n) as u8 } if n>=10 { b[2+i]=(87+n) as u8 } i=i+1 } 22 sys_write(1,b,18); return 0 23} 24 25const SN_MEMB: i64 = 0x80000000 26const SN_MEMS: i64 = 65536 27const SN_SCRATCH_OFF: i64 = 0x2000 28 29func state_hash(rf: *NxRv64imRegfile, mem: *u8, memsz: i64) -> i64 { 30 var h: i64 = 0 - 3750763034362895579 31 var i: i64 = 0 32 while i < 32 { 33 let v: i64 = nx_rv64im_rf_read(rf, i) 34 var k: i64 = 0 35 while k < 8 { h = (h ^ ((v >> (k*8)) & 0xff)) * 1099511628211; k = k + 1 } 36 i = i + 1 37 } 38 var m: i64 = 0 39 while m < memsz { h = (h ^ (mem[m] as i64)) * 1099511628211; m = m + 1 } 40 return h 41} 42func rd64(mem: *u8, off: i64) -> i64 { var v: i64=0; var i: i64=0; while i<8 { v=v|((mem[off+i] as i64)<<(i*8)); i=i+1 } return v } 43 44func build_prog(out: *u8) -> i64 { 45 let po: *i64 = sys_mmap(8) as *i64; po[0]=0 46 po[0]=ra_put(out, po[0], ra_i(0x13, 0, 5, 0, 0)) 47 po[0]=ra_put(out, po[0], ra_i(0x13, 0, 6, 0, 400)) 48 po[0]=ra_put(out, po[0], ra_i(0x13, 0, 7, 0, 0)) 49 let loop_off: i64 = po[0] 50 po[0]=ra_put(out, po[0], ra_i(0x13, 0, 5, 5, 1)) 51 po[0]=ra_put(out, po[0], ra_i(0x13, 0, 7, 7, 3)) 52 let bp: i64 = po[0] 53 po[0]=ra_put(out, po[0], ra_b(4, 5, 6, loop_off - bp)) 54 po[0]=ra_put(out, po[0], ra_u(0x37, 15, 0x80002)) 55 po[0]=ra_put(out, po[0], ra_i(0x13, 1, 15, 15, 32)) 56 po[0]=ra_put(out, po[0], ra_i(0x13, 5, 15, 15, 32)) 57 po[0]=ra_put(out, po[0], ra_s(0x23, 3, 15, 7, 0)) 58 po[0]=ra_put(out, po[0], ra_u(0x37, 10, 0x100)) 59 po[0]=ra_put(out, po[0], ra_u(0x37, 11, 0x5)) 60 po[0]=ra_put(out, po[0], ra_i(0x13, 0, 11, 11, 0x555)) 61 po[0]=ra_put(out, po[0], ra_s(0x23, 2, 10, 11, 0)) 62 return po[0] 63} 64 65func mk_sim(code: *u8, nb: i64, out_rf: *i64, out_mem: *i64) -> i64 { 66 let rf_st: *i64=sys_mmap(8*NX_RV64IM_RF_N_REGS) as *i64; let csr_st: *i64=sys_mmap(8*NX_CSR_SLOT_N) as *i64 67 let clint_st: *i64=sys_mmap(8*NX_CLINT_SLOT_N) as *i64; let uart_st: *i64=sys_mmap(8*NX_UART_SLOT_N) as *i64 68 let tx: *u8=sys_mmap(256); let mem: *u8=sys_mmap(SN_MEMS) 69 let rf: *NxRv64imRegfile=sys_mmap(64) as *NxRv64imRegfile; let csr: *NxRv64imCsrFile=sys_mmap(64) as *NxRv64imCsrFile 70 let clint: *NxClint=sys_mmap(64) as *NxClint; let uart: *NxUart=sys_mmap(64) as *NxUart; let sim: *NxRv64imSim=sys_mmap(256) as *NxRv64imSim 71 nx_rv64im_rf_init(rf, rf_st); nx_rv64im_csr_init(csr, csr_st, 0); nx_clint_init(clint, clint_st); nx_uart_init(uart, uart_st, tx, 256) 72 nx_rv64im_sim_init(sim, rf, csr, clint, uart, SN_MEMB, mem, SN_MEMS, 0) 73 var z: i64=0; while z<SN_MEMS { mem[z]=0 as u8; z=z+1 } 74 var i: i64=0; while i<nb { mem[i]=code[i]; i=i+1 } 75 out_rf[0] = rf as i64 76 out_mem[0] = mem as i64 77 return sim as i64 78} 79 80func main() -> i64 { 81 g_puts("nx_rv64_snapshot_gate (deterministic snapshot/restore -- F107i; leverages the no-float determinism)\n" as *u8) 82 let code: *u8 = sys_mmap(4096) 83 let nb: i64 = build_prog(code) 84 85 let rfp: *i64=sys_mmap(8) as *i64; let memp: *i64=sys_mmap(8) as *i64 86 var fails: i64 = 0 87 88 let simA: *NxRv64imSim = mk_sim(code, nb, rfp, memp) as *NxRv64imSim 89 let rfA: *NxRv64imRegfile = rfp[0] as *NxRv64imRegfile; let memA: *u8 = memp[0] as *u8 90 nx_rv64im_sim_run(simA, 10000000) 91 let hash_a: i64 = state_hash(rfA, memA, SN_MEMS) 92 let t2_a: i64 = nx_rv64im_rf_read(rfA, 7) 93 let scratch_a: i64 = rd64(memA, SN_SCRATCH_OFF) 94 95 let simB: *NxRv64imSim = mk_sim(code, nb, rfp, memp) as *NxRv64imSim 96 let rfB: *NxRv64imRegfile = rfp[0] as *NxRv64imRegfile; let memB: *u8 = memp[0] as *u8 97 nx_rv64im_sim_run(simB, 600) 98 let snapbuf: *u8 = sys_mmap(NX_RV64IM_SNAP_HDR + SN_MEMS + 64) 99 nx_rv64im_sim_snapshot(simB, snapbuf) 100 nx_rv64im_sim_run(simB, 10000000) 101 let hash_b: i64 = state_hash(rfB, memB, SN_MEMS) 102 103 nx_rv64im_sim_restore(simB, snapbuf) 104 nx_rv64im_sim_run(simB, 10000000) 105 let hash_b2: i64 = state_hash(rfB, memB, SN_MEMS) 106 107 g_puts(" program computed t2="); g_ph(t2_a); g_puts(" scratch_mem="); g_ph(scratch_a); g_puts(" (expect 0x4b0=1200)\n" as *u8) 108 if t2_a != 1200 { fails=fails+1; g_puts(" FAIL program did not compute t2=1200 (test would be vacuous)\n" as *u8) } 109 if scratch_a != 1200 { fails=fails+1; g_puts(" FAIL scratch memory != 1200 (memory side-effect missing)\n" as *u8) } 110 g_puts(" hash A (uninterrupted) = "); g_ph(hash_a); g_puts("\n" as *u8) 111 g_puts(" hash B (snapshot+continue) = "); g_ph(hash_b); g_puts("\n" as *u8) 112 g_puts(" hash B2 (restore+continue) = "); g_ph(hash_b2); g_puts("\n" as *u8) 113 if hash_b != hash_a { fails=fails+1; g_puts(" FAIL snapshot disturbed execution (B != A)\n" as *u8) } 114 if hash_b2 != hash_a { fails=fails+1; g_puts(" FAIL restore+continue diverged (B2 != A)\n" as *u8) } 115 116 if fails == 0 { 117 g_puts("verdict=GREEN (snapshot non-disturbing + restore byte-identical to uninterrupted; determinism exact)\n" as *u8) 118 sys_exit(0); return 0 119 } 120 g_puts("verdict=RED ("); g_ph(fails); g_puts(" failures)\n" as *u8) 121 sys_exit(1); return 1 122}