nandi/rustnim · PROOF.md

⑂ 04eb29f2f77152e460b50f58935cb88305227b43

PROOF.md · 153 lines · 6.8 KBmarkdown    Blame HistoryRaw
Prove byte-identity for base16ct by enumerating whole input domains  nandithebull 1# Is the transpiled `base16ct` byte-identical?
3Short answer: **yes for every input in the domains enumerated below, and that
4is a complete enumeration for the decoder's and encoder's per-chunk
5behaviour.** For unbounded-length inputs it is a compositional argument plus
6sampling, not a proof. This document says exactly which is which, because the
7difference matters and because a transpiler that overstates its evidence is
8the thing this project exists to be the opposite of.
10Reproduce with `cargo test --test proof`. It takes about four seconds.
12## What is being compared
14`proof/main.rs` is a crate root that references base16ct 1.0.0's own module
15files in place — `error.rs`, `lower.rs`, `upper.rs`, `mixed.rs`, `display.rs`,
16each byte-for-byte as published on crates.io — and carries `lib.rs`'s
17`decoded_len`, `encoded_len` and `decode_inner` verbatim. It enumerates input
18domains and prints one line per case.
20That same file is built twice:
23rustc  proof/main.rs                        -> binary A
24rustnim proof/main.rs <modules> | nim c     -> binary B
27and `A`'s stdout is compared with `B`'s stdout using `==` on the raw bytes.
28Current result: **151,463 cases, 9,100,470 bytes, identical**.
30The output encodes everything observable about each call: the status
31(`Ok`/`Err`), the error variant, the returned length, and the returned bytes
32in hex. A difference in any of those is a difference in those bytes.
34## The domains
36| | domain | size | complete? |
37|---|---|---|---|
38| A | every two-byte input, through `lower`, `upper` and `mixed` decode | 65,536 | **exhaustive** |
39| B | every two-byte input, through `lower` and `upper` encode | 65,536 | **exhaustive** |
40| C | every single byte, through `encode_str` and `HexDisplay` (`{}`, `{:x}`, `{:X}`) | 256 | **exhaustive** |
41| D | every length 0..=128, both length functions, and a destination one byte too small | 129 | **exhaustive** |
42| E | pseudorandom inputs, lengths 0..48, mixed valid and invalid characters, decode by all three and round-trip encode | 20,000 | sampled |
44Domain E's generator is an xorshift32 written in the driver itself, so both
45binaries produce the identical sequence. It is not a source of randomness
46between runs; it is a fixed, reproducible list.
48## Why A is the interesting one
50`decode_inner` is a map over independent two-byte chunks:
53for (src, dst) in src.chunks_exact(2).zip(dst.iter_mut()) {
54    let byte = (decode_nibble(src[0]) << 4) | decode_nibble(src[1]);
55    err |= byte >> 8;
56    *dst = byte as u8;
58match err { 0 => Ok(dst), _ => Err(Error::InvalidEncoding) }
61Chunk *i* reads `src[2i]` and `src[2i+1]`, writes `dst[i]`, and contributes to
62`err` by `|=`. Nothing else crosses between iterations. So the whole function
63is determined by two things:
651. the per-chunk function `(u8, u8) -> (u8, u16)` — output byte and error
66   contribution; and
672. the iteration count, `⌊|src| / 2⌋`, and the `|=` accumulation.
69**Domain A settles (1) completely.** All 65,536 possible chunks are tried, and
70every one produces identical output. There is no untried input to that
71function. This is the part that carries base16ct's constant-time arithmetic —
72the `i16` wrapping and the arithmetic shift — and it is not sampled at all.
74**Domain D settles the iteration count** for every length up to 128, including
75the odd-length rejection and the too-small-destination rejection.
77(2) also requires that both implementations accumulate `err` the same way.
78That is visible in the emitted Nim, and it is what the following lines say:
81var err: uint16 = 0'u16
82for rsTmpIdx4 in 0 ..< int(min((src.len div int(2'i32)), rsTmpLen3)):
83  let byte: uint16 = (((decode_nibble(src[(0 + rsTmpIdx4 * int(2'i32)) + int(0'i32)]) shl 4'u16)) or decode_nibble(src[(0 + rsTmpIdx4 * int(2'i32)) + int(1'i32)]))
84  err = err or (byte shr 8'u16)
85  dst[rsTmpOff2 + rsTmpIdx4] = cast[uint8](byte)
88(That is the emitted text verbatim, redundant parentheses and all.)
90Same bounds, same indices, same accumulation. **This step is an inspection,
91not a proof**, and it is the one link in the chain that is not mechanically
92checked. Domain E exists to attack it: 20,000 inputs of varying length, half
93of them invalid, exercising the accumulation across many chunks. If the
94iteration or accumulation differed, those would diverge.
96So the honest statement is:
98> Given the emitted loop iterates `⌊|src|/2⌋` chunks and accumulates `err` by
99> `|=` — which was read, and which 20,000 multi-chunk cases are consistent
100> with — the exhaustive agreement on all 65,536 single chunks extends by
101> induction to inputs of every length.
103## Encoding
105Encoding is per byte and independent, so domain B is the complete domain of an
106encode step, and domain C is the complete domain of `encode_nibble` as reached
107through `encode_str`. The same induction applies, with no accumulator to worry
110## Does the check actually discriminate?
112A comparison that cannot fail proves nothing, so the proof was tested by
113breaking the transpiler. Mapping Rust's `>>` to a **logical** shift instead of
114an arithmetic one — precisely the error a model without integer width and
115signedness makes, and the one described in `findings/` — produces:
11886274 line(s) differ; first at line 12338:
119  rustc: "3030 l=00/1 u=00/1 m=00/1"
120  nim  : "3030 l!InvalidEncoding u!InvalidEncoding m!InvalidEncoding"
123Input `3030` is ASCII `"00"`. The real decoder returns the byte `0x00`; the
124sabotaged one rejects it. The harness names the first failing input rather
125than reporting a count.
127The proof test also fails if the oracle produces fewer than 150,000 lines or
128does not end in `done`, so a truncated run agreeing with a truncated run
129cannot pass.
131## What this does not establish
133- **Not a proof of program equivalence.** It is exhaustive over stated finite
134  domains and a structural argument beyond them. It says nothing about inputs
135  outside those domains except through that argument.
136- **Only these functions.** base16ct's public surface is covered; rustnim in
137  general is not. The 33 differential cases in `tests/cases/` are separate,
138  smaller evidence about the rest of the lowering.
139- **One platform, one pair of compilers.** rustc 1.98.1 and Nim 2.2.4 on
140  x86-64 Linux. Both were also *probed* for the specific behaviours the
141  lowering relies on, rather than assumed from documentation — see the
142  "Settled empirically" section of `DESIGN.md`.
143- **Stdout only.** Timing is not compared, so nothing here supports base16ct's
144  constant-time claim surviving the translation. The arithmetic is
145  branch-free in both, but that is an observation about the source, not a
146  measurement.
148## Trusted base
150rustc as the oracle; Nim's compiler; the driver in `proof/main.rs` being a
151faithful enumeration; and `tests/proof.rs` comparing what it says it compares.
152The first two are the same trust any differential test places in its
153compilers. The last two are 300 lines you can read.

Prove byte-identity for base16ct by enumerating whole input domains 99b8376 nandithebull 16h ago	1	# Is the transpiled `base16ct` byte-identical?
	2
	3	Short answer: **yes for every input in the domains enumerated below, and that
	4	is a complete enumeration for the decoder's and encoder's per-chunk
	5	behaviour.** For unbounded-length inputs it is a compositional argument plus
	6	sampling, not a proof. This document says exactly which is which, because the
	7	difference matters and because a transpiler that overstates its evidence is
	8	the thing this project exists to be the opposite of.
	9
	10	Reproduce with `cargo test --test proof`. It takes about four seconds.
	11
	12	## What is being compared
	13
	14	`proof/main.rs` is a crate root that references base16ct 1.0.0's own module
	15	files in place — `error.rs`, `lower.rs`, `upper.rs`, `mixed.rs`, `display.rs`,
	16	each byte-for-byte as published on crates.io — and carries `lib.rs`'s
	17	`decoded_len`, `encoded_len` and `decode_inner` verbatim. It enumerates input
	18	domains and prints one line per case.
	19
	20	That same file is built twice:
	21
	22	```
	23	rustc proof/main.rs -> binary A
	24	rustnim proof/main.rs <modules> \| nim c -> binary B
	25	```
	26
	27	and `A`'s stdout is compared with `B`'s stdout using `==` on the raw bytes.
	28	Current result: 151,463 cases, 9,100,470 bytes, identical.
	29
	30	The output encodes everything observable about each call: the status
	31	(`Ok`/`Err`), the error variant, the returned length, and the returned bytes
	32	in hex. A difference in any of those is a difference in those bytes.
	33
	34	## The domains
	35
	36	\| \| domain \| size \| complete? \|
	37	\|---\|---\|---\|---\|
	38	\| A \| every two-byte input, through `lower`, `upper` and `mixed` decode \| 65,536 \| exhaustive \|
	39	\| B \| every two-byte input, through `lower` and `upper` encode \| 65,536 \| exhaustive \|
	40	\| C \| every single byte, through `encode_str` and `HexDisplay` (`{}`, `{:x}`, `{:X}`) \| 256 \| exhaustive \|
	41	\| D \| every length 0..=128, both length functions, and a destination one byte too small \| 129 \| exhaustive \|
	42	\| E \| pseudorandom inputs, lengths 0..48, mixed valid and invalid characters, decode by all three and round-trip encode \| 20,000 \| sampled \|
	43
	44	Domain E's generator is an xorshift32 written in the driver itself, so both
	45	binaries produce the identical sequence. It is not a source of randomness
	46	between runs; it is a fixed, reproducible list.
	47
	48	## Why A is the interesting one
	49
	50	`decode_inner` is a map over independent two-byte chunks:
	51
	52	```rust
	53	for (src, dst) in src.chunks_exact(2).zip(dst.iter_mut()) {
	54	let byte = (decode_nibble(src[0]) << 4) \| decode_nibble(src[1]);
	55	err \|= byte >> 8;
	56	*dst = byte as u8;
	57	}
	58	match err { 0 => Ok(dst), _ => Err(Error::InvalidEncoding) }
	59	```
	60
	61	Chunk i reads `src[2i]` and `src[2i+1]`, writes `dst[i]`, and contributes to
	62	`err` by `\|=`. Nothing else crosses between iterations. So the whole function
	63	is determined by two things:
	64
65	1. the per-chunk function `(u8, u8) -> (u8, u16)` — output byte and error
66	contribution; and
67	2. the iteration count, `⌊\|src\| / 2⌋`, and the `\|=` accumulation.
68
69	Domain A settles (1) completely. All 65,536 possible chunks are tried, and
70	every one produces identical output. There is no untried input to that
71	function. This is the part that carries base16ct's constant-time arithmetic —
72	the `i16` wrapping and the arithmetic shift — and it is not sampled at all.
73
74	Domain D settles the iteration count for every length up to 128, including
75	the odd-length rejection and the too-small-destination rejection.
76
77	(2) also requires that both implementations accumulate `err` the same way.
78	That is visible in the emitted Nim, and it is what the following lines say:
79
80	```nim
81	var err: uint16 = 0'u16
82	for rsTmpIdx4 in 0 ..< int(min((src.len div int(2'i32)), rsTmpLen3)):
83	let byte: uint16 = (((decode_nibble(src[(0 + rsTmpIdx4 * int(2'i32)) + int(0'i32)]) shl 4'u16)) or decode_nibble(src[(0 + rsTmpIdx4 * int(2'i32)) + int(1'i32)]))
84	err = err or (byte shr 8'u16)
85	dst[rsTmpOff2 + rsTmpIdx4] = cast[uint8](byte)
86	```
87
88	(That is the emitted text verbatim, redundant parentheses and all.)
89
90	Same bounds, same indices, same accumulation. **This step is an inspection,
91	not a proof**, and it is the one link in the chain that is not mechanically
92	checked. Domain E exists to attack it: 20,000 inputs of varying length, half
93	of them invalid, exercising the accumulation across many chunks. If the
94	iteration or accumulation differed, those would diverge.
95
96	So the honest statement is:
97
98	> Given the emitted loop iterates `⌊\|src\|/2⌋` chunks and accumulates `err` by
99	> `\|=` — which was read, and which 20,000 multi-chunk cases are consistent
100	> with — the exhaustive agreement on all 65,536 single chunks extends by
101	> induction to inputs of every length.
102
103	## Encoding
104
105	Encoding is per byte and independent, so domain B is the complete domain of an
106	encode step, and domain C is the complete domain of `encode_nibble` as reached
107	through `encode_str`. The same induction applies, with no accumulator to worry
108	about.
109
110	## Does the check actually discriminate?
111
112	A comparison that cannot fail proves nothing, so the proof was tested by
113	breaking the transpiler. Mapping Rust's `>>` to a logical shift instead of
114	an arithmetic one — precisely the error a model without integer width and
115	signedness makes, and the one described in `findings/` — produces:
116
117	```
118	86274 line(s) differ; first at line 12338:
119	rustc: "3030 l=00/1 u=00/1 m=00/1"
120	nim : "3030 l!InvalidEncoding u!InvalidEncoding m!InvalidEncoding"
121	```
122
123	Input `3030` is ASCII `"00"`. The real decoder returns the byte `0x00`; the
124	sabotaged one rejects it. The harness names the first failing input rather
125	than reporting a count.
126
127	The proof test also fails if the oracle produces fewer than 150,000 lines or
128	does not end in `done`, so a truncated run agreeing with a truncated run
129	cannot pass.
130
131	## What this does not establish
132
133	- Not a proof of program equivalence. It is exhaustive over stated finite
134	domains and a structural argument beyond them. It says nothing about inputs
135	outside those domains except through that argument.
136	- Only these functions. base16ct's public surface is covered; rustnim in
137	general is not. The 33 differential cases in `tests/cases/` are separate,
138	smaller evidence about the rest of the lowering.
139	- One platform, one pair of compilers. rustc 1.98.1 and Nim 2.2.4 on
140	x86-64 Linux. Both were also probed for the specific behaviours the
141	lowering relies on, rather than assumed from documentation — see the
142	"Settled empirically" section of `DESIGN.md`.
143	- Stdout only. Timing is not compared, so nothing here supports base16ct's
144	constant-time claim surviving the translation. The arithmetic is
145	branch-free in both, but that is an observation about the source, not a
146	measurement.
147
148	## Trusted base
149
150	rustc as the oracle; Nim's compiler; the driver in `proof/main.rs` being a
151	faithful enumeration; and `tests/proof.rs` comparing what it says it compares.
152	The first two are the same trust any differential test places in its
153	compilers. The last two are 300 lines you can read.