nx_isa_armv7a_gate.nx source
↩ module page · 873 lines · 37829 B
1// nx_isa_armv7a_gate.nx -- THE ARMv7-A CONFORMANCE RULER.
2//
3// WHY IT EXISTS: nx_emu_armv7a.nx is one of ten sovereign ISA
4// emulators in this estate and, until 2026-09-03, it was one of the
5// EIGHT that had never been measured by anything. nx_isa_conform_gate
6// listed armv7a under "UNMEASURED: armv7a cortexm loongarch64 s390x
7// sparc64 -- each owes a manual-derived KAT block here". This organ is
8// that block, kept as its OWN gate so that armv7a can be built,
9// promoted, run and ratcheted without touching a file five other
10// lanes are editing at the same time.
11//
12// THE LAW THIS ORGAN OBEYS: expectations come FROM THE ARM
13// ARCHITECTURE REFERENCE MANUAL (ARMv7-A/R, sections A5.1 data
14// processing, A5.2 load/store, A8.3 condition codes, A8.8 instruction
15// details), never from reading the emulator and writing down what it
16// happens to do. Reading the decoder tells you which classes are
17// IMPLEMENTED; it must never tell you what the answer is, or the
18// ruler is calibrated to the subject it is meant to judge.
19//
20// FIVE OUTCOMES, NEVER ONE. Collapsing them into "FAIL" makes a gap
21// unactionable: an unimplemented class and a miscomputed value need
22// OPPOSITE fixes, and a program that walked off its image is neither.
23// PASS ran and matched the manual-derived expectation
24// WRONG-ANSWER ran to completion and computed the wrong value
25// UNSUPPORTED hit an instruction class the emulator does not decode
26// RAN-OFF-END pc left the image with no exit syscall
27// FAULT bad pc, out-of-range access, or the step budget
28// The sentinels are read out of nx_emu_armv7a.nx's own constant table
29// (A7_UNSUPPORTED -1, A7_RANOFF -2, A7_FAULT -3) and an EABI exit
30// status is masked to 0..255, so no sentinel can collide with an
31// answer.
32//
33// EVERY KAT IS BUILT SO A WRONG IMPLEMENTATION GIVES A DIFFERENT
34// NUMBER, and the exit-status mask is the trap that makes that hard:
35// & 0xff hides every difference that lives above bit 7. So the
36// byte-load KAT shifts the loaded value down before exiting (a word
37// load and a byte load have the SAME low byte and are otherwise
38// indistinguishable), and the rotated-immediate KAT does the same.
39//
40// WHAT THIS RUN CAUSED TO BE BUILT: the first draft of these KATs
41// could not be run at all. The emulator never read the condition
42// field (bits 31:28), so BNE was unconditional, the loop KAT spun to
43// the step budget, and the budget path returned the INITIAL result 0
44// -- a hang that reads as "exited 0", i.e. success. CMP, TST, EOR,
45// RSB, BIC and MVN all claimed to be handled and then matched no
46// branch, so they were silent no-ops; and operand2 in register form
47// ignored the shifter. Those were implemented in nx_emu_armv7a.nx
48// before this gate could be honest, which is the sequence a ruler is
49// supposed to produce: name the gap, close the gap, then fence it.
50//
51// WHY A RATCHET AND NOT A BAR: the emulator is still incomplete (no
52// Thumb, no halfword or signed load/store, no coprocessor, no
53// syscall but exit). A gate demanding completeness would be
54// permanently RED, and a permanently RED detector is one everyone
55// learns to ignore. So the VERDICT is "armv7a did not regress against
56// its banked score" and the absolute coverage is PUBLISHED AS A
57// NUMBER beside it. The number is the worklist; the verdict is the
58// fence.
59//
60// DISPATCH: emu_armv7a_run_mem(mem, size, entry, sp0) -- the only
61// surface all ten emulators share. emu_armv7a_run exists too but
62// takes its own guest size and entry, so building on it would silently
63// test a different layout than the one this organ owns.
64//
65// license_tier: ORIGINAL
66
67import "nx_gate_verdict.nx"
68import "nx_syscalls.nx"
69import "nx_emu_armv7a.nx"
70
71// ---- guest layout THIS ORGAN owns (never read from the emulator) ----
72const AG7_GUEST_BYTES: i64 = 1048576 // 1 MiB guest image
73const AG7_ENTRY: i64 = 0 // KAT code is loaded at guest vaddr 0
74const AG7_SP: i64 = 983040 // 960 KiB: above the code, inside the image
75const AG7_MODE_FILE: i64 = 420 // 0644. 420 and 0x1a4 are the SAME
76 // constant and a sweep that greps one
77 // misses the other.
78
79// ---- non-completion codes, read from nx_emu_armv7a.nx ----
80const AG7_UNSUPPORTED: i64 = -1
81const AG7_RANOFF: i64 = -2
82const AG7_FAULT: i64 = -3
83
84// ---- outcome classes ----
85const AG7_O_PASS: i64 = 0
86const AG7_O_WRONG: i64 = 1
87const AG7_O_UNSUP: i64 = 2
88const AG7_O_FAULT: i64 = 3
89const AG7_O_RANOFF: i64 = 4
90
91// The non-PASS worklist. A count without a worklist is not actionable,
92// and a worklist printed only in the BODY is lost the moment a caller
93// tails the output, so it accumulates here and is printed at the END
94// where every positional reader looks.
95const AG7_NB_BYTES: i64 = 2048
96const AG7_NB_OFF: i64 = 0
97const AG7_NB_PTR: i64 = 1
98const AG7_NB_ROW_MAX: i64 = 256
99const AG7_BOX_BYTES: i64 = 32
100const AG7_SCRATCH: i64 = 256
101
102const AG7_NL: i64 = 10
103const AG7_SPACE: i64 = 32
104const AG7_DIG_LO: i64 = 48
105const AG7_DIG_HI: i64 = 57
106const AG7_UNSEEDED: i64 = -1
107const AG7_B10: i64 = 10
108
109// ---- ARM encoding bases, from the ARM ARM ----
110// Data processing, immediate form (A5.1.3):
111// cond 001 opcode S Rn Rd rot(4) imm8
112// Data processing, register form (A5.1.1):
113// cond 000 opcode S Rn Rd shamt(5) type(2) 0 Rm
114// The values below are the cond=AL(1110) base words; the KATs OR in
115// the register numbers and immediates, so a reader can check any one
116// of them against the manual without decoding a hex constant by hand.
117const AG7_MOV_I: i64 = 0xE3A00000 // mov Rd, imm
118const AG7_MVN_I: i64 = 0xE3E00000 // mvn Rd, imm
119const AG7_ADD_I: i64 = 0xE2800000 // add Rd, Rn, imm
120const AG7_SUB_I: i64 = 0xE2400000 // sub Rd, Rn, imm
121const AG7_RSB_I: i64 = 0xE2600000 // rsb Rd, Rn, imm (imm - Rn)
122const AG7_ORR_I: i64 = 0xE3800000 // orr Rd, Rn, imm
123const AG7_EOR_I: i64 = 0xE2200000 // eor Rd, Rn, imm
124const AG7_BIC_I: i64 = 0xE3C00000 // bic Rd, Rn, imm
125const AG7_CMP_I: i64 = 0xE3500000 // cmp Rn, imm (S=1, no writeback)
126const AG7_ADD_R: i64 = 0xE0800000 // add Rd, Rn, Rm
127const AG7_SUB_R: i64 = 0xE0400000 // sub Rd, Rn, Rm
128const AG7_AND_R: i64 = 0xE0000000 // and Rd, Rn, Rm
129const AG7_MOV_R: i64 = 0xE1A00000 // mov Rd, Rm, shift
130const AG7_CMP_R: i64 = 0xE1500000 // cmp Rn, Rm
131const AG7_MLA: i64 = 0xE0200000 // mla Rd, Rn, Rm, Ra (+0x90 marker)
132const AG7_STR_D: i64 = 0xE5000000 // str Rd,[Rn,-imm] P=1 U=0 B=0 W=0 L=0
133const AG7_LDR_D: i64 = 0xE5100000 // ldr Rd,[Rn,-imm] P=1 U=0 B=0 W=0 L=1
134const AG7_LDRB_D: i64 = 0xE5500000 // ldrb Rd,[Rn,-imm] P=1 U=0 B=1 W=0 L=1
135const AG7_PUSH: i64 = 0xE92D0000 // stmdb sp!, list
136const AG7_POP: i64 = 0xE8BD0000 // ldmia sp!, list
137const AG7_STMIB: i64 = 0xE9A00000 // stmib Rn!, list P=1 U=1 W=1 L=0
138const AG7_LDR_U: i64 = 0xE5900000 // ldr Rd,[Rn,+imm] P=1 U=1 B=0 W=0 L=1
139const AG7_BNE: i64 = 0x1A000000 // bne (cond NE = 0001)
140const AG7_MOVEQ: i64 = 0x03A00000 // moveq Rd, imm (cond EQ = 0000)
141const AG7_MOVNE: i64 = 0x13A00000 // movne Rd, imm (cond NE = 0001)
142const AG7_MOVLT: i64 = 0xB3A00000 // movlt Rd, imm (cond LT = 1011)
143const AG7_MOVGE: i64 = 0xA3A00000 // movge Rd, imm (cond GE = 1010)
144const AG7_SVC: i64 = 0xEF000000 // svc 0
145const AG7_MRC: i64 = 0xEE100F10 // mrc p15,0,r0,c0,c0,0 -- a class this
146 // interpreter does not implement
147const AG7_LDRH: i64 = 0xE15D00B2 // ldrh r0,[sp,-2] -- the EXTRA load/store
148 // space, which lives inside the data
149 // processing encoding and is told apart
150 // only by bit7=1 AND bit4=1
151const AG7_DSB: i64 = 0xF57FF01F // dsb sy -- cond 0b1111, the unconditional
152 // instruction space, a DIFFERENT decode map
153
154// field positions, so no KAT hand-shifts a bare number
155const AG7_P_RD: i64 = 12
156const AG7_P_RN: i64 = 16
157const AG7_P_RM8: i64 = 8
158const AG7_P_SHAMT: i64 = 7
159const AG7_P_SHTY: i64 = 5
160const AG7_MUL_MARK: i64 = 0x90
161const AG7_SHTY_LSR: i64 = 1
162
163// ---- KAT immediates, named for what they mean ----
164const AG7_ANS: i64 = 42 // every KAT that can returns 42
165const AG7_WRONGANS: i64 = 41 // the deliberately wrong want
166const AG7_SUMTO9: i64 = 45 // 0+1+..+9, the loop KAT answer
167const AG7_SIXTY: i64 = 60
168const AG7_C40: i64 = 40
169const AG7_C50: i64 = 50
170const AG7_C99: i64 = 99
171const AG7_C240: i64 = 240
172const AG7_C255: i64 = 255
173const AG7_C15: i64 = 15
174const AG7_C10: i64 = 10
175const AG7_C8: i64 = 8
176const AG7_C7: i64 = 7
177const AG7_C6: i64 = 6
178const AG7_C5: i64 = 5
179const AG7_C3: i64 = 3
180const AG7_C2: i64 = 2
181const AG7_C1: i64 = 1
182const AG7_C0: i64 = 0
183const AG7_XD5: i64 = 0xD5 // 0xFF eor 0xD5 = 0x2A = 42
184const AG7_ROT12: i64 = 0xC00 // rot field 12 -> imm8 ror 24
185const AG7_STKOFF: i64 = 8 // scratch slot below sp
186const AG7_LIST01: i64 = 3 // register list r0 and r1
187const AG7_LIST0: i64 = 1 // register list r0 alone
188const AG7_C64: i64 = 64 // scratch base, 64 bytes below sp
189const AG7_SVCNUM: i64 = 7 // r7 carries the EABI syscall number
190const AG7_EXITNUM: i64 = 1 // EABI exit
191const AG7_BNE_BACK5: i64 = 0xFFFFFB // imm24 = -5 words: back over 4 words + pipeline
192const AG7_SH8: i64 = 8
193const AG7_SH3: i64 = 3
194const AG7_R_SP: i64 = 13 // the ARM stack pointer is r13
195const AG7_KAT_COUNT: i64 = 17 // bind the aggregate assertion to its denominator
196
197const AG7_RATCHET: *u8 = "knowledge/status/isa_armv7a.ratchet"
198
199// A bare newline inside a string literal is ambiguous to this lexer,
200// so the byte is CONSTRUCTED.
201func ag7_nl() -> i64 {
202 let b: *u8 = sys_mmap(AG7_SCRATCH)
203 b[0] = AG7_NL as u8
204 sys_write(1, b, 1)
205 return 0
206}
207
208// ARM is LITTLE-endian. Getting this wrong is the silent-fixture
209// defect: the emulator decodes garbage, reports UNSUPPORTED, and the
210// FIXTURE's bug reads as the emulator being incomplete.
211func ag7_put_le32(code: *u8, off: i64, w: i64) -> i64 {
212 code[off] = (w) & 0xff
213 code[off + 1] = (w >> 8) & 0xff
214 code[off + 2] = (w >> 16) & 0xff
215 code[off + 3] = (w >> 24) & 0xff
216 return off + 4
217}
218
219func ag7_guest() -> *u8 { return sys_mmap(AG7_GUEST_BYTES) }
220
221// Every KAT ends with this two-word Linux EABI exit: r7 = 1, status in r0.
222func ag7_exit(m: *u8, o0: i64) -> i64 {
223 var o: i64 = o0
224 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_SVCNUM << AG7_P_RD) | AG7_EXITNUM)
225 o = ag7_put_le32(m, o, AG7_SVC)
226 return o
227}
228
229func ag7_run(m: *u8) -> i64 { return emu_armv7a_run_mem(m, AG7_GUEST_BYTES, AG7_ENTRY, AG7_SP) }
230
231// ===== outcome classification ===================================
232
233func ag7_classify(got: i64, want: i64) -> i64 {
234 if got == AG7_UNSUPPORTED { return AG7_O_UNSUP }
235 if got == AG7_RANOFF { return AG7_O_RANOFF }
236 if got == AG7_FAULT { return AG7_O_FAULT }
237 if got == want { return AG7_O_PASS }
238 return AG7_O_WRONG
239}
240
241func ag7_outcome_name(o: i64) -> *u8 {
242 if o == AG7_O_PASS { return "PASS" as *u8 }
243 if o == AG7_O_WRONG { return "WRONG-ANSWER" as *u8 }
244 if o == AG7_O_UNSUP { return "UNSUPPORTED-instruction-class" as *u8 }
245 if o == AG7_O_RANOFF { return "RAN-OFF-END-no-exit-syscall" as *u8 }
246 return "FAULT-bad-pc-or-step-budget" as *u8
247}
248
249// Print the VALUES, not just the verdict: every vacuous tooth ever
250// caught in this estate was caught by a diagnostic dump and never by a
251// verdict vector.
252func ag7_report(kat: *u8, got: i64, want: i64, bx: *i64) -> i64 {
253 let o: i64 = ag7_classify(got, want)
254 gv_puts(" KAT armv7a." as *u8)
255 gv_puts(kat)
256 gv_puts(" got=" as *u8)
257 gv_num(got)
258 gv_puts(" want=" as *u8)
259 gv_num(want)
260 gv_puts(" " as *u8)
261 gv_puts(ag7_outcome_name(o))
262 ag7_nl()
263 if o != AG7_O_PASS {
264 let nb: *u8 = bx[AG7_NB_PTR] as *u8
265 var p: i64 = bx[AG7_NB_OFF]
266 if p < (AG7_NB_BYTES - AG7_NB_ROW_MAX) {
267 p = gv_cat(nb, p, "armv7a." as *u8)
268 p = gv_cat(nb, p, kat)
269 p = gv_cat(nb, p, "=" as *u8)
270 p = gv_cat(nb, p, ag7_outcome_name(o))
271 p = gv_cat(nb, p, "(got=" as *u8)
272 p = gv_catn(nb, p, got)
273 p = gv_cat(nb, p, " want=" as *u8)
274 p = gv_catn(nb, p, want)
275 p = gv_cat(nb, p, ") " as *u8)
276 nb[p] = 0 as u8
277 bx[AG7_NB_OFF] = p
278 }
279 }
280 return o
281}
282
283// ===== the KATs =================================================
284// ARM ARM A5.1: data processing. The immediate form carries an 8-bit
285// value rotated right by twice the 4-bit rot field, which is why the
286// rotate KAT below exists at all.
287
288// A5.1.1 register form: add Rd,Rn,Rm with no shift.
289func ag7_k_imm_arith() -> i64 {
290 let m: *u8 = ag7_guest()
291 var o: i64 = 0
292 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C40) // mov r0,40
293 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C1 << AG7_P_RD) | AG7_C2) // mov r1,2
294 o = ag7_put_le32(m, o, AG7_ADD_R | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_C1)
295 o = ag7_exit(m, o)
296 return ag7_run(m)
297}
298
299func ag7_k_sub() -> i64 {
300 let m: *u8 = ag7_guest()
301 var o: i64 = 0
302 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C50) // mov r0,50
303 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C1 << AG7_P_RD) | AG7_C8) // mov r1,8
304 o = ag7_put_le32(m, o, AG7_SUB_R | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_C1)
305 o = ag7_exit(m, o)
306 return ag7_run(m)
307}
308
309// ORR then AND. An implementation that swapped the two would return
310// 255, so the pair discriminates where either alone would not.
311func ag7_k_logic() -> i64 {
312 let m: *u8 = ag7_guest()
313 var o: i64 = 0
314 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C240)
315 o = ag7_put_le32(m, o, AG7_ORR_I | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_C15)
316 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C1 << AG7_P_RD) | AG7_SIXTY)
317 o = ag7_put_le32(m, o, AG7_AND_R | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_C1)
318 o = ag7_exit(m, o)
319 return ag7_run(m)
320}
321
322// EOR was one of the opcodes the decoder claimed and never executed.
323// 0xFF eor 0xD5 = 0x2A; a silent no-op leaves 255.
324func ag7_k_eor() -> i64 {
325 let m: *u8 = ag7_guest()
326 var o: i64 = 0
327 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C255)
328 o = ag7_put_le32(m, o, AG7_EOR_I | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_XD5)
329 o = ag7_exit(m, o)
330 return ag7_run(m)
331}
332
333// BIC clears the bits of the operand: 0xFF bic 0xD5 = 0x2A.
334func ag7_k_bic() -> i64 {
335 let m: *u8 = ag7_guest()
336 var o: i64 = 0
337 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C255)
338 o = ag7_put_le32(m, o, AG7_BIC_I | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_XD5)
339 o = ag7_exit(m, o)
340 return ag7_run(m)
341}
342
343// RSB computes imm - Rn, NOT Rn - imm. Encoding it the intuitive way
344// round is the classic reverse-subtract mistake and would yield -42,
345// which the exit mask renders as 214 -- a DIFFERENT number, which is
346// the whole point.
347func ag7_k_rsb() -> i64 {
348 let m: *u8 = ag7_guest()
349 var o: i64 = 0
350 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C8)
351 o = ag7_put_le32(m, o, AG7_RSB_I | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_C50)
352 o = ag7_exit(m, o)
353 return ag7_run(m)
354}
355
356// PREDICATION, TAKEN DIRECTION. This is the distinctive ARM feature:
357// every instruction carries a condition, so a two-way choice needs no
358// branch at all. An interpreter that ignores bits 31:28 executes BOTH
359// moves and ends with 99.
360func ag7_k_pred_taken() -> i64 {
361 let m: *u8 = ag7_guest()
362 var o: i64 = 0
363 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C7)
364 o = ag7_put_le32(m, o, AG7_CMP_I | (AG7_C0 << AG7_P_RN) | AG7_C7) // 7-7 -> Z=1
365 o = ag7_put_le32(m, o, AG7_MOVEQ | (AG7_C0 << AG7_P_RD) | AG7_ANS)
366 o = ag7_put_le32(m, o, AG7_MOVNE | (AG7_C0 << AG7_P_RD) | AG7_C99)
367 o = ag7_exit(m, o)
368 return ag7_run(m)
369}
370
371// PREDICATION, SKIPPED DIRECTION. The taken test alone cannot tell a
372// working predicate from one that always fires; only the pair can.
373func ag7_k_pred_skipped() -> i64 {
374 let m: *u8 = ag7_guest()
375 var o: i64 = 0
376 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_ANS)
377 o = ag7_put_le32(m, o, AG7_CMP_I | (AG7_C0 << AG7_P_RN) | AG7_C1) // 42-1 -> Z=0
378 o = ag7_put_le32(m, o, AG7_MOVEQ | (AG7_C0 << AG7_P_RD) | AG7_C99) // must NOT run
379 o = ag7_exit(m, o)
380 return ag7_run(m)
381}
382
383// CONDITIONAL BRANCH LOOP: sum 0..9 = 45. Before the condition field
384// was implemented this KAT could not run at all -- BNE was always
385// taken, the program spun to the step budget, and the budget path
386// returned 0, which a caller reads as a successful exit.
387func ag7_k_branch_loop() -> i64 {
388 let m: *u8 = ag7_guest()
389 var o: i64 = 0
390 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C0) // r0 = 0
391 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C1 << AG7_P_RD) | AG7_C0) // r1 = 0
392 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C2 << AG7_P_RD) | AG7_C10) // r2 = 10
393 o = ag7_put_le32(m, o, AG7_ADD_R | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_C1)
394 o = ag7_put_le32(m, o, AG7_ADD_I | (AG7_C1 << AG7_P_RN) | (AG7_C1 << AG7_P_RD) | AG7_C1)
395 o = ag7_put_le32(m, o, AG7_CMP_R | (AG7_C1 << AG7_P_RN) | AG7_C2)
396 o = ag7_put_le32(m, o, AG7_BNE | AG7_BNE_BACK5)
397 o = ag7_exit(m, o)
398 return ag7_run(m)
399}
400
401// SIGNED vs UNSIGNED conditions. -1 compared with 1 sets N=1 V=0, so
402// LT is true and GE is false. A machine that decided LT/GE from an
403// unsigned comparison would take GE (0xFFFFFFFF >= 1) and return 7.
404// This also exercises MVN, another opcode that used to be a no-op.
405func ag7_k_signed_cond() -> i64 {
406 let m: *u8 = ag7_guest()
407 var o: i64 = 0
408 o = ag7_put_le32(m, o, AG7_MVN_I | (AG7_C0 << AG7_P_RD) | AG7_C0) // r0 = 0xFFFFFFFF
409 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C1 << AG7_P_RD) | AG7_C1) // r1 = 1
410 o = ag7_put_le32(m, o, AG7_CMP_R | (AG7_C0 << AG7_P_RN) | AG7_C1)
411 o = ag7_put_le32(m, o, AG7_MOVLT | (AG7_C0 << AG7_P_RD) | AG7_ANS)
412 o = ag7_put_le32(m, o, AG7_MOVGE | (AG7_C0 << AG7_P_RD) | AG7_C7)
413 o = ag7_exit(m, o)
414 return ag7_run(m)
415}
416
417// THE SHIFTER. operand2 in register form is Rm passed through a shift,
418// and an interpreter that takes the bare register returns 7 here
419// instead of 42. 1 + (5 << 3) + 1 = 42.
420func ag7_k_shifted_operand() -> i64 {
421 let m: *u8 = ag7_guest()
422 var o: i64 = 0
423 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C1)
424 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C1 << AG7_P_RD) | AG7_C5)
425 o = ag7_put_le32(m, o, AG7_ADD_R | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | (AG7_SH3 << AG7_P_SHAMT) | AG7_C1)
426 o = ag7_put_le32(m, o, AG7_ADD_I | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_C1)
427 o = ag7_exit(m, o)
428 return ag7_run(m)
429}
430
431// THE ROTATED IMMEDIATE (A5.1.3). rot=12 means the 8-bit value is
432// rotated right by 24, i.e. 0x2A becomes 0x2A00. The shift back down
433// is what makes the KAT discriminate: without it the exit mask would
434// show 0x2A either way, and an interpreter that ignored the rotate
435// would look correct.
436func ag7_k_rot_imm() -> i64 {
437 let m: *u8 = ag7_guest()
438 var o: i64 = 0
439 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_ROT12 | AG7_ANS)
440 o = ag7_put_le32(m, o, AG7_MOV_R | (AG7_C0 << AG7_P_RD) | (AG7_SH8 << AG7_P_SHAMT) | (AG7_SHTY_LSR << AG7_P_SHTY) | AG7_C0)
441 o = ag7_exit(m, o)
442 return ag7_run(m)
443}
444
445// MLA Rd,Rn,Rm,Ra = Rn*Rm + Ra, with Rd in bits 19:16 and Ra in 15:12
446// -- the operand roles are NOT in the order the mnemonic reads.
447func ag7_k_mla() -> i64 {
448 let m: *u8 = ag7_guest()
449 var o: i64 = 0
450 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C6)
451 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C1 << AG7_P_RD) | AG7_C7)
452 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C2 << AG7_P_RD) | AG7_C0)
453 o = ag7_put_le32(m, o, AG7_MLA | (AG7_C3 << AG7_P_RN) | (AG7_C2 << AG7_P_RD) | (AG7_C1 << AG7_P_RM8) | AG7_MUL_MARK | AG7_C0)
454 o = ag7_put_le32(m, o, AG7_MOV_R | (AG7_C0 << AG7_P_RD) | AG7_C3)
455 o = ag7_exit(m, o)
456 return ag7_run(m)
457}
458
459// Load/store with a NEGATIVE (U=0) immediate offset below sp.
460func ag7_k_load_store() -> i64 {
461 let m: *u8 = ag7_guest()
462 var o: i64 = 0
463 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_ANS)
464 o = ag7_put_le32(m, o, AG7_STR_D | (AG7_R_SP << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_STKOFF)
465 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C0)
466 o = ag7_put_le32(m, o, AG7_LDR_D | (AG7_R_SP << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_STKOFF)
467 o = ag7_exit(m, o)
468 return ag7_run(m)
469}
470
471// LDRB must load ONE byte. The obvious version of this test cannot
472// tell a byte load from a word load, because & 0xff at exit hides the
473// difference entirely -- so the loaded value is shifted down by 8
474// first: a correct byte load leaves 0, a word load leaves 1.
475func ag7_k_ldrb() -> i64 {
476 let m: *u8 = ag7_guest()
477 var o: i64 = 0
478 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_ANS)
479 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C1 << AG7_P_RD) | AG7_C1)
480 o = ag7_put_le32(m, o, AG7_ADD_R | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | (AG7_SH8 << AG7_P_SHAMT) | AG7_C1)
481 o = ag7_put_le32(m, o, AG7_STR_D | (AG7_R_SP << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_STKOFF)
482 o = ag7_put_le32(m, o, AG7_LDRB_D | (AG7_R_SP << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_STKOFF)
483 o = ag7_put_le32(m, o, AG7_MOV_R | (AG7_C0 << AG7_P_RD) | (AG7_SH8 << AG7_P_SHAMT) | (AG7_SHTY_LSR << AG7_P_SHTY) | AG7_C0)
484 o = ag7_put_le32(m, o, AG7_ADD_I | (AG7_C0 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_ANS)
485 o = ag7_exit(m, o)
486 return ag7_run(m)
487}
488
489// Block transfer: push then pop restores the clobbered register.
490// STMDB sp! is decrement-before, LDMIA sp! is increment-after, and
491// deriving the base from U alone rather than from P and U is how the
492// other two addressing modes silently go wrong.
493func ag7_k_push_pop() -> i64 {
494 let m: *u8 = ag7_guest()
495 var o: i64 = 0
496 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_ANS)
497 o = ag7_put_le32(m, o, AG7_PUSH | AG7_LIST01)
498 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C0)
499 o = ag7_put_le32(m, o, AG7_POP | AG7_LIST01)
500 o = ag7_exit(m, o)
501 return ag7_run(m)
502}
503
504// The other block-transfer addressing modes. STMDB and LDMIA both have
505// P different from U, so a base derived from U ALONE is right for that
506// pair and wrong for the other two -- the push/pop KAT above cannot see
507// the difference, and a mutation run PROVED it: that defect was the one
508// mutant of thirteen that survived until this KAT existed. STMIB stores
509// at base+4, so reading back through the written-back base returns 42;
510// a U-only derivation stores at base, leaves that slot zero, returns 0.
511func ag7_k_block_ib() -> i64 {
512 let m: *u8 = ag7_guest()
513 var o: i64 = 0
514 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_ANS)
515 o = ag7_put_le32(m, o, AG7_SUB_I | (AG7_R_SP << AG7_P_RN) | (AG7_C1 << AG7_P_RD) | AG7_C64)
516 o = ag7_put_le32(m, o, AG7_STMIB | (AG7_C1 << AG7_P_RN) | AG7_LIST0)
517 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_C0)
518 o = ag7_put_le32(m, o, AG7_LDR_U | (AG7_C1 << AG7_P_RN) | (AG7_C0 << AG7_P_RD) | AG7_C0)
519 o = ag7_exit(m, o)
520 return ag7_run(m)
521}
522
523// ---- LIVE negative controls: the emulator must REFUSE, not guess ----
524
525// A coprocessor access. This interpreter implements no coprocessor, so
526// the honest answer is UNSUPPORTED and never a number.
527func ag7_neg_coproc() -> i64 {
528 let m: *u8 = ag7_guest()
529 var o: i64 = 0
530 o = ag7_put_le32(m, o, AG7_MRC)
531 o = ag7_exit(m, o)
532 return ag7_run(m)
533}
534
535// The EXTRA load/store space (LDRH here) sits inside the data
536// processing encoding and is separated from it only by bit7=1 AND
537// bit4=1. Running it as data processing is a SILENT WRONG ANSWER, so
538// this control asserts it is named instead.
539func ag7_neg_extra_ldst() -> i64 {
540 let m: *u8 = ag7_guest()
541 var o: i64 = 0
542 o = ag7_put_le32(m, o, AG7_LDRH)
543 o = ag7_exit(m, o)
544 return ag7_run(m)
545}
546
547// cond 0b1111 is not "always": it selects a different decode map.
548func ag7_neg_uncond_space() -> i64 {
549 let m: *u8 = ag7_guest()
550 var o: i64 = 0
551 o = ag7_put_le32(m, o, AG7_DSB)
552 o = ag7_exit(m, o)
553 return ag7_run(m)
554}
555
556// A program with no exit syscall at all. The image is zero-filled, so
557// pc walks to the end and the interpreter must say RAN-OFF-END rather
558// than return its initial result as if it were a status.
559func ag7_neg_no_exit() -> i64 {
560 let m: *u8 = ag7_guest()
561 var o: i64 = 0
562 o = ag7_put_le32(m, o, AG7_MOV_I | (AG7_C0 << AG7_P_RD) | AG7_ANS)
563 return ag7_run(m)
564}
565
566// ===== ratchet ==================================================
567// One line: "armv7a <passed>". UNSEEDED is a NAMED third state, so
568// adopting this fence cannot fail closed on first sight. Polarity:
569// this metric is GOOD-when-higher, so it TIGHTENS on a rise and must
570// NEVER rewrite its baseline on a fall -- rewriting on a fall is how a
571// ratchet launders itself green.
572
573func ag7_match_at(buf: *u8, n: i64, p: i64, s: *u8) -> i64 {
574 var j: i64 = 0
575 var ok: i64 = 1
576 while s[j] != (0 as u8) {
577 if (p + j) >= n { ok = 0 }
578 if ok == 1 {
579 if buf[p + j] != s[j] { ok = 0 }
580 }
581 j = j + 1
582 }
583 if ok == 0 { return 0 }
584 return j
585}
586
587func ag7_digits_at(buf: *u8, n: i64, p0: i64) -> i64 {
588 var v: i64 = 0
589 var any: i64 = 0
590 var p: i64 = p0
591 var run: i64 = 1
592 while run == 1 {
593 if p >= n { run = 0 }
594 if run == 1 {
595 let c: i64 = buf[p] & 0xff
596 if c < AG7_DIG_LO { run = 0 }
597 if run == 1 {
598 if c > AG7_DIG_HI { run = 0 }
599 }
600 if run == 1 {
601 v = v * AG7_B10 + (c - AG7_DIG_LO)
602 any = 1
603 p = p + 1
604 }
605 }
606 }
607 if any == 0 { return AG7_UNSEEDED }
608 return v
609}
610
611func ag7_ratchet_read() -> i64 {
612 let lenbox: *i64 = sys_mmap(AG7_BOX_BYTES) as *i64
613 let buf: *u8 = sys_read_file(AG7_RATCHET, lenbox)
614 if (buf as i64) == 0 { return AG7_UNSEEDED }
615 let n: i64 = lenbox[0]
616 var i: i64 = 0
617 var found: i64 = AG7_UNSEEDED
618 while i < n {
619 if found < 0 {
620 let mm: i64 = ag7_match_at(buf, n, i, "armv7a" as *u8)
621 if mm > 0 {
622 if (i + mm) < n {
623 if buf[i + mm] == (AG7_SPACE as u8) {
624 found = ag7_digits_at(buf, n, i + mm + 1)
625 }
626 }
627 }
628 }
629 var adv: i64 = 1
630 while adv == 1 {
631 if i >= n { adv = 0 }
632 if adv == 1 {
633 if buf[i] == (AG7_NL as u8) { adv = 0 }
634 i = i + 1
635 }
636 }
637 }
638 return found
639}
640
641func ag7_ratchet_write(v: i64) -> i64 {
642 let d: *u8 = sys_mmap(AG7_SCRATCH)
643 var o: i64 = 0
644 o = gv_cat(d, o, "armv7a " as *u8)
645 o = gv_catn(d, o, v)
646 d[o] = AG7_NL as u8
647 o = o + 1
648 let fd: i64 = sys_openat_wr(AG7_RATCHET, AG7_MODE_FILE)
649 if fd < 0 { return -1 }
650 sys_write(fd, d, o)
651 sys_fsync(fd)
652 sys_close(fd)
653 return o
654}
655
656// ===== main =====================================================
657
658func main(argc: i64, argv: *i64) -> i64 {
659 gv_head("nx_isa_armv7a_gate -- ARMv7-A emulator conformance, KATs encoded from the ARM Architecture Reference Manual" as *u8)
660 let ctr: *i64 = gv_ctr()
661
662 let bx: *i64 = sys_mmap(AG7_BOX_BYTES) as *i64
663 let nbuf: *u8 = sys_mmap(AG7_NB_BYTES)
664 nbuf[0] = 0 as u8
665 bx[AG7_NB_OFF] = 0
666 bx[AG7_NB_PTR] = nbuf as i64
667
668 gv_puts("subject=buildroot/runtime/nx_emu_armv7a.nx dispatch=emu_armv7a_run_mem (the only surface all 10 emulators share)" as *u8)
669 ag7_nl()
670 gv_puts("guest=1MiB little-endian ARM (not Thumb), entry 0, sp 983040, exit is Linux EABI svc with r7=1 and the status in r0" as *u8)
671 ag7_nl()
672 gv_puts("outcomes are FIVE-WAY: PASS / WRONG-ANSWER / UNSUPPORTED-instruction-class / RAN-OFF-END / FAULT" as *u8)
673 ag7_nl()
674 ag7_nl()
675
676 var a7_pass: i64 = 0
677 var a7_tot: i64 = 0
678 var o: i64 = 0
679
680 o = ag7_report("imm-arith" as *u8, ag7_k_imm_arith(), AG7_ANS, bx)
681 a7_tot = a7_tot + 1
682 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
683 gv_check("isa-armv7a-imm-arith" as *u8, o == AG7_O_PASS, ctr)
684
685 o = ag7_report("sub" as *u8, ag7_k_sub(), AG7_ANS, bx)
686 a7_tot = a7_tot + 1
687 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
688 gv_check("isa-armv7a-sub" as *u8, o == AG7_O_PASS, ctr)
689
690 o = ag7_report("logic-orr-then-and" as *u8, ag7_k_logic(), AG7_SIXTY, bx)
691 a7_tot = a7_tot + 1
692 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
693 gv_check("isa-armv7a-logic-orr-then-and" as *u8, o == AG7_O_PASS, ctr)
694
695 o = ag7_report("eor" as *u8, ag7_k_eor(), AG7_ANS, bx)
696 a7_tot = a7_tot + 1
697 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
698 gv_check("isa-armv7a-eor" as *u8, o == AG7_O_PASS, ctr)
699
700 o = ag7_report("bic" as *u8, ag7_k_bic(), AG7_ANS, bx)
701 a7_tot = a7_tot + 1
702 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
703 gv_check("isa-armv7a-bic" as *u8, o == AG7_O_PASS, ctr)
704
705 o = ag7_report("rsb-operand-order" as *u8, ag7_k_rsb(), AG7_ANS, bx)
706 a7_tot = a7_tot + 1
707 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
708 gv_check("isa-armv7a-rsb-operand-order" as *u8, o == AG7_O_PASS, ctr)
709
710 o = ag7_report("predication-true-must-execute" as *u8, ag7_k_pred_taken(), AG7_ANS, bx)
711 a7_tot = a7_tot + 1
712 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
713 gv_check("isa-armv7a-predication-true-must-execute" as *u8, o == AG7_O_PASS, ctr)
714
715 o = ag7_report("predication-false-must-skip" as *u8, ag7_k_pred_skipped(), AG7_ANS, bx)
716 a7_tot = a7_tot + 1
717 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
718 gv_check("isa-armv7a-predication-false-must-skip" as *u8, o == AG7_O_PASS, ctr)
719
720 o = ag7_report("conditional-branch-loop" as *u8, ag7_k_branch_loop(), AG7_SUMTO9, bx)
721 a7_tot = a7_tot + 1
722 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
723 gv_check("isa-armv7a-conditional-branch-loop" as *u8, o == AG7_O_PASS, ctr)
724
725 o = ag7_report("signed-condition-lt-vs-ge" as *u8, ag7_k_signed_cond(), AG7_ANS, bx)
726 a7_tot = a7_tot + 1
727 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
728 gv_check("isa-armv7a-signed-condition-lt-vs-ge" as *u8, o == AG7_O_PASS, ctr)
729
730 o = ag7_report("shifted-register-operand2" as *u8, ag7_k_shifted_operand(), AG7_ANS, bx)
731 a7_tot = a7_tot + 1
732 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
733 gv_check("isa-armv7a-shifted-register-operand2" as *u8, o == AG7_O_PASS, ctr)
734
735 o = ag7_report("rotated-immediate" as *u8, ag7_k_rot_imm(), AG7_ANS, bx)
736 a7_tot = a7_tot + 1
737 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
738 gv_check("isa-armv7a-rotated-immediate" as *u8, o == AG7_O_PASS, ctr)
739
740 o = ag7_report("mla" as *u8, ag7_k_mla(), AG7_ANS, bx)
741 a7_tot = a7_tot + 1
742 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
743 gv_check("isa-armv7a-mla" as *u8, o == AG7_O_PASS, ctr)
744
745 o = ag7_report("load-store-negative-offset" as *u8, ag7_k_load_store(), AG7_ANS, bx)
746 a7_tot = a7_tot + 1
747 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
748 gv_check("isa-armv7a-load-store-negative-offset" as *u8, o == AG7_O_PASS, ctr)
749
750 o = ag7_report("ldrb-loads-one-byte" as *u8, ag7_k_ldrb(), AG7_ANS, bx)
751 a7_tot = a7_tot + 1
752 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
753 gv_check("isa-armv7a-ldrb-loads-one-byte" as *u8, o == AG7_O_PASS, ctr)
754
755 o = ag7_report("push-pop-block-transfer" as *u8, ag7_k_push_pop(), AG7_ANS, bx)
756 a7_tot = a7_tot + 1
757 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
758 gv_check("isa-armv7a-push-pop-block-transfer" as *u8, o == AG7_O_PASS, ctr)
759
760 o = ag7_report("block-transfer-ib-addressing" as *u8, ag7_k_block_ib(), AG7_ANS, bx)
761 a7_tot = a7_tot + 1
762 if o == AG7_O_PASS { a7_pass = a7_pass + 1 }
763 gv_check("isa-armv7a-block-transfer-ib-addressing" as *u8, o == AG7_O_PASS, ctr)
764
765 // ---- the fixture must have REACHED the emulator ---------------
766 // Asserting an outcome without asserting the fixture ran is how
767 // four vacuous fixtures shipped in this estate in a single day.
768 ag7_nl()
769 gv_check("fixture-reached-armv7a-emulator-at-all" as *u8, a7_pass > 0, ctr)
770 gv_check("fixture-every-kat-was-actually-run" as *u8, a7_tot == AG7_KAT_COUNT, ctr)
771
772 // ---- negative controls, classifier side -----------------------
773 // If ag7_classify were stubbed to return PASS, every green above
774 // would be fake and only these teeth would notice.
775 let ncw: i64 = ag7_classify(ag7_k_imm_arith(), AG7_WRONGANS)
776 gv_puts(" neg-control imm-arith against a deliberately wrong want=41 -> " as *u8)
777 gv_puts(ag7_outcome_name(ncw))
778 ag7_nl()
779 gv_check("neg-control-wrong-expectation-must-not-pass" as *u8, ncw == AG7_O_WRONG, ctr)
780
781 gv_check("neg-control-unsupported-sentinel-never-reads-as-pass" as *u8, ag7_classify(AG7_UNSUPPORTED, AG7_UNSUPPORTED) == AG7_O_UNSUP, ctr)
782 gv_check("neg-control-fault-sentinel-never-reads-as-pass" as *u8, ag7_classify(AG7_FAULT, AG7_FAULT) == AG7_O_FAULT, ctr)
783 gv_check("neg-control-ranoff-sentinel-never-reads-as-pass" as *u8, ag7_classify(AG7_RANOFF, AG7_RANOFF) == AG7_O_RANOFF, ctr)
784
785 // ---- negative controls, LIVE against the emulator -------------
786 // These run real machine code through the interpreter and require
787 // it to REFUSE. A refusal that returns a plausible number instead
788 // is the whole class of defect this organ exists to catch.
789 ag7_nl()
790 let nc1: i64 = ag7_neg_coproc()
791 gv_puts(" neg-control coprocessor mrc p15 -> " as *u8)
792 gv_num(nc1)
793 ag7_nl()
794 gv_check("neg-control-unimplemented-coprocessor-class-is-refused-not-guessed" as *u8, nc1 == AG7_UNSUPPORTED, ctr)
795
796 let nc2: i64 = ag7_neg_extra_ldst()
797 gv_puts(" neg-control extra load/store space ldrh -> " as *u8)
798 gv_num(nc2)
799 ag7_nl()
800 gv_check("neg-control-extra-loadstore-not-misdecoded-as-data-processing" as *u8, nc2 == AG7_UNSUPPORTED, ctr)
801
802 let nc3: i64 = ag7_neg_uncond_space()
803 gv_puts(" neg-control unconditional-instruction space (cond 1111) dsb -> " as *u8)
804 gv_num(nc3)
805 ag7_nl()
806 gv_check("neg-control-cond-1111-is-a-different-decode-map-not-always-execute" as *u8, nc3 == AG7_UNSUPPORTED, ctr)
807
808 let nc4: i64 = ag7_neg_no_exit()
809 gv_puts(" neg-control program with no exit syscall -> " as *u8)
810 gv_num(nc4)
811 ag7_nl()
812 gv_check("neg-control-no-exit-syscall-reports-RAN-OFF-END-not-a-status" as *u8, nc4 == AG7_RANOFF, ctr)
813
814 // ---- coverage, published as a NUMBER not a verdict ------------
815 ag7_nl()
816 gv_puts("coverage armv7a=" as *u8)
817 gv_num(a7_pass)
818 gv_puts("/" as *u8)
819 gv_num(a7_tot)
820 gv_puts(" classes: imm-arith sub logic eor bic rsb predication(2) branch-loop signed-cond shifter rot-imm mla load-store ldrb block-transfer(2)" as *u8)
821 ag7_nl()
822 gv_puts("NOT COVERED and NOT claimed: Thumb/Thumb-2, halfword and signed load/store, coprocessor, VFP/NEON, MRS/MSR, any syscall but exit, the pc-as-r15 read rule" as *u8)
823 ag7_nl()
824
825 // ---- ratchet -------------------------------------------------
826 let base: i64 = ag7_ratchet_read()
827 gv_puts("ratchet armv7a base=" as *u8)
828 gv_num(base)
829 gv_puts(" now=" as *u8)
830 gv_num(a7_pass)
831 gv_puts(" (base=-1 is UNSEEDED, a named state: first sight seeds, so adoption cannot fail closed)" as *u8)
832 ag7_nl()
833
834 var no_regress: i64 = 1
835 if base >= 0 {
836 if a7_pass < base { no_regress = 0 }
837 }
838
839 var wrote: i64 = 0
840 if no_regress == 1 {
841 if base < 0 { wrote = ag7_ratchet_write(a7_pass) }
842 if wrote == 0 {
843 if a7_pass > base { wrote = ag7_ratchet_write(a7_pass) }
844 }
845 }
846 gv_puts("ratchet_bytes_written=" as *u8)
847 gv_num(wrote)
848 gv_puts(" (0 = held: neither seeded nor tightened this run)" as *u8)
849 ag7_nl()
850
851 // This dialect has no disjunction operator, so the laundering
852 // condition is computed rather than expressed.
853 var laundered: i64 = 0
854 if no_regress == 0 {
855 if wrote > 0 { laundered = 1 }
856 }
857
858 gv_check("ratchet-armv7a-did-not-regress" as *u8, no_regress == 1, ctr)
859 gv_check("ratchet-never-rewritten-on-a-regression" as *u8, laundered == 0, ctr)
860
861 // THE WORKLIST, LAST, where a tailing caller can still see it.
862 gv_puts("NONPASS: " as *u8)
863 if bx[AG7_NB_OFF] == 0 {
864 gv_puts("none -- every measured KAT matched its manual-derived expectation" as *u8)
865 }
866 if bx[AG7_NB_OFF] > 0 {
867 gv_puts(bx[AG7_NB_PTR] as *u8)
868 }
869 ag7_nl()
870
871 return gv_verdict("nx_isa_armv7a_gate" as *u8, ctr,
872 "ARMv7-A conformance measured against ARM-manual-derived KATs with five-way outcomes, four LIVE refusal controls that require the interpreter to say UNSUPPORTED or RAN-OFF-END rather than return a number, coverage published as a number, fenced by a good-when-higher ratchet that seeds on first sight and never rewrites on a fall" as *u8)
873}