code wiki / (root) / nx_wasm_layout_verify_gate.nx

nx_wasm_layout_verify_gate.nx source

↩ module page · 47 lines · 2418 B

1import "nx_wasm_layout_verify_lib.nx" 2import "nx_wasm_layout_lib.nx" 3import "nx_gate_verdict.nx" 4 5func wlv_bad_word(b: *u8,n: i64,offset: i64,value: i64,c: *i64,label: *u8) -> i64 { 6 let old: i64=wlv_word(b,offset) 7 wl_word(b,offset,value) 8 gv_check_eq(label,wlv_check(b,n,1),0,c) 9 wl_word(b,offset,old) 10 return 0 11} 12func main() -> i64 { 13 let c: *i64=gv_ctr() 14 let m: *Module=ir_module_new("independent-layout" as *u8) 15 ir_add_global_string(m,"A" as *u8,1) 16 ir_add_global_bss(m,"state" as *u8,5,65528) 17 ir_add_global_data(m,"value" as *u8,5,7,8) 18 let b: *u8=sys_mmap(161) 19 gv_check_eq("record generated",wl_record(m,1,1,b,160),160,c) 20 gv_check_eq("mixed shared accepted",wlv_check(b,160,1),1,c) 21 gv_check_eq("shared record in plain mode refused",wlv_check(b,160,0),0,c) 22 gv_check_eq("truncated record refused",wlv_check(b,159,1),0,c) 23 gv_check_eq("trailing byte refused",wlv_check(b,161,1),0,c) 24 gv_check_eq("null record refused",wlv_check(0 as *u8,160,1),0,c) 25 wlv_bad_word(b,160,8,2,c,"unknown version refused") 26 wlv_bad_word(b,160,16,4,c,"exaggerated count refused") 27 wlv_bad_word(b,160,24,65535,c,"unaligned arena refused") 28 wlv_bad_word(b,160,32,2,c,"insufficient memory refused") 29 wlv_bad_word(b,160,32,4,c,"noncanonical memory extent refused") 30 wlv_bad_word(b,160,40,65544,c,"state overlapping BSS refused") 31 wlv_bad_word(b,160,48,4,c,"partial state reservation refused") 32 wlv_bad_word(b,160,56,159,c,"false declared record length refused") 33 wlv_bad_word(b,160,96,0,c,"duplicate global identity refused") 34 wlv_bad_word(b,160,104,65536,c,"overlapping global refused") 35 wlv_bad_word(b,160,112,4294967296,c,"oversize BSS refused") 36 wlv_bad_word(b,160,120,8,c,"unknown flags refused") 37 wlv_bad_word(b,160,120,7,c,"zero-init string contradiction refused") 38 wlv_bad_word(b,160,80,0,c,"missing string terminator refused") 39 wlv_bad_word(b,160,112,-1,c,"unsigned overflow refused") 40 gv_check_eq("restored record accepted",wlv_check(b,160,1),1,c) 41 wl_record(m,1,0,b,160) 42 gv_check_eq("plain record accepted",wlv_check(b,160,0),1,c) 43 let empty: *Module=ir_module_new("empty" as *u8) 44 wl_record(empty,1,1,b,160) 45 gv_check_eq("empty shared record accepted",wlv_check(b,64,1),1,c) 46 return gv_verdict("WASM-LAYOUT-VERIFY",c,"record structural proof only; source/binary binding and shared execution pending") 47}