base64-ng 1.0.7

no_std-first Base64 encoding and decoding with strict APIs and a security-heavy release process
Documentation 
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

# Kani Verification Policy

`base64-ng` keeps Kani proof harnesses in the crate. Kani execution depends on
the compiler bundled with the installed `cargo-kani` release, so the supported
pairing is documented rather than assumed.

## Current Status

- Local Rust toolchain: Rust `1.90.0`.
- Locally tested Kani: `cargo-kani 0.67.0`.
- Current result: `scripts/check_kani.sh` verifies the full current
  no-default-features Kani harness set: 17 harnesses, 0 failures.

This is not a normal Cargo dependency-resolution issue. Kani runs are compiler-integration-sensitive because Kani is a verifier with its own compiler integration.
Updating the project to Rust `1.90` does not make an older Kani release
understand that toolchain automatically.

## How To Check

Run:

```sh
cargo kani --version
scripts/check_kani.sh
```

If the installed Kani compiler is compatible, `scripts/check_kani.sh` runs:

```sh
cargo kani --no-default-features
```

The source-level harness unwind bound is intentionally set to `70` because the
constant-time-oriented alphabet scanner runs a fixed 64-iteration loop. Kani's
global `--unwind` flag only applies to filtered single-harness runs, so the full
suite carries the bound on the harness attributes.

If Kani reports that its compiler requires an older Rust version than this
crate declares, the script prints a skip and exits successfully. The stable
release gate treats that as an explicit policy skip, not as completed formal
verification.

## Harness Scope

Current harnesses cover:

- scalar `decode_chunk` output bounds and bit-packing agreement with decoded
  6-bit values
- unpadded scalar tail validation and decode output bounds
- scalar length-helper bounds
- bounded scalar encode/decode output-prefix bounds
- in-place decode prefix bounds
- clear-tail cleanup behavior on decode failures
- constant-time-oriented validate/decode agreement for one quantum

## Historical v1.0.0 Verifier Exception

The initial `1.0.0` outcome accepted a documented verifier exception:

- keep all Kani harnesses in-tree and checked by `scripts/check_kani.sh`
- treat an incompatible Kani compiler as an explicit skip, not a proof
- require replacement evidence before release-sensitive changes are accepted
- do not claim Kani-complete or formally verified behavior in the `1.0.0`
  security contract

Replacement evidence for `v1.0` consists of:

- the full `scripts/checks.sh` gate
- Miri evidence from `scripts/check_miri.sh`
- bounded fuzz smoke evidence from
  `BASE64_NG_RUN_FUZZ_SMOKE=1 scripts/check_fuzz.sh`
- deterministic tests for scalar chunk packing, in-place decode, clear-tail
  cleanup, stream fail-closed behavior, profile behavior, and constant-time
  validate/decode agreement
- generated assembly evidence from `scripts/generate_ct_asm_evidence.sh`
- invariant documentation in [INVARIANTS.md](INVARIANTS.md)
- panic-policy enforcement through `scripts/validate-panic-policy.sh`
- release metadata, MSRV/toolchain, dependency, unsafe-boundary,
  constant-time-policy, and SIMD-admission validators

That exception was intentionally narrower than a formal proof. Current `1.0.x`
evidence now includes the bounded Kani harness set.
The stable `1.0.0` guarantee is the documented API and security contract backed
by release evidence, not a whole-crate or cryptographic formal-verification
claim.

## Future Verifier Admission

Other verifier or model-checking tools may be evaluated, but they are not
release-gate evidence until they have:

- a documented local install and CI path
- reproducible commands that work with the pinned Rust toolchain
- a scoped harness plan for scalar Base64 bit-packing and buffer bounds
- no runtime dependency impact on the published crate
- clear failure behavior in release scripts

Do not lower `rust-version` only to make Kani run unless the whole crate still
passes the release gate and the MSRV change is intentional. The verifier should
follow the crate's supported Rust version, not the other way around.

## Release Policy

For each future release, the project must choose one of these outcomes:

- run Kani proofs with a compatible Kani release
- pin a documented compatible Kani workflow
- document a verifier exception and the replacement evidence required before
  release

Replacement evidence may include Miri, deterministic exhaustive tests,
fuzz-corpus evidence, generated-code review, panic-policy validation, and local
invariant documentation, but it must be named explicitly.
A Kani skip is not the same as a proof.

## Upgrade Guidance

When a newer Kani release is available:

```sh
cargo install --locked kani-verifier
cargo kani setup
cargo kani --version
scripts/check_kani.sh
```

For future releases, revisit this document whenever the installed Kani release,
the pinned Rust toolchain, or the harness unwind policy changes.