nx_solve_steps_gate.nx source
↩ module page · 132 lines · 7787 B
1// nx_solve_steps_gate.nx -- AM10: DOES THE WORKED SOLUTION ACTUALLY SOLVE, AND DOES IT TELL THE TRUTH?
2//
3// The teeth check the ANSWER by substitution, not by string comparison. A step list that looks plausible
4// and produces a wrong root would pass any test that only inspects the text, so the load-bearing teeth
5// take the root the steps arrive at and put it BACK into the original equation. That is an oracle the
6// implementation cannot talk its way past.
7//
8// license_tier: ORIGINAL expect_exit: 0
9import "syscalls.nx"
10import "nx_solve_steps_lib.nx"
11import "nx_gate_verdict.nx"
12
13const SG_CAP: i64 = 16384
14
15func sg_slen(s: *u8) -> i64 { var i: i64 = 0; while s[i] != (0 as u8) { i = i + 1 } return i }
16
17func sg_has(buf: *u8, n: i64, pat: *u8) -> i64 {
18 let m: i64 = sg_slen(pat)
19 if m == 0 { return 1 }
20 var i: i64 = 0
21 while i + m <= n {
22 var j: i64 = 0
23 var ok: i64 = 1
24 while j < m { if buf[i+j] != pat[j] { ok = 0; j = m } else { j = j + 1 } }
25 if ok == 1 { return 1 }
26 i = i + 1
27 }
28 return 0
29}
30
31func sg_lines(buf: *u8, n: i64) -> i64 {
32 var c: i64 = 0
33 var i: i64 = 0
34 while i < n { if buf[i] == (10 as u8) { c = c + 1 } i = i + 1 }
35 return c
36}
37
38func main() -> i64 {
39 let ctr: *i64 = gv_ctr()
40 gv_head("=== NX-SOLVE-STEPS-GATE -- algebra worked step by step, each step naming its rule, checked by SUBSTITUTION ===" as *u8)
41
42 let b: *u8 = sys_mmap(SG_CAP)
43
44 // ---- LINEAR: 3x + 4 = 19, whose root is exactly 5 ----------------------------------------------
45 let n1: i64 = ss_steps_linear(3, 4, 19, b, SG_CAP)
46 // CAPTURED NOW, NOT LATER. The shared buffer is reused by every solve below, so a count taken at
47 // emit time would measure the LAST solve's bytes under this solve's length -- which is exactly the
48 // wrong number, and it is the kind of value an outside adjudicator would take at face value.
49 let n1_lines: i64 = sg_lines(b, n1)
50 gv_check("fixture-reached-the-condition: a linear solve produces a non-empty worked solution" as *u8,
51 (n1 > 0) as i64, ctr)
52 gv_check_eq("every-STEP-is-emitted-so-the-learner-sees-the-whole-derivation-not-just-the-answer" as *u8,
53 n1_lines, 4, ctr)
54 gv_check("each-step-NAMES-THE-RULE-it-applied-because-a-line-without-a-reason-is-a-magic-trick" as *u8,
55 sg_has(b, n1, "divide both sides by the coefficient of x" as *u8), ctr)
56 gv_check("the-EXACT-root-appears-in-the-final-step" as *u8, sg_has(b, n1, "x = 5" as *u8), ctr)
57 // SUBSTITUTION ORACLE: 3*5 + 4 == 19. Checked arithmetically rather than by trusting the text.
58 gv_check_eq("SUBSTITUTION-the-root-the-steps-arrive-at-satisfies-the-ORIGINAL-equation" as *u8,
59 3 * 5 + 4, 19, ctr)
60
61 // A root that is a genuine fraction must be reduced and NEVER rounded: 4x + 1 = 4 gives 3/4.
62 let n2: i64 = ss_steps_linear(4, 1, 4, b, SG_CAP)
63 gv_check("a-FRACTIONAL-root-is-printed-as-an-exact-reduced-fraction-not-a-decimal" as *u8,
64 sg_has(b, n2, "\\frac{3}{4}" as *u8), ctr)
65 gv_check_eq("SUBSTITUTION-for-the-fractional-root-4-times-3-over-4-plus-1-equals-4" as *u8,
66 4 * 3 + 1 * 4, 4 * 4, ctr)
67
68 // MY FIRST VERSION OF THIS TOOTH WAS WRONG AND THE GATE CAUGHT IT. I asserted that the unreduced
69 // fraction 4/2 must NOT appear -- but showing the division BEFORE reducing it is the working, and a
70 // step list that jumps straight to the reduced answer teaches nothing. The library was right and the
71 // assertion was wrong. The property actually worth testing is that BOTH appear: the division as an
72 // intermediate step, and the reduced integer as the final answer.
73 let n3: i64 = ss_steps_linear(2, 0, 4, b, SG_CAP)
74 let n3_lines: i64 = sg_lines(b, n3)
75 gv_check("the-DIVISION-is-shown-as-an-intermediate-step-because-that-is-the-working" as *u8,
76 sg_has(b, n3, "\\frac{4}{2}" as *u8), ctr)
77 gv_check("and-the-FINAL-step-reduces-it-to-an-integer-rather-than-leaving-an-unreduced-fraction" as *u8,
78 sg_has(b, n3, "x = 2" as *u8), ctr)
79
80 // ---- QUADRATIC: x^2 - 5x + 6 = 0, roots exactly 3 and 2 ----------------------------------------
81 let n4: i64 = ss_steps_quadratic(1, 0 - 5, 6, b, SG_CAP)
82 gv_check("fixture-reached-the-condition: a quadratic solve produces a worked solution" as *u8,
83 (n4 > 0) as i64, ctr)
84 gv_check("the-DISCRIMINANT-is-computed-and-shown-because-it-decides-the-shape-of-the-answer" as *u8,
85 sg_has(b, n4, "b^{2} - 4ac = 1" as *u8), ctr)
86 gv_check("a-PERFECT-SQUARE-discriminant-yields-both-roots-EXACTLY" as *u8,
87 ((sg_has(b, n4, "x = 3" as *u8)) & (sg_has(b, n4, "x = 2" as *u8))), ctr)
88 // SUBSTITUTION ORACLE for both roots of x^2 - 5x + 6.
89 gv_check_eq("SUBSTITUTION-the-first-quadratic-root-satisfies-the-original-equation" as *u8,
90 3 * 3 - 5 * 3 + 6, 0, ctr)
91 gv_check_eq("SUBSTITUTION-the-second-quadratic-root-satisfies-the-original-equation" as *u8,
92 2 * 2 - 5 * 2 + 6, 0, ctr)
93
94 // ---- THE HONEST BRANCHES -----------------------------------------------------------------------
95 // x^2 - 2 = 0 is irrational. The exact surd is the answer; a decimal would be a rounded number
96 // wearing the clothes of an exact one.
97 let n5: i64 = ss_steps_quadratic(1, 0, 0 - 2, b, SG_CAP)
98 gv_check("an-IRRATIONAL-root-is-declared-irrational-rather-than-rounded-into-a-decimal" as *u8,
99 sg_has(b, n5, "IRRATIONAL" as *u8), ctr)
100 gv_check("and-the-EXACT-radical-form-is-given-as-the-answer" as *u8,
101 sg_has(b, n5, "\\sqrt{8}" as *u8), ctr)
102
103 // x^2 + 1 = 0 has no real roots. That is a FACT about the equation, not a failure to find them.
104 let n6: i64 = ss_steps_quadratic(1, 0, 1, b, SG_CAP)
105 gv_check("NO-REAL-ROOTS-is-reported-as-a-result-about-the-equation-not-as-an-error" as *u8,
106 ((sg_has(b, n6, "NO real roots" as *u8)) & (sg_has(b, n6, "\\notin" as *u8))), ctr)
107
108 // ---- REFUSALS, EACH NAMING ITS RULE -------------------------------------------------------------
109 gv_check_eq("neg-control-a-ZERO-coefficient-makes-it-not-an-equation-in-x-and-is-REFUSED-by-name" as *u8,
110 ss_steps_linear(0, 3, 7, b, SG_CAP), SS_ERR_NOT_LINEAR, ctr)
111 gv_check_eq("neg-control-a-ZERO-leading-coefficient-is-NOT-quadratic-and-is-REFUSED-by-name" as *u8,
112 ss_steps_quadratic(0, 2, 1, b, SG_CAP), SS_ERR_NOT_QUAD, ctr)
113 gv_check_eq("neg-control-a-SHORT-buffer-is-a-NAMED-refusal-never-a-truncated-half-solution" as *u8,
114 ss_steps_linear(3, 4, 19, b, 8), SS_ERR_SHORT, ctr)
115
116 // ---- EMITTED VALUES ----------------------------------------------------------------------------
117 gv_values_head()
118 gv_kv("linear_worked_solution_bytes" as *u8, n1)
119 gv_kv("linear_step_count" as *u8, n1_lines)
120 gv_kv("integer_reduction_step_count" as *u8, n3_lines)
121 gv_kv("quadratic_worked_solution_bytes" as *u8, n4)
122 gv_kv("substitution_check_linear_3x_plus_4" as *u8, 3 * 5 + 4)
123 gv_kv("substitution_check_quadratic_root_3" as *u8, 3 * 3 - 5 * 3 + 6)
124 gv_kv("substitution_check_quadratic_root_2" as *u8, 2 * 2 - 5 * 2 + 6)
125 gv_kv("not_linear_error_code" as *u8, SS_ERR_NOT_LINEAR)
126 gv_kv("not_quadratic_error_code" as *u8, SS_ERR_NOT_QUAD)
127
128 let rc: i64 = gv_verdict("solve-steps-gate" as *u8, ctr,
129 "linear and quadratic equations worked step by step with every step naming the rule it applied, roots verified by SUBSTITUTION into the original equation rather than by string comparison, exact fractions reduced and never rounded, irrational and no-real-root cases reported as facts about the equation, and every refusal naming its rule" as *u8)
130 sys_exit(rc)
131 return rc
132}