From what ran to the next rule Diagram

The short answer

• The feedback commands export the ledger as traces, a pinned tool proposes, a person signs a verdict, and the result goes back into the source and through the pipeline and admission like any edit

Not shown here

• The runtime itself and the gate, which only produce the ledger the loop reads
• Connected but out of scope: poly CLI, poly-lang, poly-embed, poly-core, poly-lower, sam-pattern 2.3.0

What it guarantees

• 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 what ran to the next rule

How does a running program's history become a checked rule, workflow or calibration?

A program that runs teaches its owner things the checker could not know. The loop lets that knowledge in without letting a tool or an agent decide: every step has a key, a floor and a check.

The long read

The Feedback commands read the Ledger through a journal reader and write a trace corpus: values for declared domains, a salted token for everything else, erased steps left out and counted.

poly-mine runs polyx on that corpus, or polyness on copied transcripts. Each is started by path with a fixed argument vector, a fresh environment and a pin checked first; polyness runs in a temporary home that is removed afterwards. poly reads polyness's rules by four fixed text templates and never runs its code.

Nothing the tools say is binding. A person signs a verdict on each candidate with a key that is not an agent key, and Signed records keeps it as a file. A rule judged real is promoted into the source under a marker, the pipeline checks the project, and the change is undone if the check refuses it. Admission reads every promotion back and compares it with the source, and the certificate lists them.

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.
poly-ref: poly's own model checker. It is written from the semantics and shares no code with the compiler.
gate: The two-phase mediation of an effect: propose before the call, settle after it. The Polyaxion engine decides allow, deny or escalate.
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.
witness: The path of states and actions that shows a finding, exported as a test and kept so that a person can accept the finding.
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.