rickub
Sign in Get started
nandi/rustnimpublic⑂ Fork 0
⑂ 99b8376
Branches
main View all branches → View all tags →
Commits
⬇ Clone ▾
git clone https://git.rickub.com/nandi/rustnim.git
git clone ssh://git@rickub.com/nandi/rustnim.git

Host key fingerprint (ed25519): SHA256:iycHnxEyq0Q7uyVpB7JlznP0G7JrTPXLYRcAU5CSLhc — verify it before your first connect.

Prove byte-identity for base16ct by enumerating whole input domains

"Byte-identical" had been resting on a dozen hand-written cases, which is
evidence, not a proof. proof/main.rs is a driver that references base16ct's
five module files in place -- so it cannot drift from what the crate case
transpiles -- and enumerates input domains rather than examples: every
two-byte decode input through all three decoders (65,536, the complete domain
of one decode chunk), every two-byte encode input through both encoders
(65,536), every single byte through encode_str and HexDisplay, every length
to 128 including the odd-length and short-destination rejections, and 20,000
pseudorandom multi-chunk cases from an xorshift32 written into the driver so
both sides produce the identical sequence.

Both binaries print one line per case, encoding status, error variant,
returned length and returned bytes. 151,463 cases, 9,100,470 bytes, compared
with `==` on the raw bytes: identical.

PROOF.md states what that does and does not establish. Domain A is exhaustive
over the per-chunk function, which is the part carrying the constant-time i16
arithmetic, so that is settled with nothing left untried. Extending it to
inputs of any length is an induction whose one unmechanised step -- that both
loops iterate the same chunks and accumulate err the same way -- is an
inspection of the emitted Nim, quoted verbatim, with domain E there to attack
it. The document says so rather than letting the word "proof" carry more than
it should.

The check was tested by breaking the transpiler, because a comparison that
cannot fail proves nothing. Mapping `>>` to a logical shift -- the exact
error a model without integer width makes, and the one in findings/ --
diverges on 86,274 lines, first at input "3030", ASCII "00".

