Version 0.1 — Draft (Standards Track)
Status: Draft
Author: Axion Governance Council
Applies to: Axion, T81VM, T81Lang, Cognitive Tiers
Supersession note: RFC-0022 is the preferred forward evolution path and is expected to supersede this RFC upon acceptance.
This RFC introduces the Axion Policy Language (APL), a declarative DSL used to describe recursion limits, shape bounds, and symbolic constraints that Axion enforces at runtime. It defines syntax, semantics, and integration points with the VM and compiler.
Axion currently consumes handwritten JSON-like policies. They are hard to audit and lack formal semantics. APL provides:
spec/cognitive-tiers.mdAPL is a minimal s-expression language:
(policy
(tier 3)
(max-stack 59049)
(allow-opcode TVECADD)
(deny-shape (> dims 4))
(require-proof hash:XYZ))
tier n sets the maximum cognitive tier; Axion rejects programs exceeding it.max-stack and max-trace enforce resource ceilings.allow-opcode / deny-opcode whitelist/blacklist instructions with canonical
ordering to avoid policy conflicts.deny-shape uses predicates referencing tensor metadata defined in RFC-0004.require-proof ties policies to RFC-0008 artifacts.AxPolicy syscalls for reading the active policy.Trap::SecurityFault.t81c validates policies during build, rejecting programs whose source-level
annotations contradict the active policy.@requires_policy(policy_name) on functions.APL now closes the loop on the guard metadata described in RFC-0019. The compiler embeds (policy (loop ...)) hints, (match-metadata ...) s-expressions, and canonical enum/variant ids inside the .tisc header so Axion can pair EnumIsVariant/EnumUnwrapPayload events with policy expectations. Policy authors can express these obligations through dedicated metadata predicates:
(require-match-guard
(enum Color)
(variant Blue)
(payload i32)
(result pass))
require-match-guard asserts that the Axion trace contains a guard event for the given enum and variant with the expected payload chemistry and pass/fail result; it automatically lifts the variant-id and enum-id emitted by the compiler into the policy layer. Policies that allow ENUM_UNWRAP_PAYLOAD or ENUM_IS_VARIANT while also requiring specific guards can therefore prove that guard coverage matches Axion’s deterministic metadata.
Loop hints are exposed through require-loop-hint, for example:
(require-loop-hint
(id 3)
(annotated true)
(bound 100))
This clause ensures the DTS saw a (policy (loop (id 3) (file …) (line …) (column …) (bound 100) (annotated true))) entry emitted by format_loop_metadata and that Axion can match it against the runtime guard trace before permitting high-tier opcodes inside an unbounded loop. The metadata/guard predicates stay optional so legacy binaries without the new instrumentation continue to run, but a missing guard or loop hint can trigger a deterministic Policy Fault if the policy explicitly requires it.
Axion policies may also assert the segment trace strings described in RFC-0020. The runtime now logs each stack, heap, tensor, and meta transition as a verdict.reason such as stack frame allocated stack addr=243 size=16, heap block freed heap addr=512 size=32, tensor slot allocated tensor addr=5, meta slot axion event segment=meta addr=1283, AxRead guard segment=stack addr=42, or AxSet guard segment=heap addr=128. Policies can use:
(require-segment-event
(segment tensor)
(action "tensor slot allocated")
(addr 5))
require-segment-event emits a deterministic Policy Fault if the Axion log lacks the recorded verdict.reason. Guard-dependent policies can similarly demand that AxRead guard ... or AxSet guard ... strings appear before approving privileged actions, tightly binding segment context to policy enforcement.