Testing bench — build_admission

The build-admission decider: may this build be admitted to the factory queue? Six boolean facts in, one verdict out. The judgement is a proven SPARK conjunction (Build_Admission_Pkg.May_Build) with no other path to admission; this front is its forged argv shell. Every admission the portal ever makes crosses this exact binary.

Binary: wired (named by BUILD_ADMISSION_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
prepaid, all facts good — admitted	true true true false true false	true	0
arrears, meter writable — admitted	true true false true false true	true	0
NO-ACCOUNT-NEVER-BUILDS — no account attached	false true true false true false	false	0
BAD-STANDING-NEVER-BUILDS — standing not good	true false true false true false	false	0
UNKNOWN-MODE-NEVER-BUILDS — both modes asserted	true true true true true true	false	0
UNKNOWN-MODE-NEVER-BUILDS — neither mode asserted	true true false false true true	false	0
PREPAID-WITHOUT-CREDIT-NEVER-BUILDS	true true true false false false	false	0
ARREARS-UNMETERED-NEVER-BUILDS — blind meter refuses	true true false true false false	false	0
prepaid admitted — meter fact does not bear on prepaid	true true true false true true	true	0
arrears admitted — credit fact does not bear on arrears	true true false true true true	true	0
malformed token — the front itself refuses (exit 3); the core never sees it	bogus true true false true false	(no output)	3
wrong arity — the front itself refuses (exit 3)	true true true	(no output)	3

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

Proof inventory — proven

Build_Admission_Pkg.May_Build carries the full biconditional Post: 'Result equals the five-clause conjunction, so admission has exactly one path and it is the stated one (SPARK, ledger 162, gnatprove obligations discharged; captured in ada-factory components/).
The five fail-closed theorems — NO-ACCOUNT-NEVER-BUILDS, BAD-STANDING-NEVER-BUILDS, UNKNOWN-MODE-NEVER-BUILDS, PREPAID-WITHOUT-CREDIT-NEVER-BUILDS, ARREARS-UNMETERED-NEVER-BUILDS — follow from that biconditional; they are consequences of the proven contract, not separate promises.
The Post carries the defining equation (Result = the body's expression), so the Post-weaker-than-body class does not bite on this core: the contract is exactly as strong as the body.
The truth table graded 12/12 by the forge harness before admission, and the artifact was admitted via signed receipt.

Proof inventory — NOT proven

The front itself (build_admission_front.adb — argv parsing, the exit-status mapping, IO) is compile-gated only: tested by the truth table, never proven. The proof covers the judgement, not the shell around it.
The signed-receipt machinery that admitted this artifact (the Admission_Receipt package) sits in the Post-weaker-than-body class — its Post proves less than its body does — so the receipt's own guarantee carries exactly that reduced weight, and this note will not dress it up.
Nothing here proves the CALLER assembles the six facts honestly: the portal's fact derivation is Go, tested not proven, and the examination bench exists so a member can see those facts with their sources named.

Open issues — raised, standing until closed

The front is compile-gated only — a forged, proven argv shell is owed if the shell is ever to carry the same weight as the core.
No dedicated adversarial pass has been recorded against this artifact; the bench's malformed-token rows exercise the front's own refusal, which is necessary but not a pass.

Security checklist — graded from evidence

Item	Grade	Evidence
Memory safety by construction	core: yes, by construction; front shell: not established	the core is a SPARK expression function with no IO and no state, absence-of-runtime-error obligations discharged (ledger 162); the .adb shell is Ada with runtime checks, compile-gated only
Proof coverage	core: all obligations discharged; front shell: none	gnatprove run recorded in the wu-build-admission prove logs; the shell carries zero proof obligations because it was never brought under SPARK_Mode
Fail-closed doors witnessed	witnessed	exit-3 refusals on malformed tokens and wrong arity graded in the 12/12 truth table and re-runnable on this bench; the unwired-decider refusal (unset BUILD_ADMISSION_DECIDER refuses every admission) is exercised by the portal's own tests
Adversarial pass	not yet	no adversarial pass recorded against this artifact — stated, not hidden
Dependency surface	0 external modules beyond the GNAT runtime	the front's with-clauses are Ada.Command_Line, Ada.Text_IO and the core package; no third-party code anywhere in the artifact
Provenance chain	intact	prose spec -> forged spec -> prove logs -> provenance JSONs in wu-build-admission/edge -> admitted via signed receipt (ledger 162); the chain's weakest link is the receipt's own Post-weaker-than-body caveat, named above

The fitting bench

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

Testing bench: build_admission_front