Skip to content

Feature-decision procedure

Every new feature you might want to add to Punix gets classified into one of four categories. This is the protocol — apply it before writing code; never "work around."

The classification determines where the feature lives:

Category Where it lives When it applies
Native Pure config layer (the IC core handles it) The feature can be expressed by the inheritance-calculus rules themselves.
Fold-over-value (a) A pure transform applied to evaluated values; lowered to a fold The feature is a deterministic function of evaluated values.
Provably-host (b) Below the eval/realise seam The feature is oracle-dependent — it needs something from the host (env vars, files, network, time) that the pure layer cannot see.
Totalize-as-data © Modelled as data in the frontend, not as an effect The feature LOOKS like it needs an effect, but can be encoded as "this contribution never existed" or similar.

Examples

Feature Category Why
if/then/else, list flattening, scenarios Native The IC rules cover them.
force (CVE-pin propagation), scenario-merge Fold-over-value Pure transformation of evaluated values.
Secrets ({from_env=…}, {from_file=…}) Provably-host Oracle-dependent. The pure layer must NOT see the value.
GC, deploy-time fetch, system time, IFD Provably-host All require host state the pure layer can't see.
Removal of a contribution Totalize-as-data Modelled in the frontend as "this contribution never existed."
Build cycles, generation manifests Provably-host Host filesystem state.

Why this matters

The decidability + termination proof of the pure layer requires that nothing in that layer perform an effect. A PR that puts a (b) feature — secrets, IFD, build-cycle, generations, removal — into the pure layer is rejected by theorem, not by review preference. The proof would no longer go through.

This is also what gives Punix its operational guarantees:

  • "Permuting source ⇒ byte-identical store paths" works because every value in the pure layer is a deterministic function of syntax.
  • "Secrets never reach the store" works because secrets are classified (b) and structurally cannot enter the pure layer.
  • "punix check cannot diverge" works because the type checker walks a finite tree once.

Violate the procedure, and you violate at least one of these.

How to apply

When you're about to write a new feature:

  1. Write down what oracle it needs, if any. Env vars? File reads? Network? Time? Filesystem state? If yes, it's (b).
  2. Write down what evaluated values it transforms, if any. If it can be expressed as "given these resolved values, produce that resolved value", it's (a).
  3. If neither, check whether it can be encoded as data © — e.g., "this contribution never existed" instead of "remove this contribution."
  4. Only if all three are no is the feature native.

The default classification is (b) — that's where most new features land in practice. Putting a (b) feature in the pure layer is the most common architectural mistake.

Worked example: "delete a contribution"

A naive design might add a delete primitive: delete M.field ⇒ M.field is no longer set in the composed root.

Classification:

  • Native? No — the IC rules don't have "delete." Adding one changes the structural recursion.
  • Fold-over-value? Maybe, but the consequences are subtle. A delete that runs after CIA arbitration is a post-hoc effect; the conformance property "permuted source ⇒ byte-identical values" gets fragile.
  • Provably-host? No — there's no oracle involved.
  • Totalize-as-data? YES. Encode "delete" in the frontend as "this contribution never existed at all." The lowerer drops the contribution before the IC layer sees it. No structural change to the pure layer. No new IR node. Decidability proof survives.

That's why Punix doesn't have a runtime delete; the surface is "don't write that contribution in the first place," and migration tools rewrite source to do so.

Worked example: "use a secret as a build input"

A user wants to use {from_env="GH_TOKEN"} as the auth token in a source = { type = "url", url = "…", token = … } field.

Classification:

  • Native? No — the token IS an env-time value.
  • Fold-over-value? No — the value is not in the IR.
  • Provably-host? YES. Read at deploy/realise time, not at type-check.
  • Totalize-as-data? No — the value isn't substitutable.

Where it lives: at the fetch boundary, below the seam, like secrets in Service.environment. The pure layer sees the reference string only; the fetcher resolves the env var at realise time.

(Stage 6 wires this for deploy-time Service.environment; realise- time fetch-with-secret is roadmap — but the classification is already settled.)

Reviewer checklist

When reviewing a feature PR, ask:

  • Did the author state the category?
  • If (a), is the lowered fold pure (no env / fs / time reads)?
  • If (b), does the feature live below the seam?
  • If ©, does the frontend rewrite produce the same canonical IR as if the source had been written that way to begin with?
  • If "native," does the new rule preserve termination + the finite-tree structural recursion?
  • Is there at least one conformance test that fails if the feature is moved to the wrong category?

The last point matters most. A correctly-classified feature has a property the conformance suite can pin. If you can't write one, the classification is probably wrong.