nx_amort_gate.nx source
↩ module page · 97 lines · 5089 B
1// nx_amort_gate.nx -- LOAN AMORTIZATION GATE.
2// Proves exact monthly interest, the level payment found by bisection (minimal payment that clears the loan),
3// the final payment that absorbs the rounding, the CONSERVATION invariant (sum of principal reductions ==
4// principal, with and without interest), zero total interest at 0pct, monotonicity of balance in payment, and
5// the fail-closed refusals. Zero-rate cases are hand-exact. license_tier: ORIGINAL No hw writes (Rule 26). expect_exit: 0
6
7import "nx_amort_lib.nx"
8import "nx_matter_lib.nx"
9
10func ag_puts(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
11func ag_putn(v: i64) -> i64 {
12 let t: *u8 = sys_mmap(32)
13 var o: i64 = 0
14 var m: i64 = v
15 if m < 0 { t[o] = 45 as u8; o = o + 1; m = 0 - m }
16 let d: *u8 = sys_mmap(32)
17 var k: i64 = 0
18 if m == 0 { d[0] = 48 as u8; k = 1 }
19 while m > 0 { d[k] = (48 + (m % 10)) as u8; m = m / 10; k = k + 1 }
20 var i: i64 = 0
21 while i < k { t[o] = d[k - 1 - i]; o = o + 1; i = i + 1 }
22 sys_write(1, t, o)
23 return 0
24}
25func ag_ck(cnt: *i64, name: *u8, got: i64, want: i64) -> i64 {
26 if got == want {
27 cnt[0] = cnt[0] + 1
28 ag_puts(" PASS " as *u8); ag_puts(name); ag_puts(" = " as *u8); ag_putn(got); ag_puts("\n" as *u8)
29 return 1
30 }
31 cnt[1] = cnt[1] + 1
32 ag_puts(" FAIL " as *u8); ag_puts(name); ag_puts(" got " as *u8); ag_putn(got)
33 ag_puts(" want " as *u8); ag_putn(want); ag_puts("\n" as *u8)
34 return 0
35}
36
37func main(argc: i64, argv: *i64) -> i64 {
38 let cnt: *i64 = sys_mmap(16) as *i64
39 cnt[0] = 0
40 cnt[1] = 0
41
42 ag_puts("NISHI-AMORT-GATE (loan amortization: exact penny allocation, conservation, fail-closed)\n" as *u8)
43
44 // ---- exact monthly interest: 12pct/yr on $1000.00 = $10.00 ----
45 ag_ck(cnt, "A1 monthly interest 12pct on 100000 cents = 1000" as *u8, amort_monthly_interest(100000, 1200), 1000)
46
47 // ---- ZERO-RATE hand-exact anchors ----
48 ag_ck(cnt, "A2 $1200 at 0pct over 12mo -> level payment 10000" as *u8, amort_level_payment(120000, 0, 12), 10000)
49 ag_ck(cnt, "A3 balance after 12 payments of 10000 = 0 exactly" as *u8, amort_balance_after(120000, 0, 10000, 12), 0)
50 ag_ck(cnt, "A4 $1000 at 0pct over 12mo -> level payment 8334 (ceil, never underpays)" as *u8, amort_level_payment(100000, 0, 12), 8334)
51 ag_ck(cnt, "A5 final payment 8326 absorbs the rounding" as *u8, amort_final_payment(100000, 0, 12), 8326)
52 let fin0: i64 = amort_final_payment(100000, 0, 12)
53 let lev0: i64 = amort_level_payment(100000, 0, 12)
54 var finlt: i64 = 0
55 if fin0 < lev0 { finlt = 1 }
56 ag_ck(cnt, "A6 final payment < level payment (last payment absorbs the residue)" as *u8, finlt, 1)
57 ag_ck(cnt, "A7 CONSERVATION: principal reductions sum to 100000 (0pct)" as *u8, amort_principal_sum(100000, 0, 12), 100000)
58 ag_ck(cnt, "A8 total interest at 0pct = 0" as *u8, amort_total_interest(100000, 0, 12), 0)
59
60 // ---- WITH INTEREST: conservation + the bisected minimal payment ----
61 ag_ck(cnt, "A9 CONSERVATION: principal reductions sum to 100000 (12pct)" as *u8, amort_principal_sum(100000, 1200, 12), 100000)
62 let m12: i64 = amort_level_payment(100000, 1200, 12)
63 var paysoff: i64 = 0
64 if amort_balance_after(100000, 1200, m12, 12) <= 0 { paysoff = 1 }
65 ag_ck(cnt, "A10 the level payment clears the loan in 12 months" as *u8, paysoff, 1)
66 var minimal: i64 = 0
67 if amort_balance_after(100000, 1200, m12 - 1, 12) > 0 { minimal = 1 }
68 ag_ck(cnt, "A11 it is MINIMAL: one cent less does NOT clear in 12 months" as *u8, minimal, 1)
69 let ti12: i64 = amort_total_interest(100000, 1200, 12)
70 var tipos: i64 = 0
71 if ti12 > 0 { tipos = 1 }
72 ag_ck(cnt, "A12 total interest at 12pct is positive" as *u8, tipos, 1)
73
74 // ---- monotonicity: a larger payment leaves a smaller balance ----
75 let bbig: i64 = amort_balance_after(100000, 1200, 20000, 12)
76 let bsmall: i64 = amort_balance_after(100000, 1200, 5000, 12)
77 var mono: i64 = 0
78 if bbig < bsmall { mono = 1 }
79 ag_ck(cnt, "A13 balance is monotone-decreasing in the payment" as *u8, mono, 1)
80
81 // ---- *FAIL-CLOSED: no schedule on nonsense input ----
82 ag_ck(cnt, "A14 zero principal -> AMORT_BAD" as *u8, amort_level_payment(0, 1200, 12), AMORT_BAD)
83 ag_ck(cnt, "A15 negative rate -> AMORT_BAD" as *u8, amort_level_payment(100000, 0 - 5, 12), AMORT_BAD)
84 ag_ck(cnt, "A16 zero term -> AMORT_BAD" as *u8, amort_level_payment(100000, 1200, 0), AMORT_BAD)
85 ag_ck(cnt, "A17 fail-closed propagates: total_interest on zero principal = AMORT_BAD" as *u8, amort_total_interest(0, 1200, 12), AMORT_BAD)
86
87 ag_puts("nx_amort_gate: pass=" as *u8); ag_putn(cnt[0])
88 ag_puts(" fail=" as *u8); ag_putn(cnt[1]); ag_puts("\n" as *u8)
89 if cnt[1] == 0 {
90 ag_puts("AMORT nx_amort: VERDICT=GREEN (exact penny allocation + conservation + bisected minimal payment; fail-closed)\n" as *u8)
91 sys_exit(0)
92 return 0
93 }
94 ag_puts("AMORT nx_amort: VERDICT=RED\n" as *u8)
95 sys_exit(1)
96 return 1
97}