Is the transpiled base16ct byte-identical?

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153

# Is the transpiled `base16ct` byte-identical?

Short answer: **yes for every input in the domains enumerated below, and that
is a complete enumeration for the decoder's and encoder's per-chunk
behaviour.** For unbounded-length inputs it is a compositional argument plus
sampling, not a proof. This document says exactly which is which, because the
difference matters and because a transpiler that overstates its evidence is
the thing this project exists to be the opposite of.

Reproduce with `cargo test --test proof`. It takes about four seconds.

## What is being compared

`proof/main.rs` is a crate root that references base16ct 1.0.0's own module
files in place — `error.rs`, `lower.rs`, `upper.rs`, `mixed.rs`, `display.rs`,
each byte-for-byte as published on crates.io — and carries `lib.rs`'s
`decoded_len`, `encoded_len` and `decode_inner` verbatim. It enumerates input
domains and prints one line per case.

That same file is built twice:

```
rustc  proof/main.rs                        -> binary A
rustnim proof/main.rs <modules> | nim c     -> binary B
```

and `A`'s stdout is compared with `B`'s stdout using `==` on the raw bytes.
Current result: **151,463 cases, 9,100,470 bytes, identical**.

The output encodes everything observable about each call: the status
(`Ok`/`Err`), the error variant, the returned length, and the returned bytes
in hex. A difference in any of those is a difference in those bytes.

## The domains

| | domain | size | complete? |
|---|---|---|---|
| A | every two-byte input, through `lower`, `upper` and `mixed` decode | 65,536 | **exhaustive** |
| B | every two-byte input, through `lower` and `upper` encode | 65,536 | **exhaustive** |
| C | every single byte, through `encode_str` and `HexDisplay` (`{}`, `{:x}`, `{:X}`) | 256 | **exhaustive** |
| D | every length 0..=128, both length functions, and a destination one byte too small | 129 | **exhaustive** |
| E | pseudorandom inputs, lengths 0..48, mixed valid and invalid characters, decode by all three and round-trip encode | 20,000 | sampled |

Domain E's generator is an xorshift32 written in the driver itself, so both
binaries produce the identical sequence. It is not a source of randomness
between runs; it is a fixed, reproducible list.

## Why A is the interesting one

`decode_inner` is a map over independent two-byte chunks:

```rust
for (src, dst) in src.chunks_exact(2).zip(dst.iter_mut()) {
    let byte = (decode_nibble(src[0]) << 4) | decode_nibble(src[1]);
    err |= byte >> 8;
    *dst = byte as u8;
}
match err { 0 => Ok(dst), _ => Err(Error::InvalidEncoding) }
```

Chunk *i* reads `src[2i]` and `src[2i+1]`, writes `dst[i]`, and contributes to
`err` by `|=`. Nothing else crosses between iterations. So the whole function
is determined by two things:

1. the per-chunk function `(u8, u8) -> (u8, u16)` — output byte and error
   contribution; and
2. the iteration count, `⌊|src| / 2⌋`, and the `|=` accumulation.

**Domain A settles (1) completely.** All 65,536 possible chunks are tried, and
every one produces identical output. There is no untried input to that
function. This is the part that carries base16ct's constant-time arithmetic —
the `i16` wrapping and the arithmetic shift — and it is not sampled at all.

**Domain D settles the iteration count** for every length up to 128, including
the odd-length rejection and the too-small-destination rejection.

(2) also requires that both implementations accumulate `err` the same way.
That is visible in the emitted Nim, and it is what the following lines say:

```nim
var err: uint16 = 0'u16
for rsTmpIdx4 in 0 ..< int(min((src.len div int(2'i32)), rsTmpLen3)):
  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)]))
  err = err or (byte shr 8'u16)
  dst[rsTmpOff2 + rsTmpIdx4] = cast[uint8](byte)
```

(That is the emitted text verbatim, redundant parentheses and all.)

Same bounds, same indices, same accumulation. **This step is an inspection,
not a proof**, and it is the one link in the chain that is not mechanically
checked. Domain E exists to attack it: 20,000 inputs of varying length, half
of them invalid, exercising the accumulation across many chunks. If the
iteration or accumulation differed, those would diverge.

So the honest statement is:

> Given the emitted loop iterates `⌊|src|/2⌋` chunks and accumulates `err` by
> `|=` — which was read, and which 20,000 multi-chunk cases are consistent
> with — the exhaustive agreement on all 65,536 single chunks extends by
> induction to inputs of every length.

## Encoding

Encoding is per byte and independent, so domain B is the complete domain of an
encode step, and domain C is the complete domain of `encode_nibble` as reached
through `encode_str`. The same induction applies, with no accumulator to worry
about.

## Does the check actually discriminate?

A comparison that cannot fail proves nothing, so the proof was tested by
breaking the transpiler. Mapping Rust's `>>` to a **logical** shift instead of
an arithmetic one — precisely the error a model without integer width and
signedness makes, and the one described in `findings/` — produces:

```
86274 line(s) differ; first at line 12338:
  rustc: "3030 l=00/1 u=00/1 m=00/1"
  nim  : "3030 l!InvalidEncoding u!InvalidEncoding m!InvalidEncoding"
```

Input `3030` is ASCII `"00"`. The real decoder returns the byte `0x00`; the
sabotaged one rejects it. The harness names the first failing input rather
than reporting a count.

The proof test also fails if the oracle produces fewer than 150,000 lines or
does not end in `done`, so a truncated run agreeing with a truncated run
cannot pass.

## What this does not establish

- **Not a proof of program equivalence.** It is exhaustive over stated finite
  domains and a structural argument beyond them. It says nothing about inputs
  outside those domains except through that argument.
- **Only these functions.** base16ct's public surface is covered; rustnim in
  general is not. The 33 differential cases in `tests/cases/` are separate,
  smaller evidence about the rest of the lowering.
- **One platform, one pair of compilers.** rustc 1.98.1 and Nim 2.2.4 on
  x86-64 Linux. Both were also *probed* for the specific behaviours the
  lowering relies on, rather than assumed from documentation — see the
  "Settled empirically" section of `DESIGN.md`.
- **Stdout only.** Timing is not compared, so nothing here supports base16ct's
  constant-time claim surviving the translation. The arithmetic is
  branch-free in both, but that is an observation about the source, not a
  measurement.

## Trusted base

rustc as the oracle; Nim's compiler; the driver in `proof/main.rs` being a
faithful enumeration; and `tests/proof.rs` comparing what it says it compares.
The first two are the same trust any differential test places in its
compilers. The last two are 300 lines you can read.