code wiki / _hdl_build / nx_adnet_view_gate.nx

nx_adnet_view_gate.nx

buildroot/runtime/_hdl_build/nx_adnet_view_gate.nx

5121 B88 linesdepth 5pulls 5 transitivereach 0 importersview sourcekind gate/prooftopic adnet

docs dependencies structs consts functions

about

nx_adnet_view_gate.nx -- GATE for nx_adnet_view (MRC viewable-impression measurement). Proves, by independent re-derivation rather than by calling the code under test to describe itself: (1) the emitted observer carries BOTH MRC thresholds, sourced from the consts (script/const drift = RED) (2) the second is CONTINUOUS, not cumulative -- the timer is cancelled when the creative leaves view (3) it fires AT MOST ONCE per page (disconnect + latch), so a scroll-by cannot inflate the count (4) FAIL-CLOSED: a malformed id journals NOTHING while still answering 204 (no id oracle) (5) PRIVACY BY CONSTRUCTION: the beacon carries no cookie/visitor/referrer token -- a PAIRED control, asserting a known-present token present AND a known-absent token absent, so the gate is proven able to fail rather than trivially green. expect_exit: 0 license_tier: ORIGINAL

dependencies 2 imports · 0 importers

imports: nx_syscalls.nxnx_adnet_view.nx

imported by: nobody (leaf or entry point)

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

structs

none

consts

none

functions

14	func tv_slen(s: *u8) -> i64 { var i: i64 = 0; while s[i] != (0 as u8) { i = i + 1 } return i } called by 3: tv_puts tv_has main
15	func tv_puts(s: *u8) -> i64 { sys_write(1, s, tv_slen(s)); return 0 } called by 2: tv_check main calls 2: sys_write tv_slen
16	func tv_pn(v: i64) -> i64 called by 1: main calls 2: sys_mmap sys_write
28	func tv_has(buf: u8, n: i64, pat: u8) -> i64 called by 1: main calls 1: tv_slen
42	func tv_check(name: *u8, cond: i64) -> i64 called by 1: main calls 1: tv_puts
48	func main() -> i64 calls 8: tv_puts sys_mmap aview_script tv_check tv_has aview_resp+2