From a clean check to a loadable program Diagram

The short answer

• Admission re-runs the pipeline, refuses any check not run, signs a certificate over the digests, and the runtime refuses any file that no longer matches it

Not shown here

• The language packages and the ledger, which admission does not touch
• Connected but out of scope: Workflow server, poly CLI, Check pipeline, Signed records, Feedback commands, Polyaxion

What it guarantees

• A check that did not run or hit a bound is never CLEAN: the verdict fold ranks INCONCLUSIVE and UNDERPOWERED apart from CLEAN, vacuous properties are INCONCLUSIVE, and admission refuses a build with any check not run
• The runtime executes the artefacts the checker checked: the certificate binds each file by digest and load refuses any mismatch, so the checked program is the running program over its check domains
• An agent key never signs a person record: approvals, acceptances, verdicts and adjudications are the owner's decisions; the signature check at admission and at the runtime refuses an agent key, whatever the transport

From a clean check to a loadable program

How does a clean check become something the runtime will load?

Between a check and a run there is a gap in which files can change and a person can be impersonated. Admission closes it with digests and signatures, so the runtime needs no trust in the process that did the checking.

The long read

Admission begins by running the pipeline again over the project and refusing if any machine or policy has a check not run or a vacuous property. The architecture document says such a stage is recorded in the certificate as notRun; the code refuses instead (PT12.5).

Findings can be accepted, but only by a person: Admission reads signed acceptances from Signed records and refuses a record signed with an agent key. It also reads back every promotion, proposal and refit record in the project and compares each with its source or map (PL6513, PL6520, PL6521). A build with policies is admitted only if the Polyaxion engine is the pinned one.

The Certificate format then binds the source and artefact digests, the checked instances, the toolchain versions and the handler closure, and the issuer signs the digest. The certificate sits beside the Certified build.

At load, the runtime verifies signatures, re-hashes the artefacts and checks the toolchain. Any difference refuses the load with a diagnostic.

Terms used here

artefact: A file produced by lowering a machine, such as the contract, the SAM v2 module or the effects manifest. The engines read artefacts and never the source.
certificate: A signed record that binds a program's source and artefact digests to the checks that ran and their results. The runtime loads only what one names.
ledger: The record of every step, advice, decision, outcome, gate verdict and effect of a run, hash-chained per run with signed heads and a periodic anchor.
vacuous: A property whose antecedent is never true where it is judged. It holds for no reason the program gives, so it is INCONCLUSIVE and never CLEAN.
promotion: Adding a mined rule that a person judged real to a program, under a marker, after checking the project, so that admission can read it back.
refit: Fitting a new calibration map from a person's signed verdicts, written as a new file with a signed record and never edited in place.
idempotency key: A value sent with a write so that the receiver can recognise a retry of the same request and do the work once. In poly it is the intent id, and the runtime sets it.