_nx_loop_v2_oracle.nx source
↩ module page · 82 lines · 2958 B
1// _nx_loop_v2_oracle.nx -- correctness oracle for the V2 frame-based
2// loop primitive (nx_loop_begin/step/break/finish + watchdog).
3//
4// 8 oracles cover NORMAL, BOUND_EXHAUSTED, TIMED_OUT, STALLED + edge
5// cases (max_iters=0, break-on-first-step, progress reset).
6
7import "syscalls.nx"
8import "nx_loop.nx"
9import "nx_clock.nx"
10
11func main() -> i64 {
12 // (1) Counted loop, body breaks on iter 5 -> NORMAL, iters=5
13 let lp1: *NxLoopFrame = nx_loop_begin(100)
14 while nx_loop_step(lp1) == 1 {
15 if lp1.iters == 5 { nx_loop_break(lp1) }
16 }
17 let v1: *NxLoopFrame = nx_loop_finish(lp1)
18 if v1.verdict_kind != NX_LV_NORMAL { return 1 }
19 if v1.iters != 5 { return 2 }
20
21 // (2) Bound exhausted: max=10, body never breaks -> BOUND_EXHAUSTED, iters=10
22 let lp2: *NxLoopFrame = nx_loop_begin(10)
23 while nx_loop_step(lp2) == 1 {
24 // body does nothing
25 }
26 let v2: *NxLoopFrame = nx_loop_finish(lp2)
27 if v2.verdict_kind != NX_LV_BOUND_EXHAUSTED { return 3 }
28 if v2.iters != 10 { return 4 }
29
30 // (3) max=0 -> immediate BOUND_EXHAUSTED, iters=0
31 let lp3: *NxLoopFrame = nx_loop_begin(0)
32 while nx_loop_step(lp3) == 1 {
33 // never enters
34 }
35 let v3: *NxLoopFrame = nx_loop_finish(lp3)
36 if v3.verdict_kind != NX_LV_BOUND_EXHAUSTED { return 5 }
37 if v3.iters != 0 { return 6 }
38
39 // (4) Break on first step -> NORMAL, iters=1
40 let lp4: *NxLoopFrame = nx_loop_begin(100)
41 while nx_loop_step(lp4) == 1 {
42 nx_loop_break(lp4)
43 }
44 let v4: *NxLoopFrame = nx_loop_finish(lp4)
45 if v4.verdict_kind != NX_LV_NORMAL { return 7 }
46 if v4.iters != 1 { return 8 }
47
48 // (5) break_with reason -> NORMAL with reason captured
49 let lp5: *NxLoopFrame = nx_loop_begin(100)
50 while nx_loop_step(lp5) == 1 {
51 if lp5.iters == 3 { nx_loop_break_with(lp5, 42) }
52 }
53 let v5: *NxLoopFrame = nx_loop_finish(lp5)
54 if v5.verdict_kind != NX_LV_NORMAL { return 9 }
55 if v5.reason != 42 { return 10 }
56
57 // (6) Stall detection: max_no_progress=5, body never marks progress
58 // -> STALLED at iter 5
59 let lp6: *NxLoopFrame = nx_loop_begin_watchdog(100, 0, 5)
60 while nx_loop_step(lp6) == 1 {
61 // never calls nx_loop_mark_progress
62 }
63 let v6: *NxLoopFrame = nx_loop_finish(lp6)
64 if v6.verdict_kind != NX_LV_STALLED { return 11 }
65
66 // (7) Progress prevents stall: mark progress each iter, max_no_progress=5,
67 // max_iters=10 -> BOUND_EXHAUSTED (not STALLED)
68 let lp7: *NxLoopFrame = nx_loop_begin_watchdog(10, 0, 5)
69 while nx_loop_step(lp7) == 1 {
70 nx_loop_mark_progress(lp7)
71 }
72 let v7: *NxLoopFrame = nx_loop_finish(lp7)
73 if v7.verdict_kind != NX_LV_BOUND_EXHAUSTED { return 12 }
74 if v7.iters != 10 { return 13 }
75
76 // (8) nx_loop_was_normal helper
77 if nx_loop_was_normal(v1) != 1 { return 14 }
78 if nx_loop_was_normal(v2) != 0 { return 15 }
79 if nx_loop_was_normal(v6) != 0 { return 16 }
80
81 return 0
82}