Testing bench — credit_grant

The credit-grant decider: may this grant be made? Each grant kind carries exactly one form of evidence — a purchase grants on a validated receipt, a discretionary grant on an authorised operator, an achievement on a server-side attestation — and evidence that has ever granted, on any membership, never grants again. The judgement is the proven Credit_Grant_Pkg.May_Grant; this front is its forged argv shell, and it is the only door credit enters any account by.

Binary: wired (named by CREDIT_GRANT_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
validated purchase, never granted before — granted	purchase true false false false	true	0
PURCHASE-NEEDS-RECEIPT — no validated receipt, no grant	purchase false false false false	false	0
GRANT-IS-ONCE — a replayed receipt never grants again	purchase true false false true	false	0
no borrowed evidence — operator and attestation cannot stand in for a receipt	purchase false true true false	false	0
authorised operator award — granted	discretionary false true false false	true	0
DISCRETION-NEEDS-OPERATOR — unauthorised, no grant	discretionary false false false false	false	0
server-side attested achievement — granted	achievement false false true false	true	0
ACHIEVEMENT-NEEDS-ATTESTATION — a client asserting its own completion is not evidence	achievement false false false false	false	0
GRANT-IS-ONCE — a replayed attestation never grants again	achievement false false true true	false	0
unknown grant kind — the front itself refuses (exit 3)	bribery true false false false	(no output)	3
wrong arity — the front itself refuses (exit 3)	purchase true	(no output)	3

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

Proof inventory — proven

Credit_Grant_Pkg.May_Grant and Has_Evidence carry defining-equation Posts plus the named theorems — GRANT-IS-ONCE, NO-GRANT-WITHOUT-EVIDENCE, PURCHASE-NEEDS-RECEIPT, DISCRETION-NEEDS-OPERATOR, ACHIEVEMENT-NEEDS-ATTESTATION — all discharged (SPARK, ledger 86).
Each Post carries the defining equation (Result = the body's expression), so the Post-weaker-than-body class does not bite on this core.
The truth table graded 13/13 by the forge harness before admission.
Anti-replay witnessed LIVE through the portal on 08-13: the same evidence ref granted once and refused on replay, through the real front, not a mock.

Proof inventory — NOT proven

The truth of Already_Granted is NOT this core's: it rests on the grant registry's append-only integrity, which is ledger machinery (Go), tested not proven. The core proves everything that follows from the flag; nothing about how the flag was established.
Attested means SERVER-SIDE attestation by definition, but no proof constrains the harness from mis-wiring a client assertion into that parameter — that discipline is convention plus review today.
The front shell (credit_grant_front.adb) is compile-gated only — tested by the truth table, never proven.

Open issues — raised, standing until closed

Journalled grants carry no proof that a front admitted them: the credit journal records the movement, not the verdict that allowed it. A grant admitted yesterday is indistinguishable in the journal from one inserted by hand. Module #5 (the receipts module) is owed to close this.
The front shell is compile-gated only.
No dedicated adversarial pass recorded against this artifact.

Security checklist — graded from evidence

Item	Grade	Evidence
Memory safety by construction	core: yes, by construction; front shell: not established	SPARK expression functions, no IO, no state, obligations discharged (ledger 86); the .adb shell is compile-gated Ada
Proof coverage	core: all obligations discharged; front shell: none	gnatprove logs in wu-credit-grant/edge; the shell carries no proof obligations
Fail-closed doors witnessed	witnessed	exit-3 refusals on unknown kind and wrong arity graded in the 13/13 table and re-runnable here; the anti-replay refusal witnessed live through the portal 08-13; the unwired-front refusal (unset CREDIT_GRANT_DECIDER means no credit enters any account) exercised by the portal's tests
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 for the core; open at the journal seam	prose spec -> prove logs -> provenance JSONs in wu-credit-grant/edge (ledger 86); but a journalled grant does not yet carry the front's verdict with it — the module #5 gap named in the open issues

The fitting bench

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

Testing bench: credit_grant_front