nx_folkgame_sow_gate.nx source
↩ module page · 159 lines · 7714 B
1// nx_folkgame_sow_gate.nx -- GATE for the sow (mancala) family of nx_folkgame_sow_lib.
2//
3// THE LOAD-BEARING TOOTH IS T8: seed conservation over an EXHAUSTIVE game tree. Sowing moves seeds
4// and never creates or destroys one, so the total must equal perside*2*seeds at EVERY node of the
5// tree, not at a sampled few. A sowing loop that is off by one anywhere -- a wrap that drops a seed,
6// a capture that adds one, a relay that re-sows a pit it already emptied -- breaks it at some node,
7// and no implementation can satisfy it across thousands of positions by accident.
8// HONEST SCOPE, STATED PLAINLY: this is an INVARIANT, not a published constant. Unlike the align
9// family's 255168 there is no cheap external number for these boards. Conservation proves the seeds
10// are handled correctly; it does NOT prove the capture rules match Oware as played. The external
11// anchor for that is OpenSpiel's Oware, graded THOROUGHLY-TESTED in its own table, and cross-checking
12// against it is the named open rung. A green here means the arithmetic is sound and says nothing
13// stronger.
14// T9 CARRIES THE ANTI-VACUITY: the conservation checker is proven able to FAIL by planting a seed
15// into a live position and asserting the total goes wrong. A checker that has only ever agreed has
16// not been shown to check anything.
17// license_tier: ORIGINAL No hw writes (Rule 26).
18import "nx_folkgame_sow_lib.nx"
19import "nx_gate_verdict.nx"
20
21const FGG_SPEC: *u8 = "knowledge/compare/folkgames.sow"
22// Definitional, from the boards themselves: Oware is six pits a side of four seeds, so 48 in play
23// and six opening moves. Congkak is seven of seven (98) and Pallanguzhi seven of six (84).
24const FGG_OWARE_CELLS: i64 = 12
25const FGG_OWARE_TOTAL: i64 = 48
26const FGG_OWARE_OPEN: i64 = 6
27const FGG_KALAH_CELLS: i64 = 14
28const FGG_CONGKAK_TOTAL: i64 = 98
29const FGG_PALLAN_TOTAL: i64 = 84
30// Oware branches at most six ways, so a depth of six visits tens of thousands of positions -- deep
31// enough that a conservation break has many chances to appear, and bounded so the gate stays inside
32// the evidence layer's deadline.
33const FGG_WALK_DEPTH: i64 = 6
34
35func fgg_slen(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } return n }
36
37// Exhaustive walk. Returns nodes visited; bad[0] counts every node whose seed total is wrong.
38func fgg_walk(base: i64, snap: *i64, sw: i64, mvb: *i64, mm: i64, probe: *i64, d: i64, maxd: i64, bad: *i64) -> i64 {
39 if fgs_total(base) != fgs_expected(base) { bad[0] = bad[0] + 1 }
40 if d >= maxd { return 1 }
41 let out: *i64 = ((mvb as i64) + d * mm * FG_WORD) as *i64
42 let n: i64 = fgs_moves(base, out, probe)
43 if n == 0 { return 1 }
44 let sv: *i64 = ((snap as i64) + d * sw * FG_WORD) as *i64
45 var nodes: i64 = 1
46 var i: i64 = 0
47 while i < n {
48 fg_save(base, sv)
49 fgs_apply(base, out[i], probe)
50 nodes = nodes + fgg_walk(base, snap, sw, mvb, mm, probe, d + 1, maxd, bad)
51 fg_load(base, sv)
52 i = i + 1
53 }
54 return nodes
55}
56
57func fgg_open_moves(base: i64, probe: *i64) -> i64 {
58 let mm: i64 = fg_maxmoves(base)
59 let out: *i64 = sys_mmap(mm * FG_WORD) as *i64
60 let n: i64 = fgs_moves(base, out, probe)
61 sys_munmap(out as *u8, mm * FG_WORD)
62 return n
63}
64
65func main() -> i64 {
66 let ctr: *i64 = gv_ctr()
67 gv_head("nx_folkgame_sow -- mancala plays by its own spec, and seeds are conserved across an exhaustive tree" as *u8)
68
69 let ow: i64 = fg_parse_named_file(FGG_SPEC, "oware" as *u8)
70 gv_check("T1 oware section parses from the shared family spec" as *u8, (ow != 0) as i64, ctr)
71 var ok2: i64 = 0
72 var ok3: i64 = 0
73 var ok4: i64 = 0
74 var probe: *i64 = 0 as *i64
75 if ow != 0 {
76 probe = sys_mmap(fg_snapwords(ow) * FG_WORD) as *i64
77 if fg_cells(ow) == FGG_OWARE_CELLS { ok2 = 1 }
78 fgs_reset(ow)
79 if fgs_total(ow) == FGG_OWARE_TOTAL { ok3 = 1 }
80 if fgg_open_moves(ow, probe) == FGG_OWARE_OPEN { ok4 = 1 }
81 }
82 gv_check("T2 oware is a twelve pit board" as *u8, ok2, ctr)
83 gv_check("T3 forty-eight seeds are in play at the opening, six pits of four a side" as *u8, ok3, ctr)
84 gv_check("T4 six legal opening moves, one per non-empty pit on the mover's side" as *u8, ok4, ctr)
85
86 var ok5: i64 = 0
87 var ok6: i64 = 0
88 let ka: i64 = fg_parse_named_file(FGG_SPEC, "kalah" as *u8)
89 if ka != 0 {
90 if fg_cells(ka) == FGG_KALAH_CELLS { ok5 = 1 }
91 fgs_reset(ka)
92 if fgs_total(ka) == FGG_OWARE_TOTAL { ok6 = 1 }
93 }
94 gv_check("T5 kalah is the same six by four board plus two stores, so fourteen cells" as *u8, ok5, ctr)
95 gv_check("T6 kalah also opens with forty-eight seeds: the stores start empty and hold no seeds of their own" as *u8, ok6, ctr)
96
97 var ok7: i64 = 0
98 let co: i64 = fg_parse_named_file(FGG_SPEC, "congkak" as *u8)
99 let pa: i64 = fg_parse_named_file(FGG_SPEC, "pallanguzhi" as *u8)
100 if co != 0 {
101 if pa != 0 {
102 fgs_reset(co)
103 fgs_reset(pa)
104 if fgs_total(co) == FGG_CONGKAK_TOTAL {
105 if fgs_total(pa) == FGG_PALLAN_TOTAL { ok7 = 1 }
106 }
107 }
108 }
109 gv_check("T7 congkak opens with ninety-eight seeds and pallanguzhi with eighty-four, each derived from its own board" as *u8, ok7, ctr)
110
111 var ok8: i64 = 0
112 var nodes: i64 = 0
113 if ow != 0 {
114 let sw: i64 = fg_snapwords(ow)
115 let mm: i64 = fg_maxmoves(ow)
116 let depth: i64 = FGG_WALK_DEPTH + 2
117 let snap: *i64 = sys_mmap(depth * sw * FG_WORD) as *i64
118 let mvb: *i64 = sys_mmap(depth * mm * FG_WORD) as *i64
119 let bad: *i64 = sys_mmap(FG_WORD * 2) as *i64
120 bad[0] = 0
121 fgs_reset(ow)
122 nodes = fgg_walk(ow, snap, sw, mvb, mm, probe, 0, FGG_WALK_DEPTH, bad)
123 gv_puts(" exhaustive oware walk to depth " as *u8)
124 gv_num(FGG_WALK_DEPTH)
125 gv_puts(" visited " as *u8)
126 gv_num(nodes)
127 gv_puts(" positions, seed-total violations: " as *u8)
128 gv_num(bad[0])
129 gv_puts("\n" as *u8)
130 if bad[0] == 0 { if nodes > 0 { ok8 = 1 } }
131 }
132 gv_subjects("positions visited by the conservation walk" as *u8, nodes, ctr)
133 gv_check("T8 seeds are conserved at EVERY position of the exhaustive oware tree, not at a sample" as *u8, ok8, ctr)
134
135 var ok9: i64 = 0
136 if ow != 0 {
137 fgs_reset(ow)
138 let st: *i64 = fg_state(ow)
139 st[0] = st[0] + 1
140 if fgs_total(ow) != fgs_expected(ow) { ok9 = 1 }
141 st[0] = st[0] - 1
142 if fgs_total(ow) != fgs_expected(ow) { ok9 = 0 }
143 }
144 gv_check("neg-control-conservation-can-fail planting one seed into a live position makes the total WRONG, and removing it makes it right again, so the checker is not vacuous" as *u8, ok9, ctr)
145
146 let b1: *u8 = "family|sow\ncells|13\nperside|6\nseeds|4\nstore|0\n" as *u8
147 let b2: *u8 = "family|sow\ncells|12\nseeds|4\n" as *u8
148 let b3: *u8 = "family|sow\ncells|12\nperside|6\n" as *u8
149 let r1: i64 = fg_parse(b1, fgg_slen(b1))
150 let r2: i64 = fg_parse(b2, fgg_slen(b2))
151 let r3: i64 = fg_parse(b3, fgg_slen(b3))
152 gv_check("neg-control-layout-mismatch-refused a board whose cells do not equal perside times two plus its stores is REFUSED with both numbers named" as *u8, (r1 == 0) as i64, ctr)
153 gv_check("neg-control-no-perside-refused a sow game without a perside row is REFUSED" as *u8, (r2 == 0) as i64, ctr)
154 gv_check("neg-control-no-seeds-refused a sow game without a seeds row is REFUSED" as *u8, (r3 == 0) as i64, ctr)
155
156 let rc: i64 = gv_verdict("FOLKGAME-SOW" as *u8, ctr, "mancala conserves its seeds across an exhaustive tree and refuses a board that cannot be sown" as *u8)
157 sys_exit(rc)
158 return rc
159}