code wiki / _hdl_build / nx_share_plane_gate.nx

nx_share_plane_gate.nx

buildroot/runtime/_hdl_build/nx_share_plane_gate.nx

14500 B285 linesdepth 2pulls 3 transitivereach 0 importersview sourcekind gate/prooftopic share
docsdependenciesstructsconstsfunctions

about

nx_share_plane_gate.nx -- the regression proof for the share plane. Every tooth is stated as the ATTACK it blocks, because a sharing plane's job is refusal: the failure mode is not "the feature is missing", it is "someone saw something they should not have", and that failure is silent. license_tier: ORIGINAL expect_exit: 0

dependencies 2 imports · 0 importers

nx_syscalls.nx nx_share_plane.nx nx_share_plane_gate.nx

imports: nx_syscalls.nxnx_share_plane.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main sys_mmap g_w sys_write fresh sys_mmap ↻ sp_slots_needed sp_init sp_may sp_owner_of sp_at sp_live_cap sp_at ↻ g_t g_w ↻ sp_claim sp_owner_of ↻ sp_append sp_grant sp_owner_of ↻ sp_may_grant sp_owner_of ↻ sp_live_cap ↻ sp_append ↻ sp_count sp_revoke sp_owner_of ↻ sp_may_grant ↻ sp_append ↻ g_n sys_mmap ↻ sys_write ↻ sp_gift sp_owner_of ↻ sp_append ↻ sp_owner_of ↻ sp_provenance_len sp_at ↻ sp_provenance_at sp_at ↻

structs

none

consts

8const SG_CAP: i64 = 64
9const SG_ALICE: i64 = 1001
10const SG_BOB: i64 = 1002
11const SG_CARA: i64 = 1003
12const SG_DAN: i64 = 1004
13const SG_ALBUM: i64 = 7001
14const SG_CARD: i64 = 7002

functions

16func g_w(s: *u8) -> i64 { var n: i64=0; while s[n]!=(0 as u8){n=n+1} sys_write(1,s,n); return 0 }
called by 2: g_tmain calls 1: sys_write
17func g_n(v: i64) -> i64
called by 1: main calls 2: sys_mmapsys_write
27func g_t(pass: i64, label: *u8, fails: *i64) -> i64
called by 1: main calls 1: g_w
32func fresh() -> *i64
called by 1: main calls 3: sys_mmapsp_slots_neededsp_init
38func main() -> i64
calls 18: sys_mmapg_wfreshsp_mayg_tsp_claim+12