How Poly is put together

One question each

In reading order. Components link to the source they were drawn from, at the revision analysed.

Generated from an analysis of the repository at 116bb50 (Poly v1.3.1) with archlens. The diagrams show what the code does, and mark what the design describes but the code does not build.

Doctrines, guarantees and constraints

The statements the diagrams are drawn to support, as the architecture document gives them, with the risks it names against itself.

Doctrines

• The semantics is the definition, and every check compares the lowering with it 04-semantics defines what a program means; translation validation runs the lowered module and poly-ref on every reachable state and refuses any disagreement
• An effect meets five refusals before the policy engine decides origin, memory, budget, grant and mandate each refuse or escalate finally whatever a policy says; only then does the Polyaxion gate propose
• The core is host-neutral and a host adapter is configuration only no package names a host or imports a host SDK; an adapter is JSON and markdown that launches poly mcp, poly lsp or poly run --mcp, so a new host adds no code

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
• 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
• 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
• A step and its ledger events commit together or not at all the ledger store subclasses polyrun's and writes the step event inside the dispatch transaction, so the kernel's atomicity covers the ledger
• An irreversible effect that may be attempted twice is not admitted unless it names how its target is kept from running it twice poly-ref reports PL4003 with a witness (a delivery in which the target may execute twice) unless the effect is keyed (an idempotency header and a window that holds the retry horizon) or idempotent by nature in the pinned standard library. The runtime sets the key on every write in a capability the handler cannot bypass. What poly does not verify are the assumptions K17 (the target honours the key) and K18 (an effect declared idempotent by nature is), which a certificate names when an effect declares them

Constraints

• poly-ref shares no code with the compiler a checker written from the same code would agree with its bugs; poly-ref may import only node builtins, sam-pattern and type-only imports of core
• No check package imports poly-io network code lives in poly-io alone, so nothing on a check path can open a socket
• No language-model call decides a verdict or a gate decision a verdict must be a function of the program and the semantics. The one way to a model is poly new, which the CLI and the MCP server load by name; its drafts go back through the pipeline and are never admitted by it.
• In packages/, only poly-new and poly-mine may start a process every child process of the product is then one of three named tools, started with a fixed argument vector, a fresh environment, a pin check, a timeout and an output cap. The demo is outside packages/ and starts a process in three places only (the replay driver, its scripts and the stand-in's key tool), which rule 7 names
• Engines are copied unchanged, never forked poly relies on the Poly stack conceptually, not physically; a change an engine needs is made in its own repository and copied in again, and a test re-hashes every vendored file

Trade-offs

• A check not run blocks admission instead of being recorded in the certificate the architecture document has the certificate carry a notRun list; the code refuses to admit instead, so no certificate ever says a check was skipped, at the cost that a build whose optional stage cannot run cannot be admitted at all

Risks

• Nothing in the packages records advice the runtime can append an advice event, but no package calls it and no advisor is consulted at issue or at the gate; only tests call it. The architecture document describes the advisor as part of the runtime.
• The key proves a retry runs once; it says nothing about a second request The key is the intent id, so a second request is a second intent with a second key. The concierge of v1.3.0 refunded twice for that reason, and v1.3.1 fixes the program with a refund ledger in the Desk (per customer thread, because the order's identity is opaque). The checker's model cannot tell the order, so this class of defect is shown by the room, not decided by the check; per-order identity is proposed for v2.0