# 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.