feat(formal): extend source-linked authorization assurance

[bordumb]

Selected authorization-to-execution guarantees stopped at independent models or assumed caller inputs. This branch connects additional shipping Rust functions to exact Lean specifications, so acceptance earns the stated validity, field binding, admission bounds and refusal behavior.

Shipping code consumes proved identifier/scope constructors, status and temporal checks, request/counter/connection preimages, reservation admission, cumulative-record validation and connection-entry membership. The complete connection validator now earns bounded nonempty allowlists, global native String/profile ordering, text validity, duplicate absence and temporal shape with exact error precedence. Its standard-library interface assumptions remain explicit.

The decoder batches prove exact construction, cursor/head/integer/null behavior, all 256 first-byte classifications, payload/UTF-8 reading, collection heads, protocol fields and the completion guard. Thirty-one additional source-composed cases cover huge lengths, truncation, malformed UTF-8, indefinite collection rejection, size/nonempty rules and exact 32-byte digests. Regression cases distinguish type peeking from successful parsing, input length from input identity, and header refusal from narrowing refusal after consumption. The harness inventory also excludes explicit-path test modules without counting their helpers as shipping targets.

AP-SPEC-069 remains in progress. Full protocol-object codecs, verifier/caller composition, backend histories and cryptographic integration remain open in the implementation ledger; this PR does not claim end-to-end completion.

Validation of the latest checkpoint:

• 917 compiled/audited statements; all 902 previous complete declaration records unchanged; no new axioms.
• Full Lean build, 18/18 qualification cases and two byte-identical clean Rust-to-Lean replays.
• 25 reviewed models, none unreviewed, zero compiled external axioms. Two transparent String methods extend an existing reviewed model interface.
• Frozen parity over 43,200 complete records; 43 connection and 232 active gateway tests pass, with 26 existing ignored gateway tests unchanged.
• All 173 xtask tests, affected-target linting, native refinement vectors, historical coverage reproduction and the 48-harness shipping-call inventory pass. Kani solver execution was skipped; no new solver result is claimed.
• Primary decision scope remains 134/1047 functions, 1833/11563 code lines and 23/82 check sites; codec roles are excluded from that headline. Exact staged Gitleaks v8.28.0 scan passes.

Source closure: 182ce049a050aeef56cb3ac53dad37a08f5ef9b35d1fbf27816471bd22ca3ac0.

See docs/assurance/AP_SPEC_069_STATUS.md and specification §§13.36–13.41. Hosted checks on the pushed revision remain required; coding continues without waiting for CI.