That sabotage also found a wrong claim of my own. DESIGN.md said Nim's `T(x)`
range-checks and that `cast` was therefore the only faithful spelling of
Rust's `as`. Sabotaging cast to `T(x)` changed nothing, because Nim truncates
there too: uint8(511'u16) is 255, uint8(300'i32) is 44, uint8(-1'i32) is 255.
The conclusion stands but the reason was wrong, and it had been assumed
rather than probed. Both the document and the code comment now say what is
true and how it was established.

Two lowering fixes fell out of writing the driver: `let x = &mut buf[..n]`
must bind a `var`, since Rust may write through it and Nim only accepts a
`var` where a `var` parameter is wanted; and `let s = &buf[..n]` now binds an
alias, because Nim will not let a `let` borrow out of a local and a view is a
reference with nothing to materialise -- restricted to initialisers that are
side-effect-free place expressions, so substituting re-evaluates nothing.

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
nandithebull committed 2026-09-18T20:48:38-07:00 Browse files
99b8376 parent: afb2a6e
modified DESIGN.md +24 -5
@@ -267,26 +267,45 @@ runner) rather than a wrong answer.
267267 4. **`char` round-trips.** Rust `char` → Nim `Rune`, confirmed for ASCII and
268268 non-ASCII scalars in both `{}` and `{:?}`, and across `as u32`
269269 (`tests/cases/014`).
270+5. **Nim's integer conversion `T(x)` truncates; it does not range-check.**
271+ `uint8(511'u16)` is `255`, `uint8(300'i32)` is `44`, `uint8(-1'i32)` is
272+ `255` — the same answers as `cast[uint8]`. An earlier version of this
273+ document asserted that `T(x)` range-checks, and used that to justify
274+ `cast`. The conclusion stands — `cast` is the clearer spelling of
275+ "truncate" — but the stated reason was wrong, and it had been assumed
276+ rather than probed. Found by sabotaging the cast lowering and watching the
277+ exhaustive proof *not* fail, which is what a sabotage test is for.
270278
271279 ### Still open
272280
273-5. `checked_*` and `saturating_*` are not mapped yet; they are currently
281+6. `checked_*` and `saturating_*` are not mapped yet; they are currently
274282 rejected as unsupported methods rather than approximated.
275-6. Generics (type and const parameters), `move` closures, closure bodies with
283+7. Generics (type and const parameters), `move` closures, closure bodies with
276284 statements, and trait impls other than the formatting traits and `From` are
277285 rejected with a reason.
278286 Lifetime parameters are *not* a rejection: they carry no runtime meaning
279287 and Nim is GC'd, so `fn encode<'a>(..)` lowers fine.
280-7. Float formatting matches Rust for ordinary values and for `inf`/`NaN`, but
288+8. Float formatting matches Rust for ordinary values and for `inf`/`NaN`, but
281289 the exponent-form thresholds have only been checked at `1e21`.
282-8. Functions are scoped by module now, but *types* are still global: two
290+9. Functions are scoped by module now, but *types* are still global: two
283291 modules declaring the same type name would collide. Relatedly, a crate's
284292 own `type Result<T>` is told apart from the builtin `Result<T, E>` by
285293 arity, which is not how Rust resolves it.
286-9. `String::from_utf8_unchecked` copies, because Nim's `string` is an owned
294+10. `String::from_utf8_unchecked` copies, because Nim's `string` is an owned
287295 value. Rust's consumes the `Vec` without copying. Observably the same from
288296 the caller, but it is a copy where Rust has none.
289297
298+## Proof of byte-identity for `base16ct`
299+
300+[`PROOF.md`](PROOF.md) sets out what is actually established: exhaustive
301+agreement over every two-byte decode input (65,536), every two-byte encode
302+input (65,536), every single byte through `encode_str` and `HexDisplay`, and
303+every length to 128 — plus a compositional argument extending those to inputs
304+of any length, and 20,000 pseudorandom multi-chunk cases attacking the one
305+step in that argument that is inspection rather than enumeration. Run it with
306+`cargo test --test proof`. It is explicit about the difference between the
307+exhaustive parts and the sampled ones.
308+
290309 ## Testing: differential, not golden
291310
292311 The bar is **behavioural equivalence with rustc**, not that the output looks
@@ -267,26 +267,45 @@ runner) rather than a wrong answer.
267 4. **`char` round-trips.** Rust `char` → Nim `Rune`, confirmed for ASCII and267 4. **`char` round-trips.** Rust `char` → Nim `Rune`, confirmed for ASCII and
268 non-ASCII scalars in both `{}` and `{:?}`, and across `as u32`268 non-ASCII scalars in both `{}` and `{:?}`, and across `as u32`
269 (`tests/cases/014`).269 (`tests/cases/014`).
270+5. **Nim's integer conversion `T(x)` truncates; it does not range-check.**
271+ `uint8(511'u16)` is `255`, `uint8(300'i32)` is `44`, `uint8(-1'i32)` is
272+ `255` — the same answers as `cast[uint8]`. An earlier version of this
273+ document asserted that `T(x)` range-checks, and used that to justify
274+ `cast`. The conclusion stands — `cast` is the clearer spelling of
275+ "truncate" — but the stated reason was wrong, and it had been assumed
276+ rather than probed. Found by sabotaging the cast lowering and watching the
277+ exhaustive proof *not* fail, which is what a sabotage test is for.
270 278
271 ### Still open279 ### Still open
272 280
273-5. `checked_*` and `saturating_*` are not mapped yet; they are currently281+6. `checked_*` and `saturating_*` are not mapped yet; they are currently
274 rejected as unsupported methods rather than approximated.282 rejected as unsupported methods rather than approximated.
275-6. Generics (type and const parameters), `move` closures, closure bodies with283+7. Generics (type and const parameters), `move` closures, closure bodies with
276 statements, and trait impls other than the formatting traits and `From` are284 statements, and trait impls other than the formatting traits and `From` are
277 rejected with a reason.285 rejected with a reason.
278 Lifetime parameters are *not* a rejection: they carry no runtime meaning286 Lifetime parameters are *not* a rejection: they carry no runtime meaning
279 and Nim is GC'd, so `fn encode<'a>(..)` lowers fine.287 and Nim is GC'd, so `fn encode<'a>(..)` lowers fine.
280-7. Float formatting matches Rust for ordinary values and for `inf`/`NaN`, but288+8. Float formatting matches Rust for ordinary values and for `inf`/`NaN`, but
281 the exponent-form thresholds have only been checked at `1e21`.289 the exponent-form thresholds have only been checked at `1e21`.
282-8. Functions are scoped by module now, but *types* are still global: two290+9. Functions are scoped by module now, but *types* are still global: two
283 modules declaring the same type name would collide. Relatedly, a crate's291 modules declaring the same type name would collide. Relatedly, a crate's
284 own `type Result<T>` is told apart from the builtin `Result<T, E>` by292 own `type Result<T>` is told apart from the builtin `Result<T, E>` by
285 arity, which is not how Rust resolves it.293 arity, which is not how Rust resolves it.
286-9. `String::from_utf8_unchecked` copies, because Nim's `string` is an owned294+10. `String::from_utf8_unchecked` copies, because Nim's `string` is an owned
287 value. Rust's consumes the `Vec` without copying. Observably the same from295 value. Rust's consumes the `Vec` without copying. Observably the same from
288 the caller, but it is a copy where Rust has none.296 the caller, but it is a copy where Rust has none.
289 297
298+## Proof of byte-identity for `base16ct`
299+
300+[`PROOF.md`](PROOF.md) sets out what is actually established: exhaustive
301+agreement over every two-byte decode input (65,536), every two-byte encode
302+input (65,536), every single byte through `encode_str` and `HexDisplay`, and
303+every length to 128 — plus a compositional argument extending those to inputs
304+of any length, and 20,000 pseudorandom multi-chunk cases attacking the one
305+step in that argument that is inspection rather than enumeration. Run it with
306+`cargo test --test proof`. It is explicit about the difference between the
307+exhaustive parts and the sampled ones.
308+
290 ## Testing: differential, not golden309 ## Testing: differential, not golden
291 310
292 The bar is **behavioural equivalence with rustc**, not that the output looks311 The bar is **behavioural equivalence with rustc**, not that the output looks
added PROOF.md +153 -0
new file mode 100644
@@ -0,0 +1,153 @@
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.
new file mode 100644
@@ -0,0 +1,153 @@
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.
modified README.md +7 -0
@@ -69,6 +69,13 @@ once per byte into the formatter.
6969 That is the crate the transpiler in [`findings/`](findings/) emitted an empty
7070 file for, while exiting 0.
7171
72+How strong is "byte-identical"? [`PROOF.md`](PROOF.md) answers that precisely:
73+exhaustive over every two-byte decode input, every two-byte encode input and
74+every single byte through `encode_str`/`HexDisplay`, plus a compositional
75+argument for longer inputs and 20,000 pseudorandom cases attacking it.
76+`cargo test --test proof` runs it — 151,463 cases, 9.1 MB of output, compared
77+byte for byte.
78+
7279 ## Tests
7380
7481 ```bash
@@ -69,6 +69,13 @@ once per byte into the formatter.
69 That is the crate the transpiler in [`findings/`](findings/) emitted an empty69 That is the crate the transpiler in [`findings/`](findings/) emitted an empty
70 file for, while exiting 0.70 file for, while exiting 0.
71 71
72+How strong is "byte-identical"? [`PROOF.md`](PROOF.md) answers that precisely:
73+exhaustive over every two-byte decode input, every two-byte encode input and
74+every single byte through `encode_str`/`HexDisplay`, plus a compositional
75+argument for longer inputs and 20,000 pseudorandom cases attacking it.
76+`cargo test --test proof` runs it — 151,463 cases, 9.1 MB of output, compared
77+byte for byte.
78+
72 ## Tests79 ## Tests
73 80
74 ```bash81 ```bash
added proof/main.rs +222 -0
new file mode 100644
@@ -0,0 +1,222 @@
1+//@ cfg: feature=alloc
2+// Exhaustive differential driver for base16ct.
3+//
4+// This is the crate root for the proof harness. The five module files are the
5+// crate's own sources, referenced in place rather than copied, so this cannot
6+// drift from what `tests/cases/026-base16ct-crate/` transpiles. `lib.rs`'s
7+// core is carried here verbatim, as it is there.
8+//
9+// The point of this file is to enumerate *entire input domains* rather than a
10+// handful of examples. See PROOF.md for what that does and does not establish.
11+
12+#[path = "../tests/cases/026-base16ct-crate/display.rs"]
13+mod display;
14+#[path = "../tests/cases/026-base16ct-crate/error.rs"]
15+mod error;
16+#[path = "../tests/cases/026-base16ct-crate/lower.rs"]
17+mod lower;
18+#[path = "../tests/cases/026-base16ct-crate/mixed.rs"]
19+mod mixed;
20+#[path = "../tests/cases/026-base16ct-crate/upper.rs"]
21+mod upper;
22+
23+#[cfg(feature = "alloc")]
24+pub use std::{string::String, vec::Vec};
25+
26+pub use crate::display::HexDisplay;
27+pub use crate::error::{Error, Result};
28+
29+/// Compute decoded length of the given hex-encoded input.
30+#[inline(always)]
31+pub fn decoded_len(bytes: &[u8]) -> Result<usize> {
32+ if bytes.len() & 1 == 0 {
33+ Ok(bytes.len() / 2)
34+ } else {
35+ Err(Error::InvalidLength)
36+ }
37+}
38+
39+/// Get the length of Base16 (hex) produced by encoding the given bytes.
40+#[inline(always)]
41+pub fn encoded_len(bytes: &[u8]) -> usize {
42+ bytes.len() * 2
43+}
44+
45+fn decode_inner<'a>(
46+ src: &[u8],
47+ dst: &'a mut [u8],
48+ decode_nibble: impl Fn(u8) -> u16,
49+) -> Result<&'a [u8]> {
50+ let dst = dst
51+ .get_mut(..decoded_len(src)?)
52+ .ok_or(Error::InvalidLength)?;
53+
54+ let mut err: u16 = 0;
55+ for (src, dst) in src.chunks_exact(2).zip(dst.iter_mut()) {
56+ let byte = (decode_nibble(src[0]) << 4) | decode_nibble(src[1]);
57+ err |= byte >> 8;
58+ *dst = byte as u8;
59+ }
60+
61+ match err {
62+ 0 => Ok(dst),
63+ _ => Err(Error::InvalidEncoding),
64+ }
65+}
66+
67+// --------------------------------------------------------------- reporting
68+
69+/// One decode result, rendered so that any difference in status, length or
70+/// content shows up as a difference in these bytes.
71+fn report(tag: &str, r: Result<&[u8]>) {
72+ match r {
73+ Ok(v) => {
74+ print!("{}=", tag);
75+ for b in v.iter() {
76+ print!("{:02x}", b);
77+ }
78+ print!("/{}", v.len());
79+ }
80+ Err(e) => print!("{}!{:?}", tag, e),
81+ }
82+}
83+
84+fn main() {
85+ // -- Domain A: every two-byte input, all three decoders. 65,536 inputs,
86+ // which is the complete domain of a single decode chunk and therefore
87+ // pins the nibble function exactly.
88+ println!("A two-byte decode, exhaustive");
89+ let mut hi: u32 = 0;
90+ while hi < 256 {
91+ let mut lo: u32 = 0;
92+ while lo < 256 {
93+ let src: [u8; 2] = [hi as u8, lo as u8];
94+ let mut b1 = [0u8; 4];
95+ let mut b2 = [0u8; 4];
96+ let mut b3 = [0u8; 4];
97+ print!("{:02x}{:02x} ", hi, lo);
98+ report("l", lower::decode(&src, &mut b1));
99+ print!(" ");
100+ report("u", upper::decode(&src, &mut b2));
101+ print!(" ");
102+ report("m", mixed::decode(&src, &mut b3));
103+ println!("");
104+ lo += 1;
105+ }
106+ hi += 1;
107+ }
108+
109+ // -- Domain B: every two-byte input, both encoders. Encoding is defined
110+ // per byte, so this is the complete domain of an encode step too.
111+ println!("B two-byte encode, exhaustive");
112+ let mut a: u32 = 0;
113+ while a < 256 {
114+ let mut b: u32 = 0;
115+ while b < 256 {
116+ let src: [u8; 2] = [a as u8, b as u8];
117+ let mut e1 = [0u8; 4];
118+ let mut e2 = [0u8; 4];
119+ print!("{:02x}{:02x} ", a, b);
120+ report("l", lower::encode(&src, &mut e1));
121+ print!(" ");
122+ report("u", upper::encode(&src, &mut e2));
123+ println!("");
124+ b += 1;
125+ }
126+ a += 1;
127+ }
128+
129+ // -- Domain C: every single byte, encode_str and HexDisplay.
130+ println!("C single-byte encode_str and HexDisplay, exhaustive");
131+ let mut c: u32 = 0;
132+ while c < 256 {
133+ let src: [u8; 1] = [c as u8];
134+ let mut e = [0u8; 2];
135+ match lower::encode_str(&src, &mut e) {
136+ Ok(s) => print!("{:02x} s={} ", c, s),
137+ Err(er) => print!("{:02x} s!{:?} ", c, er),
138+ }
139+ println!("x={:x} X={:X} d={}", HexDisplay(&src), HexDisplay(&src), HexDisplay(&src));
140+ c += 1;
141+ }
142+
143+ // -- Domain D: lengths 0..=128, both length functions and the buffer-size
144+ // boundary. Covers odd/even and the too-small-destination path.
145+ println!("D lengths, exhaustive to 128");
146+ let big = [b'a'; 128];
147+ let mut n: usize = 0;
148+ while n <= 128 {
149+ let src = &big[..n];
150+ match decoded_len(src) {
151+ Ok(v) => print!("{} dl={} el={}", n, v, encoded_len(src)),
152+ Err(e) => print!("{} dl!{:?} el={}", n, e, encoded_len(src)),
153+ }
154+ // Destination exactly one byte too small, to exercise the bound.
155+ let mut tight = [0u8; 64];
156+ let want = n / 2;
157+ if want > 0 && want <= 64 {
158+ let fit = &mut tight[..want - 1];
159+ print!(" ");
160+ report("t", mixed::decode(src, fit));
161+ }
162+ println!("");
163+ n += 1;
164+ }
165+
166+ // -- Domain E: pseudorandom inputs of varied length, from a generator
167+ // defined here so both sides produce the identical sequence.
168+ println!("E pseudorandom, 20000 cases");
169+ let mut state: u32 = 2463534242;
170+ let mut i: u32 = 0;
171+ while i < 20000 {
172+ // xorshift32, chosen because it is exactly representable in both
173+ // languages: u32 wrapping shifts and xor, nothing else.
174+ state ^= state << 13;
175+ state ^= state >> 17;
176+ state ^= state << 5;
177+ let len: usize = (state % 49) as usize;
178+
179+ let mut buf = [0u8; 48];
180+ let mut j: usize = 0;
181+ while j < len {
182+ state ^= state << 13;
183+ state ^= state >> 17;
184+ state ^= state << 5;
185+ // Mostly hex characters, sometimes not, so both the accepting and
186+ // the rejecting paths are exercised.
187+ let pick = state % 20;
188+ if pick < 16 {
189+ let d = (state >> 8) % 16;
190+ if d < 10 {
191+ buf[j] = 48 + d as u8;
192+ } else if (state >> 4) % 2 == 0 {
193+ buf[j] = 87 + d as u8;
194+ } else {
195+ buf[j] = 55 + d as u8;
196+ }
197+ } else {
198+ buf[j] = (state >> 16) as u8;
199+ }
200+ j += 1;
201+ }
202+ let src = &buf[..len];
203+
204+ let mut d1 = [0u8; 24];
205+ let mut d2 = [0u8; 24];
206+ let mut d3 = [0u8; 24];
207+ print!("{} {} ", i, len);
208+ report("l", lower::decode(src, &mut d1));
209+ print!(" ");
210+ report("u", upper::decode(src, &mut d2));
211+ print!(" ");
212+ report("m", mixed::decode(src, &mut d3));
213+
214+ // Round trip: encode the bytes, decode them back.
215+ let mut enc = [0u8; 96];
216+ report(" e", lower::encode(src, &mut enc));
217+ println!("");
218+ i += 1;
219+ }
220+
221+ println!("done");
222+}
new file mode 100644
@@ -0,0 +1,222 @@
1+//@ cfg: feature=alloc
2+// Exhaustive differential driver for base16ct.
3+//
4+// This is the crate root for the proof harness. The five module files are the
5+// crate's own sources, referenced in place rather than copied, so this cannot
6+// drift from what `tests/cases/026-base16ct-crate/` transpiles. `lib.rs`'s
7+// core is carried here verbatim, as it is there.
8+//
9+// The point of this file is to enumerate *entire input domains* rather than a
10+// handful of examples. See PROOF.md for what that does and does not establish.
11+
12+#[path = "../tests/cases/026-base16ct-crate/display.rs"]
13+mod display;
14+#[path = "../tests/cases/026-base16ct-crate/error.rs"]
15+mod error;
16+#[path = "../tests/cases/026-base16ct-crate/lower.rs"]
17+mod lower;
18+#[path = "../tests/cases/026-base16ct-crate/mixed.rs"]
19+mod mixed;
20+#[path = "../tests/cases/026-base16ct-crate/upper.rs"]
21+mod upper;
22+
23+#[cfg(feature = "alloc")]
24+pub use std::{string::String, vec::Vec};
25+
26+pub use crate::display::HexDisplay;
27+pub use crate::error::{Error, Result};
28+
29+/// Compute decoded length of the given hex-encoded input.
30+#[inline(always)]
31+pub fn decoded_len(bytes: &[u8]) -> Result<usize> {
32+ if bytes.len() & 1 == 0 {
33+ Ok(bytes.len() / 2)
34+ } else {
35+ Err(Error::InvalidLength)
36+ }
37+}
38+
39+/// Get the length of Base16 (hex) produced by encoding the given bytes.
40+#[inline(always)]
41+pub fn encoded_len(bytes: &[u8]) -> usize {
42+ bytes.len() * 2
43+}
44+
45+fn decode_inner<'a>(
46+ src: &[u8],
47+ dst: &'a mut [u8],
48+ decode_nibble: impl Fn(u8) -> u16,
49+) -> Result<&'a [u8]> {
50+ let dst = dst
51+ .get_mut(..decoded_len(src)?)
52+ .ok_or(Error::InvalidLength)?;
53+
54+ let mut err: u16 = 0;
55+ for (src, dst) in src.chunks_exact(2).zip(dst.iter_mut()) {
56+ let byte = (decode_nibble(src[0]) << 4) | decode_nibble(src[1]);
57+ err |= byte >> 8;
58+ *dst = byte as u8;
59+ }
60+
61+ match err {
62+ 0 => Ok(dst),
63+ _ => Err(Error::InvalidEncoding),
64+ }
65+}
66+
67+// --------------------------------------------------------------- reporting
68+
69+/// One decode result, rendered so that any difference in status, length or
70+/// content shows up as a difference in these bytes.
71+fn report(tag: &str, r: Result<&[u8]>) {
72+ match r {
73+ Ok(v) => {
74+ print!("{}=", tag);
75+ for b in v.iter() {
76+ print!("{:02x}", b);
77+ }
78+ print!("/{}", v.len());
79+ }
80+ Err(e) => print!("{}!{:?}", tag, e),
81+ }
82+}
83+
84+fn main() {
85+ // -- Domain A: every two-byte input, all three decoders. 65,536 inputs,
86+ // which is the complete domain of a single decode chunk and therefore
87+ // pins the nibble function exactly.
88+ println!("A two-byte decode, exhaustive");
89+ let mut hi: u32 = 0;
90+ while hi < 256 {
91+ let mut lo: u32 = 0;
92+ while lo < 256 {
93+ let src: [u8; 2] = [hi as u8, lo as u8];
94+ let mut b1 = [0u8; 4];
95+ let mut b2 = [0u8; 4];
96+ let mut b3 = [0u8; 4];
97+ print!("{:02x}{:02x} ", hi, lo);
98+ report("l", lower::decode(&src, &mut b1));
99+ print!(" ");
100+ report("u", upper::decode(&src, &mut b2));
101+ print!(" ");
102+ report("m", mixed::decode(&src, &mut b3));
103+ println!("");
104+ lo += 1;
105+ }
106+ hi += 1;
107+ }
108+
109+ // -- Domain B: every two-byte input, both encoders. Encoding is defined
110+ // per byte, so this is the complete domain of an encode step too.
111+ println!("B two-byte encode, exhaustive");
112+ let mut a: u32 = 0;
113+ while a < 256 {
114+ let mut b: u32 = 0;
115+ while b < 256 {
116+ let src: [u8; 2] = [a as u8, b as u8];
117+ let mut e1 = [0u8; 4];
118+ let mut e2 = [0u8; 4];
119+ print!("{:02x}{:02x} ", a, b);
120+ report("l", lower::encode(&src, &mut e1));
121+ print!(" ");
122+ report("u", upper::encode(&src, &mut e2));
123+ println!("");
124+ b += 1;
125+ }
126+ a += 1;
127+ }
128+
129+ // -- Domain C: every single byte, encode_str and HexDisplay.
130+ println!("C single-byte encode_str and HexDisplay, exhaustive");
131+ let mut c: u32 = 0;
132+ while c < 256 {
133+ let src: [u8; 1] = [c as u8];
134+ let mut e = [0u8; 2];
135+ match lower::encode_str(&src, &mut e) {
136+ Ok(s) => print!("{:02x} s={} ", c, s),
137+ Err(er) => print!("{:02x} s!{:?} ", c, er),
138+ }
139+ println!("x={:x} X={:X} d={}", HexDisplay(&src), HexDisplay(&src), HexDisplay(&src));
140+ c += 1;
141+ }
142+
143+ // -- Domain D: lengths 0..=128, both length functions and the buffer-size
144+ // boundary. Covers odd/even and the too-small-destination path.
145+ println!("D lengths, exhaustive to 128");
146+ let big = [b'a'; 128];
147+ let mut n: usize = 0;
148+ while n <= 128 {
149+ let src = &big[..n];
150+ match decoded_len(src) {
151+ Ok(v) => print!("{} dl={} el={}", n, v, encoded_len(src)),
152+ Err(e) => print!("{} dl!{:?} el={}", n, e, encoded_len(src)),
153+ }
154+ // Destination exactly one byte too small, to exercise the bound.
155+ let mut tight = [0u8; 64];
156+ let want = n / 2;
157+ if want > 0 && want <= 64 {
158+ let fit = &mut tight[..want - 1];
159+ print!(" ");
160+ report("t", mixed::decode(src, fit));
161+ }
162+ println!("");
163+ n += 1;
164+ }
165+
166+ // -- Domain E: pseudorandom inputs of varied length, from a generator
167+ // defined here so both sides produce the identical sequence.
168+ println!("E pseudorandom, 20000 cases");
169+ let mut state: u32 = 2463534242;
170+ let mut i: u32 = 0;
171+ while i < 20000 {
172+ // xorshift32, chosen because it is exactly representable in both
173+ // languages: u32 wrapping shifts and xor, nothing else.
174+ state ^= state << 13;
175+ state ^= state >> 17;
176+ state ^= state << 5;
177+ let len: usize = (state % 49) as usize;
178+
179+ let mut buf = [0u8; 48];
180+ let mut j: usize = 0;
181+ while j < len {
182+ state ^= state << 13;
183+ state ^= state >> 17;
184+ state ^= state << 5;
185+ // Mostly hex characters, sometimes not, so both the accepting and
186+ // the rejecting paths are exercised.
187+ let pick = state % 20;
188+ if pick < 16 {
189+ let d = (state >> 8) % 16;
190+ if d < 10 {
191+ buf[j] = 48 + d as u8;
192+ } else if (state >> 4) % 2 == 0 {
193+ buf[j] = 87 + d as u8;
194+ } else {
195+ buf[j] = 55 + d as u8;
196+ }
197+ } else {
198+ buf[j] = (state >> 16) as u8;
199+ }
200+ j += 1;
201+ }
202+ let src = &buf[..len];
203+
204+ let mut d1 = [0u8; 24];
205+ let mut d2 = [0u8; 24];
206+ let mut d3 = [0u8; 24];
207+ print!("{} {} ", i, len);
208+ report("l", lower::decode(src, &mut d1));
209+ print!(" ");
210+ report("u", upper::decode(src, &mut d2));
211+ print!(" ");
212+ report("m", mixed::decode(src, &mut d3));
213+
214+ // Round trip: encode the bytes, decode them back.
215+ let mut enc = [0u8; 96];
216+ report(" e", lower::encode(src, &mut enc));
217+ println!("");
218+ i += 1;
219+ }
220+
221+ println!("done");
222+}
modified src/lower.rs +71 -3
@@ -1398,6 +1398,27 @@ impl Lowerer {
13981398 }
13991399
14001400 let v = self.expr_at(&init.expr, ann.as_ref())?;
1401+
1402+ // `let s = &buf[..n]` binds a view of a place that is already in
1403+ // scope. Nim's borrow checker will not let a `let` borrow out of a
1404+ // local, and there is nothing to materialise anyway -- a view is a
1405+ // reference. Binding it as an alias substitutes the same expression at
1406+ // each use, which re-evaluates nothing because the initialiser is a
1407+ // place expression with no side effects.
1408+ if v.window.is_none()
1409+ && matches!(v.ty, Some(Nim::OpenArray(_)))
1410+ && is_pure_place(&init.expr)
1411+ {
1412+ let t = v.ty.clone().unwrap();
1413+ let elem = match &t {
1414+ Nim::OpenArray(e) => Some((**e).clone()),
1415+ _ => None,
1416+ };
1417+ self.bind_alias(&name, Alias::Value { code: v.code.clone(), ty: Some(t) });
1418+ let _ = elem;
1419+ return Ok(());
1420+ }
1421+
14011422 if let Some(w) = v.window.clone() {
14021423 // `let dst = dst.get_mut(..n).ok_or(..)?;` -- the binding names a
14031424 // view into the caller's buffer. Copying it into a `seq` would
@@ -1435,6 +1456,11 @@ impl Lowerer {
14351456 }
14361457 // Rust's immutable `let` is Nim's `let`; `let mut` is `var`. Shadowing
14371458 // works in both, so a re-`let` of the same name needs no rename.
1459+ //
1460+ // `let x = &mut y[..n]` is an immutable binding of a *mutable* borrow:
1461+ // Rust may write through it, and Nim only accepts a `var` where a
1462+ // `var` parameter is wanted, so the binding has to be one.
1463+ let mutable = mutable || is_mut_borrow(&init.expr);
14381464 let kw = if mutable { "var" } else { "let" };
14391465 let line = format!("{} {}: {} = {}", kw, ident(&name), t.render(), v.code);
14401466 self.line(&line);
@@ -2660,9 +2686,10 @@ impl Lowerer {
26602686 let code = match (&from, &to) {
26612687 (f, t) if f.is_integer() && t.is_integer() => {
26622688 // Rust's `as` between integers is a pure bit-width truncation
2663- // or sign-extension — never a range check. Nim's `T(x)` *does*
2664- // range-check and would raise where Rust wraps, so `cast` is
2665- // the only faithful spelling. Probed against both compilers.
2689+ // or sign-extension, never a range check. `cast` says exactly
2690+ // that. (Nim's `T(x)` turns out to truncate here as well --
2691+ // see DESIGN.md item 5 -- but `cast` is the spelling that
2692+ // means it rather than the one that happens to agree.)
26662693 format!("cast[{}]({})", t.render(), v.code)
26672694 }
26682695 (f, Nim::Prim(p)) if f.is_integer() && (p == "float64" || p == "float32") => {
@@ -3853,6 +3880,47 @@ fn fmt_proc(t: &str) -> &'static str {
38533880 }
38543881 }
38553882
3883+/// Whether an expression denotes a place -- a variable, a field, or an index
3884+/// or slice of one -- and so may be re-evaluated with no side effect.
3885+fn is_pure_place(e: &Expr) -> bool {
3886+ match e {
3887+ Expr::Path(_) => true,
3888+ Expr::Field(f) => is_pure_place(&f.base),
3889+ Expr::Index(i) => {
3890+ is_pure_place(&i.expr)
3891+ && match &*i.index {
3892+ Expr::Range(r) => {
3893+ r.start.as_deref().map_or(true, is_pure_place)
3894+ && r.end.as_deref().map_or(true, is_pure_place)
3895+ }
3896+ other => is_pure_place(other),
3897+ }
3898+ }
3899+ Expr::Lit(_) => true,
3900+ Expr::Reference(r) => is_pure_place(&r.expr),
3901+ Expr::Paren(p) => is_pure_place(&p.expr),
3902+ Expr::Group(g) => is_pure_place(&g.expr),
3903+ // Arithmetic on places is still side-effect free, so a bound like
3904+ // `..want - 1` does not stop the binding being an alias.
3905+ Expr::Binary(b) if !is_compound(&b.op) => {
3906+ is_pure_place(&b.left) && is_pure_place(&b.right)
3907+ }
3908+ Expr::Unary(u) => is_pure_place(&u.expr),
3909+ Expr::Cast(c) => is_pure_place(&c.expr),
3910+ _ => false,
3911+ }
3912+}
3913+
3914+/// Whether an expression is a `&mut` borrow, directly or through parens.
3915+fn is_mut_borrow(e: &Expr) -> bool {
3916+ match e {
3917+ Expr::Reference(r) => r.mutability.is_some(),
3918+ Expr::Paren(p) => is_mut_borrow(&p.expr),
3919+ Expr::Group(g) => is_mut_borrow(&g.expr),
3920+ _ => false,
3921+ }
3922+}
3923+
38563924 fn takes_self(sig: &syn::Signature) -> bool {
38573925 matches!(sig.inputs.first(), Some(FnArg::Receiver(_)))
38583926 }
@@ -1398,6 +1398,27 @@ impl Lowerer {
1398 }1398 }
1399 1399
1400 let v = self.expr_at(&init.expr, ann.as_ref())?;1400 let v = self.expr_at(&init.expr, ann.as_ref())?;
1401+
1402+ // `let s = &buf[..n]` binds a view of a place that is already in
1403+ // scope. Nim's borrow checker will not let a `let` borrow out of a
1404+ // local, and there is nothing to materialise anyway -- a view is a
1405+ // reference. Binding it as an alias substitutes the same expression at
1406+ // each use, which re-evaluates nothing because the initialiser is a
1407+ // place expression with no side effects.
1408+ if v.window.is_none()
1409+ && matches!(v.ty, Some(Nim::OpenArray(_)))
1410+ && is_pure_place(&init.expr)
1411+ {
1412+ let t = v.ty.clone().unwrap();
1413+ let elem = match &t {
1414+ Nim::OpenArray(e) => Some((**e).clone()),
1415+ _ => None,
1416+ };
1417+ self.bind_alias(&name, Alias::Value { code: v.code.clone(), ty: Some(t) });
1418+ let _ = elem;
1419+ return Ok(());
1420+ }
1421+
1401 if let Some(w) = v.window.clone() {1422 if let Some(w) = v.window.clone() {
1402 // `let dst = dst.get_mut(..n).ok_or(..)?;` -- the binding names a1423 // `let dst = dst.get_mut(..n).ok_or(..)?;` -- the binding names a
1403 // view into the caller's buffer. Copying it into a `seq` would1424 // view into the caller's buffer. Copying it into a `seq` would
@@ -1435,6 +1456,11 @@ impl Lowerer {
1435 }1456 }
1436 // Rust's immutable `let` is Nim's `let`; `let mut` is `var`. Shadowing1457 // Rust's immutable `let` is Nim's `let`; `let mut` is `var`. Shadowing
1437 // works in both, so a re-`let` of the same name needs no rename.1458 // works in both, so a re-`let` of the same name needs no rename.
1459+ //
1460+ // `let x = &mut y[..n]` is an immutable binding of a *mutable* borrow:
1461+ // Rust may write through it, and Nim only accepts a `var` where a
1462+ // `var` parameter is wanted, so the binding has to be one.
1463+ let mutable = mutable || is_mut_borrow(&init.expr);
1438 let kw = if mutable { "var" } else { "let" };1464 let kw = if mutable { "var" } else { "let" };
1439 let line = format!("{} {}: {} = {}", kw, ident(&name), t.render(), v.code);1465 let line = format!("{} {}: {} = {}", kw, ident(&name), t.render(), v.code);
1440 self.line(&line);1466 self.line(&line);
@@ -2660,9 +2686,10 @@ impl Lowerer {
2660 let code = match (&from, &to) {2686 let code = match (&from, &to) {
2661 (f, t) if f.is_integer() && t.is_integer() => {2687 (f, t) if f.is_integer() && t.is_integer() => {
2662 // Rust's `as` between integers is a pure bit-width truncation2688 // Rust's `as` between integers is a pure bit-width truncation
2663- // or sign-extension — never a range check. Nim's `T(x)` *does*2689+ // or sign-extension, never a range check. `cast` says exactly
2664- // range-check and would raise where Rust wraps, so `cast` is2690+ // that. (Nim's `T(x)` turns out to truncate here as well --
2665- // the only faithful spelling. Probed against both compilers.2691+ // see DESIGN.md item 5 -- but `cast` is the spelling that
2692+ // means it rather than the one that happens to agree.)
2666 format!("cast[{}]({})", t.render(), v.code)2693 format!("cast[{}]({})", t.render(), v.code)
2667 }2694 }
2668 (f, Nim::Prim(p)) if f.is_integer() && (p == "float64" || p == "float32") => {2695 (f, Nim::Prim(p)) if f.is_integer() && (p == "float64" || p == "float32") => {
@@ -3853,6 +3880,47 @@ fn fmt_proc(t: &str) -> &'static str {
3853 }3880 }
3854 }3881 }
3855 3882
3883+/// Whether an expression denotes a place -- a variable, a field, or an index
3884+/// or slice of one -- and so may be re-evaluated with no side effect.
3885+fn is_pure_place(e: &Expr) -> bool {
3886+ match e {
3887+ Expr::Path(_) => true,
3888+ Expr::Field(f) => is_pure_place(&f.base),
3889+ Expr::Index(i) => {
3890+ is_pure_place(&i.expr)
3891+ && match &*i.index {
3892+ Expr::Range(r) => {
3893+ r.start.as_deref().map_or(true, is_pure_place)
3894+ && r.end.as_deref().map_or(true, is_pure_place)
3895+ }
3896+ other => is_pure_place(other),
3897+ }
3898+ }
3899+ Expr::Lit(_) => true,
3900+ Expr::Reference(r) => is_pure_place(&r.expr),
3901+ Expr::Paren(p) => is_pure_place(&p.expr),
3902+ Expr::Group(g) => is_pure_place(&g.expr),
3903+ // Arithmetic on places is still side-effect free, so a bound like
3904+ // `..want - 1` does not stop the binding being an alias.
3905+ Expr::Binary(b) if !is_compound(&b.op) => {
3906+ is_pure_place(&b.left) && is_pure_place(&b.right)
3907+ }
3908+ Expr::Unary(u) => is_pure_place(&u.expr),
3909+ Expr::Cast(c) => is_pure_place(&c.expr),
3910+ _ => false,
3911+ }
3912+}
3913+
3914+/// Whether an expression is a `&mut` borrow, directly or through parens.
3915+fn is_mut_borrow(e: &Expr) -> bool {
3916+ match e {
3917+ Expr::Reference(r) => r.mutability.is_some(),
3918+ Expr::Paren(p) => is_mut_borrow(&p.expr),
3919+ Expr::Group(g) => is_mut_borrow(&g.expr),
3920+ _ => false,
3921+ }
3922+}
3923+
3856 fn takes_self(sig: &syn::Signature) -> bool {3924 fn takes_self(sig: &syn::Signature) -> bool {
3857 matches!(sig.inputs.first(), Some(FnArg::Receiver(_)))3925 matches!(sig.inputs.first(), Some(FnArg::Receiver(_)))
3858 }3926 }
added tests/proof.rs +177 -0
new file mode 100644
@@ -0,0 +1,177 @@
1+//! The exhaustive differential check described in `PROOF.md`.
2+//!
3+//! This is separate from `tests/differential.rs` because it is a different
4+//! kind of claim. That runner asks whether a handful of hand-written cases
5+//! agree; this one enumerates *entire input domains* — every two-byte input
6+//! to the decoder, every two-byte input to the encoder, every single byte
7+//! through `encode_str` and `HexDisplay` — and compares the complete output
8+//! of both programs byte for byte.
9+//!
10+//! The driver in `proof/main.rs` references base16ct's own module files in
11+//! place, so this cannot drift from what `tests/cases/026-base16ct-crate/`
12+//! transpiles.
13+
14+use std::fs;
15+use std::io::Write as _;
16+use std::path::{Path, PathBuf};
17+use std::process::{Command, Stdio};
18+
19+const RUSTNIM: &str = env!("CARGO_BIN_EXE_rustnim");
20+
21+fn find_nim() -> PathBuf {
22+ if let Ok(p) = std::env::var("RUSTNIM_NIM") {
23+ return PathBuf::from(p);
24+ }
25+ let mut dir: Option<&Path> = Some(Path::new(env!("CARGO_MANIFEST_DIR")));
26+ while let Some(d) = dir {
27+ let c = d.join(".nim-toolchain/bin/nim");
28+ if c.is_file() {
29+ return c;
30+ }
31+ dir = d.parent();
32+ }
33+ panic!("no .nim-toolchain/bin/nim found; set RUSTNIM_NIM");
34+}
35+
36+fn sh(cmd: &mut Command, what: &str) -> Vec<u8> {
37+ let out = cmd
38+ .stdout(Stdio::piped())
39+ .stderr(Stdio::piped())
40+ .output()
41+ .unwrap_or_else(|e| panic!("{what}: spawn: {e}"));
42+ if !out.status.success() {
43+ let mut msg = String::from_utf8_lossy(&out.stderr).into_owned();
44+ if msg.trim().is_empty() {
45+ msg = String::from_utf8_lossy(&out.stdout).into_owned();
46+ }
47+ panic!("{what} failed ({:?}):\n{}", out.status.code(), tail(&msg));
48+ }
49+ out.stdout
50+}
51+
52+fn tail(s: &str) -> String {
53+ let v: Vec<&str> = s.trim_end().lines().collect();
54+ v[v.len().saturating_sub(25)..].join("\n")
55+}
56+
57+/// Report the first differing line, and how many lines differ in total.
58+fn first_difference(a: &[u8], b: &[u8]) -> String {
59+ let (sa, sb) = (String::from_utf8_lossy(a), String::from_utf8_lossy(b));
60+ let (la, lb): (Vec<_>, Vec<_>) = (sa.lines().collect(), sb.lines().collect());
61+ let mut first = None;
62+ let mut count = 0usize;
63+ for i in 0..la.len().max(lb.len()) {
64+ if la.get(i) != lb.get(i) {
65+ count += 1;
66+ if first.is_none() {
67+ first = Some(i);
68+ }
69+ }
70+ }
71+ match first {
72+ None => format!("{} vs {} bytes, but every line matches", a.len(), b.len()),
73+ Some(i) => format!(
74+ "{count} line(s) differ; first at line {}:\n rustc: {:?}\n nim : {:?}",
75+ i + 1,
76+ la.get(i),
77+ lb.get(i)
78+ ),
79+ }
80+}
81+
82+#[test]
83+fn base16ct_is_byte_identical_over_the_enumerated_domains() {
84+ let root = Path::new(env!("CARGO_MANIFEST_DIR"));
85+ let work = root.join("tests/.work/proof");
86+ let _ = fs::remove_dir_all(&work);
87+ fs::create_dir_all(&work).unwrap();
88+
89+ let driver = root.join("proof/main.rs");
90+ let crate_dir = root.join("tests/cases/026-base16ct-crate");
91+ let mut modules: Vec<PathBuf> = fs::read_dir(&crate_dir)
92+ .unwrap()
93+ .filter_map(|e| e.ok().map(|e| e.path()))
94+ .filter(|p| {
95+ p.extension().is_some_and(|x| x == "rs")
96+ && p.file_name().is_some_and(|f| f != "main.rs")
97+ })
98+ .collect();
99+ modules.sort();
100+ assert!(
101+ modules.len() == 5,
102+ "expected base16ct's five module files, found {:?}",
103+ modules
104+ );
105+
106+ // -- rustc: the oracle.
107+ let rs_bin = work.join("rs");
108+ sh(
109+ Command::new("rustc")
110+ .arg("--edition=2021")
111+ .arg("--cfg")
112+ .arg("feature=\"alloc\"")
113+ .arg("-A")
114+ .arg("warnings")
115+ .arg(&driver)
116+ .arg("-o")
117+ .arg(&rs_bin)
118+ .env("TMPDIR", &work),
119+ "rustc",
120+ );
121+ let expected = sh(&mut Command::new(&rs_bin).env("TMPDIR", &work), "the Rust binary");
122+
123+ // -- rustnim, then Nim.
124+ let nim_src = work.join("proof.nim");
125+ let mut t = Command::new(RUSTNIM);
126+ t.arg(&driver);
127+ for m in &modules {
128+ t.arg(m);
129+ }
130+ t.arg("--cfg")
131+ .arg("feature=alloc")
132+ .arg("-o")
133+ .arg(&nim_src)
134+ .env("TMPDIR", &work);
135+ sh(&mut t, "rustnim");
136+
137+ let meta = fs::metadata(&nim_src).expect("rustnim wrote no output file");
138+ assert!(meta.len() > 0, "rustnim wrote an empty output file");
139+
140+ let nim_bin = work.join("nim");
141+ sh(
142+ Command::new(find_nim())
143+ .arg("c")
144+ .arg("--hints:off")
145+ .arg("--warnings:off")
146+ .arg("--colors:off")
147+ .arg(format!("--nimcache:{}", work.join("cache").display()))
148+ .arg(format!("-o:{}", nim_bin.display()))
149+ .arg(&nim_src)
150+ .env("TMPDIR", &work),
151+ "nim c",
152+ );
153+ let actual = sh(&mut Command::new(&nim_bin).env("TMPDIR", &work), "the Nim binary");
154+
155+ // The output must be substantial: an empty or truncated run agreeing with
156+ // an empty or truncated run would otherwise read as success, which is the
157+ // exact failure this project exists to avoid.
158+ let lines = expected.iter().filter(|b| **b == b'\n').count();
159+ assert!(
160+ lines > 150_000 && expected.ends_with(b"done\n"),
161+ "the oracle did not run to completion: {lines} lines, {} bytes",
162+ expected.len()
163+ );
164+
165+ assert!(
166+ expected == actual,
167+ "outputs differ.\n{}",
168+ first_difference(&expected, &actual)
169+ );
170+
171+ let _ = writeln!(
172+ std::io::stderr(),
173+ "proof: {} cases, {} bytes of output, byte-identical",
174+ lines,
175+ expected.len()
176+ );
177+}
new file mode 100644
@@ -0,0 +1,177 @@
1+//! The exhaustive differential check described in `PROOF.md`.
2+//!
3+//! This is separate from `tests/differential.rs` because it is a different
4+//! kind of claim. That runner asks whether a handful of hand-written cases
5+//! agree; this one enumerates *entire input domains* — every two-byte input
6+//! to the decoder, every two-byte input to the encoder, every single byte
7+//! through `encode_str` and `HexDisplay` — and compares the complete output
8+//! of both programs byte for byte.
9+//!
10+//! The driver in `proof/main.rs` references base16ct's own module files in
11+//! place, so this cannot drift from what `tests/cases/026-base16ct-crate/`
12+//! transpiles.
13+
14+use std::fs;
15+use std::io::Write as _;
16+use std::path::{Path, PathBuf};
17+use std::process::{Command, Stdio};
18+
19+const RUSTNIM: &str = env!("CARGO_BIN_EXE_rustnim");
20+
21+fn find_nim() -> PathBuf {
22+ if let Ok(p) = std::env::var("RUSTNIM_NIM") {
23+ return PathBuf::from(p);
24+ }
25+ let mut dir: Option<&Path> = Some(Path::new(env!("CARGO_MANIFEST_DIR")));
26+ while let Some(d) = dir {
27+ let c = d.join(".nim-toolchain/bin/nim");
28+ if c.is_file() {
29+ return c;
30+ }
31+ dir = d.parent();
32+ }
33+ panic!("no .nim-toolchain/bin/nim found; set RUSTNIM_NIM");
34+}
35+
36+fn sh(cmd: &mut Command, what: &str) -> Vec<u8> {
37+ let out = cmd
38+ .stdout(Stdio::piped())
39+ .stderr(Stdio::piped())
40+ .output()
41+ .unwrap_or_else(|e| panic!("{what}: spawn: {e}"));
42+ if !out.status.success() {
43+ let mut msg = String::from_utf8_lossy(&out.stderr).into_owned();
44+ if msg.trim().is_empty() {
45+ msg = String::from_utf8_lossy(&out.stdout).into_owned();
46+ }
47+ panic!("{what} failed ({:?}):\n{}", out.status.code(), tail(&msg));
48+ }
49+ out.stdout
50+}
51+
52+fn tail(s: &str) -> String {
53+ let v: Vec<&str> = s.trim_end().lines().collect();
54+ v[v.len().saturating_sub(25)..].join("\n")
55+}
56+
57+/// Report the first differing line, and how many lines differ in total.
58+fn first_difference(a: &[u8], b: &[u8]) -> String {
59+ let (sa, sb) = (String::from_utf8_lossy(a), String::from_utf8_lossy(b));
60+ let (la, lb): (Vec<_>, Vec<_>) = (sa.lines().collect(), sb.lines().collect());
61+ let mut first = None;
62+ let mut count = 0usize;
63+ for i in 0..la.len().max(lb.len()) {
64+ if la.get(i) != lb.get(i) {
65+ count += 1;
66+ if first.is_none() {
67+ first = Some(i);
68+ }
69+ }
70+ }
71+ match first {
72+ None => format!("{} vs {} bytes, but every line matches", a.len(), b.len()),
73+ Some(i) => format!(
74+ "{count} line(s) differ; first at line {}:\n rustc: {:?}\n nim : {:?}",
75+ i + 1,
76+ la.get(i),
77+ lb.get(i)
78+ ),
79+ }
80+}
81+
82+#[test]
83+fn base16ct_is_byte_identical_over_the_enumerated_domains() {
84+ let root = Path::new(env!("CARGO_MANIFEST_DIR"));
85+ let work = root.join("tests/.work/proof");
86+ let _ = fs::remove_dir_all(&work);
87+ fs::create_dir_all(&work).unwrap();
88+
89+ let driver = root.join("proof/main.rs");
90+ let crate_dir = root.join("tests/cases/026-base16ct-crate");
91+ let mut modules: Vec<PathBuf> = fs::read_dir(&crate_dir)
92+ .unwrap()
93+ .filter_map(|e| e.ok().map(|e| e.path()))
94+ .filter(|p| {
95+ p.extension().is_some_and(|x| x == "rs")
96+ && p.file_name().is_some_and(|f| f != "main.rs")
97+ })
98+ .collect();
99+ modules.sort();
100+ assert!(
101+ modules.len() == 5,
102+ "expected base16ct's five module files, found {:?}",
103+ modules
104+ );
105+
106+ // -- rustc: the oracle.
107+ let rs_bin = work.join("rs");
108+ sh(
109+ Command::new("rustc")
110+ .arg("--edition=2021")
111+ .arg("--cfg")
112+ .arg("feature=\"alloc\"")
113+ .arg("-A")
114+ .arg("warnings")
115+ .arg(&driver)
116+ .arg("-o")
117+ .arg(&rs_bin)
118+ .env("TMPDIR", &work),
119+ "rustc",
120+ );
121+ let expected = sh(&mut Command::new(&rs_bin).env("TMPDIR", &work), "the Rust binary");
122+
123+ // -- rustnim, then Nim.
124+ let nim_src = work.join("proof.nim");
125+ let mut t = Command::new(RUSTNIM);
126+ t.arg(&driver);
127+ for m in &modules {
128+ t.arg(m);
129+ }
130+ t.arg("--cfg")
131+ .arg("feature=alloc")
132+ .arg("-o")
133+ .arg(&nim_src)
134+ .env("TMPDIR", &work);
135+ sh(&mut t, "rustnim");
136+
137+ let meta = fs::metadata(&nim_src).expect("rustnim wrote no output file");
138+ assert!(meta.len() > 0, "rustnim wrote an empty output file");
139+
140+ let nim_bin = work.join("nim");
141+ sh(
142+ Command::new(find_nim())
143+ .arg("c")
144+ .arg("--hints:off")
145+ .arg("--warnings:off")
146+ .arg("--colors:off")
147+ .arg(format!("--nimcache:{}", work.join("cache").display()))
148+ .arg(format!("-o:{}", nim_bin.display()))
149+ .arg(&nim_src)
150+ .env("TMPDIR", &work),
151+ "nim c",
152+ );
153+ let actual = sh(&mut Command::new(&nim_bin).env("TMPDIR", &work), "the Nim binary");
154+
155+ // The output must be substantial: an empty or truncated run agreeing with
156+ // an empty or truncated run would otherwise read as success, which is the
157+ // exact failure this project exists to avoid.
158+ let lines = expected.iter().filter(|b| **b == b'\n').count();
159+ assert!(
160+ lines > 150_000 && expected.ends_with(b"done\n"),
161+ "the oracle did not run to completion: {lines} lines, {} bytes",
162+ expected.len()
163+ );
164+
165+ assert!(
166+ expected == actual,
167+ "outputs differ.\n{}",
168+ first_difference(&expected, &actual)
169+ );
170+
171+ let _ = writeln!(
172+ std::io::stderr(),
173+ "proof: {} cases, {} bytes of output, byte-identical",
174+ lines,
175+ expected.len()
176+ );
177+}