`FStar.Bytes` is inconsistent: `repr_bytes` / `repr_bytes_size` prove `False`

## Summary

`FStar.Bytes` ships two mutually contradictory axioms. Any program that
opens `FStar.Bytes` can prove `False` — and hence anything at all — in one
line, with no `assume`, no `admit`, no tactic, no `--ext` flag and no
option changes. The resulting module verifies *and* extracts.

Because the offending lemma carries an `SMTPat`, no explicit lemma call is
even required: merely mentioning `fits_in_k_bytes 0 0` in a proof context
is enough. Ordinary `FStar.Bytes` clients can therefore hit this by
accident.

`FStar.Bytes` is an interface-only module: there is no `ulib/FStar.Bytes.fst`
and no OCaml realization under `ulib/ml/`. Every `val` in it is an unproven
axiom that F* trusts unconditionally.

## Repro

```fstar
module BytesReprBytes
module B = FStar.Bytes
let bad () : Lemma False = B.repr_bytes_size 0 0
```

```
$ fstar.exe BytesReprBytes.fst
Verified module: BytesReprBytes
All verification conditions discharged successfully
```

Everything follows:

```fstar
let one_is_two () : Lemma (1 == 2) = bad ()
let anything (a: Type) : Tot a = bad (); false_elim ()
let boom : int = anything int
```

This also extracts cleanly:

```
$ fstar.exe --codegen OCaml --odir out BytesReprBytes.fst
$ cat out/BytesReprBytes.ml
open Prims
let anything (uu___ : unit) : 'a= FStar_Pervasives.false_elim ()
let boom : Prims.int= anything ()
```

### No lemma call needed (`SMTPat`)

```fstar
module BytesReprBytesAuto
module B = FStar.Bytes
let bad () : Lemma False = assert (B.fits_in_k_bytes 0 0)
```

Also verifies.

## Root cause

`ulib/FStar.Bytes.fsti`:

```fstar
let fits_in_k_bytes (n:nat) (k:nat) = FStar.UInt.size n (8 * k)
type uint_k (k:nat) = n:nat{fits_in_k_bytes n k}

(** repr_bytes n: The number of bytes needed to represent a nat **)
val repr_bytes:
n:nat
-> k:pos{fits_in_k_bytes n k} // <-- result is a `pos`, i.e. >= 1

val repr_bytes_size:
k:nat // <-- `nat`, so `k = 0` is allowed
-> n:uint_k k
-> Lemma (ensures (repr_bytes n <= k))
[SMTPat (fits_in_k_bytes n k)]
```

- `repr_bytes`'s declared result type is `k:pos{...}`, so
`repr_bytes 0 >= 1`.
- `uint_k 0 = n:nat{FStar.UInt.size n 0} = n:nat{0 <= n /\ n < pow2 0}`,
which is inhabited exactly by `0`. So `repr_bytes_size 0 0` is a
well-typed application, and it yields `repr_bytes 0 <= 0`.

`1 <= repr_bytes 0 <= 0` is `False`.

The `k` argument of `repr_bytes_size` is the only place where `0` slips
through: the intended reading is "if `n` fits in `k` bytes then `k` bytes
are enough", but `k = 0` bytes trivially "fit" `n = 0` under
`UInt.size n 0`, while `repr_bytes` is specified never to return `0`.

## The interface is only well-typed because of the inconsistency

```fstar
val bytes_of_int:
k:nat
-> n:nat{repr_bytes n <= k /\ k < pow2 32}
-> lbytes k

val bytes_of_int_of_bytes:
b:bytes{length b <= 32}
-> Lemma (ensures (bytes_of_int (length b) (int_of_bytes b) == b))
[SMTPat (int_of_bytes b)]
```

Instantiating `bytes_of_int_of_bytes` at `empty_bytes` (`length = 0`)
mentions `bytes_of_int 0 (int_of_bytes empty_bytes)`. Since
`int_of_bytes empty_bytes : uint_k 0` is necessarily `0`, that application
requires `repr_bytes 0 <= 0` — precisely the false fact above. F* accepts
it, discharging the obligation with the `repr_bytes_size` `SMTPat`. So
`FStar.Bytes`'s own `ensures` clause is well-typed only *because* the
axiom set is inconsistent:

```fstar
module BytesIllTyped
module B = FStar.Bytes
let derived ()
: Lemma (B.bytes_of_int 0 (B.int_of_bytes B.empty_bytes) == B.empty_bytes) =
B.bytes_of_int_of_bytes B.empty_bytes
```

verifies.

## Suggested fixes

Any one of these removes the contradiction; the first is the smallest and
matches the intended meaning:

1. Strengthen `repr_bytes_size`'s first argument to `k:pos`.
2. Weaken `repr_bytes`'s result type from `k:pos{...}` to `k:nat{...}`, and
change `lemma_repr_bytes_values` so that `repr_bytes 0 == 0`. (This
changes the meaning of `repr_bytes 0` and will affect clients.)
3. Require `n:pos` in `repr_bytes_size`.
4. More broadly: `FStar.Bytes` is a sizeable axiom set with no
implementation and no realization, so nothing checks it for consistency.
Consider giving it a model (even a `Seq byte`-based one behind the
interface) so that these `val`s are discharged rather than trusted, or
at minimum adding a consistency smoke test.

## Prior art checked

Searched the FStarLang/FStar tracker (open and closed) for `repr_bytes`,
`repr_bytes_size`, `FStar.Bytes inconsistent`, and `Bytes unsound`. The
only `repr_bytes` hit is #86 (extraction of `Prims.int`), which is
unrelated. #2072 ("A soundness issue?") is about zero-size vectors in
HACL*'s Merkle trees, also unrelated. No issue reports this.

## Environment

- F* v2026.08.23, commit `f3dd580cd58cdc5ccc0a64e4697c8cdad5a9e208`
(latest release at time of writing).
- `ulib/FStar.Bytes.fsti` is byte-identical between that release and
current `FStarLang/FStar` `master`; the file has not been touched by any
recent change to this area.
- No flags, no `#set-options`, no `#push-options`, no tactics.

Start with ulib/FStar.Bytes.fsti and reproduce the contradiction using the BytesReprBytes example from the issue. Inspect the repr_bytes and repr_bytes_size refinements, then evaluate the suggested smallest fix of requiring a positive byte count. Done means the reproducer no longer verifies False and a regression check covers the zero-byte case.

Written by the indexing model from the issue text.