code wiki / _hdl_build / nx_totp_extvec_gate.nx

nx_totp_extvec_gate.nx

buildroot/runtime/_hdl_build/nx_totp_extvec_gate.nx

13455 B289 linesdepth 5pulls 7 transitivereach 0 importersview sourcekind gate/prooftopic totp
docsdependenciesstructsconstsfunctions

about

nx_totp_extvec_gate.nx -- TOTP vs RFC 6238 Appendix B, all SIX published SHA-1 vectors. COMPLETES THE 2FA CHAIN. nx_hotp_extvec_gate proved HOTP (RFC 4226, 10/10). This proves TOTP, which adds the TIME-STEP DERIVATION T = floor(unix_time / X) on top of HOTP and uses EIGHT digits rather than six. ★Neither addition is implied by the other: an 8-digit dynamic truncation exercises a different modulus than 6, and T-derivation is integer division that nothing below it can validate. TWO INDEPENDENT CHECKS PER ROW, because the table publishes enough to separate them: 1. DERIVED T -- our own time/30 must equal the document's "Value of T (Hex)" column 2. TOTP CODE -- totp_sha1_value(seed, 20, time, 30, 8) must equal the document's TOTP column ★IF ONLY THE CODE WERE CHECKED, A WRONG T AND A COMPENSATING TRUNCATION BUG COULD CANCEL. Checking the intermediate the authority happened to publish makes that impossible -- USE EVERY COLUMN THE AUTHORITY GIVES YOU; THE INTERMEDIATE ONES ARE THERE TO LOCALISE FAILURES. ⚠SCOPE, STATED HONESTLY: RFC 6238 publishes EIGHTEEN rows -- 6 time points x {SHA1, SHA256, SHA512}. This gate grades the SIX SHA-1 rows only, because this tree has TOTP over SHA-1 and not over SHA-256 or SHA-512. The other twelve are NOT skipped-and-forgotten: they are counted and reported as UNIMPLEMENTED-MODE, which is a capability gap, not a pass. ★A ROW YOU CANNOT COMPUTE IS NOT A ROW YOU PASSED, AND CALLING IT "N/A" IN SILENCE IS HOW COVERAGE INFLATES. ⚠THE SEED IS READ FROM THE DOCUMENT (`String seed = "3132...3930";`) -- 20 bytes, never typed from recall. ★THE KEY IS AN ANSWER TOO. ⚠ROW SELECTION IS BY THE EXACT CELL "| SHA1 |" (two spaces). "SHA1" alone is NOT a safe discriminator here because SHA256/SHA512 rows exist; a substring test would grade all eighteen against a SHA-1 implementation. ★A SUBSTRING NEEDLE FLATTERS SILENTLY. license_tier: ORIGINAL expect_exit: 0

dependencies 4 imports · 0 importers

nx_syscalls.nx nx_sha256_wasm.nx nx_totp_sha1.nx nx_gate_verdict.nx nx_totp_extvec_gate.nx

imports: nx_syscalls.nxnx_sha256_wasm.nxnx_totp_sha1.nxnx_gate_verdict.nx

imported by: nobody (leaf or entry point)

call flow from main pre-order; caps 40 nodes / depth 6 declared; ↻ = already shown

main w sys_write sys_mmap nxa_die sys_write ↻ sys_exit nxa_lock_take nxa_lock_addr sys_write ↻ nxa_lock_give nxa_lock_addr ↻ nxa_report_overrun sys_write ↻ nxa_dump_printable sys_write ↻ nxa_dump_sizes sys_write ↻ sys_read_file sys_openat_rd sys_lseek sys_mmap ↻ sys_read sys_munmap sys_close nx_sha256_one_shot _h_set _sha256_compress _blk_word_be _rotr32 _h_get _sha256_k _h_set ↻ _h_get ↻ hexnib wb sys_write ↻ findfrom starts parsehex_run

structs

none

consts

none

functions

32func w(s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(1, s, n); return 0 }
called by 2: nnmain calls 1: sys_write
33func wb(b: *u8, n: i64) -> i64 { sys_write(1, b, n); return 0 }
called by 1: main calls 1: sys_write
35func nn(v: i64) -> i64
called by 1: main calls 3: wsys_mmapsys_write
49func hexnib(v: i64) -> i64 { if v < 10 { return 48 + v } return 87 + v }
called by 1: main
50func hexval(c: i64) -> i64
56func isws(c: i64) -> i64
63func starts(b: *u8, n: i64, at: i64, s: *u8) -> i64
called by 1: findfrom
72func findfrom(b: *u8, n: i64, s: *u8, from: i64) -> i64
called by 1: main calls 1: starts
78func parsehex_run(b: *u8, n: i64, from: i64, out: *u8, want: i64) -> i64
called by 1: main calls 1: hexval
95func next_dec(b: *u8, n: i64, p0: i64, endp: *i64) -> i64
called by 1: main calls 1: isws
120func next_hex_i64(b: *u8, n: i64, p0: i64, want: i64, endp: *i64) -> i64
called by 1: main calls 2: iswshexval
142func main() -> i64