Testing bench — credit_spend

The credit-spend decider: may this spend proceed? Never in arrears, never beyond the balance, and never beyond the remaining refund-window velocity allowance — so the worst-case fraud loss inside the window is a known number by construction, not a convention. The judgement is the proven Credit_Grant_Pkg.May_Spend; this front is its forged argv shell. Nothing in the portal consumes it yet — that gap is stated on its note, not papered over.

Binary: wired (named by CREDIT_SPEND_DECIDER; the path comes only from the server's environment, never from this page)

Theorems the proven core carries

Run it yourself

Space-separated tokens, at most 8, each at most 32 characters of [A-Za-z0-9_]. Malformed tokens are allowed through on purpose: the front's own refusal of them — exit status 3 — is part of what this bench exists to show you.

The truth table — worked examples, re-runnable

These are the rows the forge's harness graded before this artifact was admitted. Running them here re-executes each one against the wired binary, live, and grades the match in front of you.

The inspector's note

Example	argv	expected stdout	expected exit
balance covers it, window open — spend proceeds	1000 false 200 500 0	true	0
NO-SPEND-IN-ARREARS — an account in arrears spends nothing	1000 true 200 500 0	false	0
NO-OVERDRAW — amount beyond balance refuses	100 false 200 500 0	false	0
zero balance spends nothing — balance must be positive	0 false 0 500 0	false	0
VELOCITY-BOUNDS-LOSS — 400 exceeds the remaining 300 of the window	1000 false 400 500 200	false	0
velocity edge — exactly the remaining allowance is permitted	1000 false 300 500 200	true	0
EXHAUSTED-WINDOW-SPENDS-NOTHING — one penny past a spent window refuses	1000 false 1 500 500	false	0
honest edge: a ZERO spend is permitted even with an exhausted window (0 <= 0, by construction)	1000 false 0 500 500	true	0
EXHAUSTED-IS-ZERO — drawn past the cap leaves nothing, refuses	1000 false 1 500 600	false	0
malformed number — the front itself refuses (exit 3)	banana false 200 500 0	(no output)	3
wrong arity — the front itself refuses (exit 3)	1000 false 200	(no output)	3

Authored by the seat, 2026-08-13 — grades from evidence, narrated not invented.

Proof inventory — proven

Credit_Grant_Pkg.May_Spend and Remaining_Velocity carry defining-equation Posts plus the named theorems — NO-SPEND-IN-ARREARS, NO-OVERDRAW, VELOCITY-BOUNDS-LOSS, EXHAUSTED-WINDOW-SPENDS-NOTHING, NEVER-EXCEEDS-CAP, EXHAUSTED-IS-ZERO — all discharged (SPARK, same core as the grant decider).
Each Post carries the defining equation, so the Post-weaker-than-body class does not bite on this core.
The worst-case draw-down inside the refund window is bounded by the cap BY CONSTRUCTION (VELOCITY-BOUNDS-LOSS): the loss ceiling is a theorem, not a rate limiter's promise.
The truth table graded 11/11 by the forge harness, including the arrears refusal and both velocity edges.

Proof inventory — NOT proven

A zero-amount spend is PERMITTED even with an exhausted window (0 <= 0 holds) — proven behaviour, stated here so nobody mistakes the theorem for 'an exhausted window refuses everything'. It refuses every positive amount.
Balance, Cap and Drawn arrive as Naturals established by the caller; nothing here proves the caller folded them honestly from the journal.
The front shell (credit_spend_front.adb) is compile-gated only.

Open issues — raised, standing until closed

Nothing consumes this decider yet: the portal's Go shell has no spend seam, so no spend — charged or refused — has ever crossed this front in production. It stands in the zone as a delivered, testable artifact whose consumer is future work; this bench is currently the only place it runs.
The front shell is compile-gated only.
No dedicated adversarial pass recorded against this artifact.
The zone bench's token charset ([A-Za-z0-9_]) excludes '-', so a NEGATIVE number can never reach this front through the web bench: the front's own refusal of negatives is exercised only in the forge harness, not re-runnable here. A rail of the bench, stated rather than hidden.

Security checklist — graded from evidence

Item	Grade	Evidence
Memory safety by construction	core: yes, by construction; front shell: not established	SPARK expression functions over Natural with discharged obligations; the .adb shell is compile-gated Ada
Proof coverage	core: all obligations discharged; front shell: none	gnatprove logs in wu-credit-grant/edge-spend; the shell carries no proof obligations
Fail-closed doors witnessed	witnessed on this bench only	exit-3 refusals on malformed numbers and wrong arity graded in the 11/11 table and re-runnable here; no production door consults this front yet, so no production refusal has ever been witnessed — the honest limit of the grade
Adversarial pass	not yet	no adversarial pass recorded — stated, not hidden
Dependency surface	0 external modules beyond the GNAT runtime	with-clauses: Ada.Command_Line, Ada.Text_IO, the core package; no third-party code
Provenance chain	intact	prose spec -> prove logs -> provenance JSONs in wu-credit-grant/edge-spend; unconsumed in production, so the chain ends at delivery rather than at a wired door

The fitting bench

fitting evidence: none yet — no artifact has been fitted to a customer environment

Testing bench: credit_spend_front