Packages, Resolution and Trust: PatLang's Package Design

PackagesPackages became pressing once the toolchain stopped depending on Rust. Useful work with documents and media needs readers and writers for PDF, Office files and image formats, and nearly all of those sit on top of DEFLATE compression and zip archives. So the first packages are that common base, written as pure PatLang byte-level code over List<Int>, with no host-language shortcuts.

From a publisher's files to a program that includes them, the pieces fit together as below. The manifest format, the content hashes and the first packages exist; resolution, the install plan and the group signatures are designed and not yet built.

What a package is Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

AA package is a versioned set of PatLang include files described by a manifest. A program uses one by including its entry file, and since the v2 compiler includes each file once by its normalised path, two packages can both include a third without its top-level code running twice.

The manifest, manifest.pkg, is plain text, one key value field per line, every value ASCII, so that a PatLang program can parse it with one line split and one split at the first space:

# packages/zip/manifest.pkg
package zip
version 0.1.0
summary zip archive reader and writer (stored and deflated entries, CRC-32 checked)
entry zip.patlang
include zip.patlang
depends deflate >= 0.1.0, < 0.2.0
file zip.patlang sha256 9fc97f0f52d5c63f6a5bba758245058a933d5c30fa4d37cca7f37ed1584d6d4c

Two choices in that format carry most of the design. Version ranges are written out in full, >= 0.1.0, < 0.2.0, with no caret or tilde shorthand, which keeps both the parser and the resolution rules to plain comparisons. And every shipped file carries its SHA-256 hash, so the manifest pins the exact bytes a program will load. Files are committed with LF line endings on every platform, so that a checkout's bytes are the bytes that were hashed. A small tool built on the sha256 package checks every file line and reports ok, MISMATCH, MISSING or MALFORMED.LF everywhere avoids hash drift on checkout

The first three packages Ephemeral / ToolingKnowledge that evolves in months to a year — check for updates

EachEach package ships Gherkin feature files and a runner, and each runner uses Python's standard library as its reference implementation: zlib, zipfile and hashlib. Interoperability is checked in both directions, so PatLang must read what Python writes and Python must read what PatLang writes. The Python is a test oracle only and never ships as package code. Each package also has a benchmark at four doubling input sizes, the habit that catches a quadratic loop before it reaches real files.

Resolution as logic Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

ChoosingChoosing versions that satisfy every package's constraints at once is a search problem, and package managers have long treated it as one. Mancinelli and colleagues, analysing the Debian and Mandriva distributions, encoded whether a package can be installed as a boolean formula and handed it to a SAT solver¹.SAT solvers find satisfying assignments

PatLang already has a constraint engine: rule_add and solve do Prolog-style backward chaining, as the goal-oriented programming demo shows. The plan is to use it directly. Reading a manifest asserts facts:

rule_add("pkg_available", ["deflate", "0.1.0"], [])
rule_add("pkg_available", ["zip", "0.1.0"], [])
rule_add("pkg_requires", ["zip", "0.1.0", "deflate", "ge", "0.1.0"], [])
rule_add("pkg_requires", ["zip", "0.1.0", "deflate", "lt", "0.2.0"], [])

Constraint satisfaction then becomes ordinary rules over one built-in comparison, version_cmp:

rule satisfies(V, ge, Min) :- version_cmp(V, Min, gt).
rule satisfies(V, ge, Min) :- version_cmp(V, Min, eq).
rule satisfies(V, lt, Max) :- version_cmp(V, Max, lt).

rule dep_candidate(Pkg, PVer, Dep, DVer) :-
    pkg_requires(Pkg, PVer, Dep, Op, Bound),
    pkg_available(Dep, DVer),
    satisfies(DVer, Op, Bound).

One question is left open on purpose. "Every constraint holds" is universally quantified, and plain Horn rules express that through negation: no constraint is violated. Whether solve gains negation as failure, or the check stays a small loop over the solutions of dep_candidate, will be decided when resolution is built.

Installation as a plan Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

OnceOnce versions are chosen, installing them is a planning problem: reach the state installed(zip, 0.1.0) through actions that fetch, verify and install one package each, where installing a package requires its dependencies installed first. PatLang's GOAP planner (action_add/plan) does uniform-cost search over actions with preconditions, effects and costs, which fits that shape directly:GOAP: Goal-Oriented Action Planning

action_add("fetch_deflate_0_1_0", [], [["fetched", ["deflate", "0.1.0"]]], [], 1)
action_add("verify_deflate_0_1_0", [["fetched", ["deflate", "0.1.0"]]],
           [["verified", ["deflate", "0.1.0"]]], [], 1)
action_add("install_deflate_0_1_0", [["verified", ["deflate", "0.1.0"]]],
           [["installed", ["deflate", "0.1.0"]]], [], 1)
action_add("install_zip_0_1_0",
           [["verified", ["zip", "0.1.0"]], ["installed", ["deflate", "0.1.0"]]],
           [["installed", ["zip", "0.1.0"]]], [], 1)
let steps = plan([["installed", ["zip", "0.1.0"]]])

For zip and its one dependency, the actions and their preconditions form this graph, and the plan is a path through it that ends at installed(zip):

The actions are generated from the resolved facts, one set per candidate version, and policy lives in the costs. An install whose effect already holds can cost nothing, so the planner prefers what is already present; cost rising with a version's age makes it prefer the newest version that fits. Verification is a precondition of installation in the plan's own structure, so no route to installed skips it. Resolution and installation are designed but unbuilt; the manifest format, the three packages and the hash checker exist.

Trust: one group model for networking and packages Ephemeral / ToolingKnowledge that evolves in months to a year — check for updates

TodayToday a package is trusted because it sits in the PatLang repository. That stops being enough as soon as packages come from anywhere else, and the same problem is already waiting on the networking side. PatLang programs on one machine can discover each other and call each other's advertised capabilities, but a capability description is entirely self-reported, and the signals listener binds to localhost only. On one machine that is a risk inside one user's trust boundary. Across a network it becomes the central problem.

The project's decision is to answer both with one model. It comes from a design for PatLang networking called ensemble membership, and the package plan applies it to publishers and releases. Neither is built yet.

Ensemble membership

The networking design starts from a launcher that starts a set of independent PatLang processes and then leaves. It is a genesis provisioner with no continuing authority. Each process receives a bootstrap package: a group identifier, a high-entropy 256-bit bootstrap secret, a one-use launch ticket of its own, hints at which IP addresses its peers may be on, and the group's protocol parameters. From there the processes have to do everything themselves:

1. Discover each other when addresses are known but service ports are not. A discovery probe carries a hint computed as a message authentication code over the bootstrap secret and the current time window, so a process from another group learns nothing from it, not even that the group exists.
2. Prove to each other that they belong, with no certificates. A 256-bit secret cannot be guessed, so the peers need no password-authenticated exchange. Each pair runs an ephemeral X25519 key exchange² with the bootstrap secret mixed into the transcript, the pattern of the Noise framework's psk handshakes³ and TLS 1.3's psk_dhe_ke mode⁴. Only another holder of the secret can derive the resulting key. The transcript binds both sides' nonces and ephemeral keys, the group, the protocol version and the hash of the sender's launch ticket, and key confirmation runs in both directions. The group then forms over these pairwise channels.
3. Agree on who is in the group. Each candidate makes a fresh signing key pair, its membership witness, and sends the public key with its launch ticket, encrypted, over those channels. The candidates order themselves deterministically and commit a genesis record once every candidate has signed the identical record. A duplicated or unlisted ticket aborts genesis.
4. Replace bootstrap authority with membership. After genesis the bootstrap secret is retired and the tickets are burned. The membership view lists each member's public key, and each member is known by a handle, (group, epoch, slot, incarnation), which means nothing outside that group and epoch.

Formation, for two of the processes, runs as follows; every pair of processes does the same, and the launcher is gone before any of it starts:

Membership here is relational. A process can belong to several groups at once, with unrelated handles, keys and epochs in each, and no protocol data links its memberships unless the application chooses to.

Collective authority

A group makes decisions by quorum, and a quorum counts distinct admitted memberships: several valid messages from one member still count once. The design gives three ways for approvals to travel, adopted in order:

Approvals and evidence are signatures made with the witness key. A key shared by two members, such as the one from their pairwise exchange, would let either forge the other's message and prove nothing to a third member, and evidence that a member signed two conflicting proposals has to convince everyone else.

Anonymous approvals still have to be counted once each. For that the design uses a nullifier: a value derived deterministically from a member's secret witness and the exact decision being voted on. The same witness voting twice on one decision produces the same nullifier, so the verifier counts unique nullifiers. A nullifier is scoped to one decision and identifies nothing beyond it, which keeps it from turning into an identity of its own.

Disagreement and divergence

Agreement is deliberately bounded. A proposal extends one committed log head and names the current epoch and view; a member approves at most one of any conflicting proposals for the same decision; and a proposal commits when a quorum of current members, by default ⌊N/2⌋ + 1 of N, signs the identical proposal. The certificate and the new log head are written to disk before anything acts on them.

Within that, the design separates two kinds of disagreement. Members who disagree about a choice are what voting is for, and the quorum settles it. Members who disagree about a fact show that at least one of them is behind, cut off, faulty or lying, and that is worth asking about. So the design questions claims and state and never questions votes: one of its invariants is that a member's choice between proposals, or a rejection that claims no failed check, is never grounds for a challenge, quarantine or exclusion.

For that line to be drawable, a vote has to say what it is claiming. A proposal names its checks: conditions over the committed log and the payload, such as the require clauses of the action it proposes or a GOAP plan's preconditions. Each check is named by the hash of its PatLang source and must be a pure function of the log at a given head and the payload, with no clock, randomness or local state, so that every member computes the same answer. It is the same discipline PatLang already applies between its two engines, whose agreement suite requires a program to give the same result on both. A vote then carries the log head it ran the checks against, its verdict, and the result of each check:

Vote {
  group_id, epoch, view_hash, decision_id, payload_hash
  log_head                                  # the head the checks were run against
  verdict: approve | reject
  checks: [(check_hash, holds | fails)]     # all of them to approve; those that failed to reject
  signature
}

An approval says every check holds at that head. A rejection either names the checks it found failing or names none, and a rejection naming none is a choice from which nothing follows. A member may also simply not vote. Three kinds of factual divergence are questioned:

The outcomes are graded by what each can prove. A member that turns out to be behind fetches the certificates between its head and the committed one, checks each, and catches up with nobody blamed. A head presented as committed without its quorum certificate is objective evidence, and so are two different signed states from one handle for the same epoch and sequence number, which is equivocation and goes to exclusion. A false check claim is objective as well, since every member can re-run the check, but it cannot distinguish a lie from a bug in the member's engine, so on its own it leads to quarantine and a report naming the check's source hash; excluding the member still needs the usual quorum. Two different signed answers to one nonce mean two processes hold the same key, which calls for a rekey. That last check is cheap and incomplete: a thief who stays silent is not caught by it. Silence in general counts only as operational evidence, because the member may simply be cut off.

Questioning is itself limited, so that it cannot become a way to attack a member. Every challenge is signed and therefore attributable, and must name its cause, the two conflicting votes or the stale record; a challenge naming none is dropped. Each member may challenge each other member only a bounded number of times per epoch, and challenges past the bound are dropped and count as operational evidence against the challenger. Challenges and answers all go into the transcript. In the anonymous mode a vote's check claims travel inside its proof, so a verifier re-runs the checks and refuses to count a vote whose claims are false, but it cannot blame the voter without linking the vote to a member, which is what that mode exists to prevent.

Some of this is still open in the plan: the challenge bound, what subset of PatLang counts as pure enough for a check, how a check's source travels with a proposal, and whether repeated false check claims with no other evidence should ever lead to exclusion, since each one may be an engine bug. One planned demonstration exercises all three outcomes at once: a member cut off rejoins behind and catches up unblamed, a member approving a plan whose precondition fails at the named head is quarantined, and a member who rejects everything is never challenged.

Exclusion as a configuration change

Admission, departure and exclusion are transitions from one epoch to the next, each approved by a quorum of the epoch before it; a peer list edited locally changes nothing the group recognises. A member can move through four stages. Suspicion is a claim, quarantine a temporary restriction, exclusion the removal of current authority, and revocation an attempt to stop the same credential coming back. Evidence carries different weight by kind. A member that signs two conflicting proposals for the same decision, presents a head without its certificate, or makes a false check claim has produced objective, checkable evidence; repeated malformed traffic is operational; distrust with nothing checkable behind it can justify investigation or quarantine, but needs a higher threshold before anyone is excluded for good. When a quorum votes on excluding a member, the accused is left out of both the vote and the denominator, so a compromised member cannot block its own removal. A committed exclusion advances the epoch and rotates the keys, and the excluded process can no longer authenticate current messages.

The design records one trade-off as unavoidable: perfect anonymity and durable blacklisting are incompatible unless a returning applicant proves hidden continuity with a credential that can be revoked. Its first version sits at a stated point on that spectrum. Launch tickets are burned at genesis, the bootstrap secret is retired, and an excluded process can return only through an invitation the ensemble issues, with a fresh handle and incarnation.

Group decisions as PatLang facts

The PatLang-facing interface exposes groups and keeps cryptography out of reach: ensemble_bootstrap, ensemble_propose, ensemble_seek_agreement, ensemble_propose_exclusion, ensemble_create_invitation and their neighbours, with secrets held as opaque handles. Group state is projected into the logic engine as facts such as member(g, peer_4, epoch_7), quorum_proved(g, proposal_31, threshold_3), excluded(g, peer_6, epoch_8) and diverged, and raises ordinary PatLang events such as group.divergence.check and group.divergence.resolved. A quorum certificate then takes part in ordinary PatLang reasoning: a GOAP plan whose activation requires quorum_proved runs only after the group has approved it, and an exclusion changes who may contribute. With approver privacy on, only the quorum fact is projected.

The design sets out its own limits. It assumes a partially synchronous network and crash-recovery, makes no claim to general Byzantine consensus, and stops a process safely if it ever sees two conflicting certificates for one decision. The whole mechanism is a PatLang package compiled by v2, with its state machine taking the transport as a parameter so that it can be tested over simulated networks. The only code it trusts outside v2-compiled PatLang is the operating system's and the browser's, for sockets and for cryptographic operations on secrets. Its planned demonstrations include five processes forming a group after the launcher has already exited, one process holding unlinkable memberships of two groups, and an excluded process restarted with its old witness and ticket failing to get back in.

Applying it to packages

A package's publishers form a group in this sense, and the decisions the group makes are releases. A release is a statement naming a manifest by its hash, and the group's quorum certificate over that statement is the attestation. Members join and leave through epoch transitions, so the group's whole history is a chain starting at its genesis record. A consumer trusts a group by pinning its genesis hash once, and checks everything else against the chain. Today's single maintainer fits the same formats, as a group whose quorum is 1 of 1.

Package trust differs from the networking case in three ways, and each changes the design:

• The verifier is an outsider. A consumer belongs to no group, holds none of its keys, and is not online with it. Signatures over public keys listed in the view, which the networking design already uses so that one member can convince another, are what let an outsider check a release too.
• Verification is offline and late. A consumer may check a release years after it was made, with no member online, so everything it needs travels as files: the group's log and the release's certificate.
• There is no launcher. A publisher group's founders each make their own key pair and sign the genesis record, and its hash is what consumers pin.

Every record is plain text in the manifest's own key value format, and starts with a line naming its kind and format version. That line separates the kinds by domain, so a signature over one kind of record can never be read as a signature over another:

record patlang-release 1
group 3f9c...
epoch 1
view 51aa...
package zip
version 0.1.0
manifest 9fc9...

The records link into one chain, anchored at the hash the consumer pinned:

Verifying a package walks that chain using public data only: the file hashes against the manifest, the genesis record against the pinned hash, each epoch transition against a quorum of the view before it, and finally the release statement against a quorum of its own epoch's view. Two further checks address attacks on package distribution that Cappos and colleagues documented, in which a malicious mirror serves old signed metadata, either to roll a client back or to freeze it at one point in time so that it never sees a fix⁵. The consumer's trust store records the highest epoch it has seen for each group and refuses a log that ends below it. A group can also withdraw a release, or mark a compromised member's key as revoked from a date, after which releases that depended on that key no longer verify. Withdrawn versions are never offered to the installation planner as candidates, and the planner's verify action produces verified only when verification passed.

Each dependency is verified against its own pin, since trust in a package does not carry to the packages it depends on; a manifest can at most recommend a pin for one. Where the very first pin comes from is left to the project owner, because a package cannot vouch for its own genesis hash: whoever could change the package could change the pin beside it. The candidates are pins shipped with the toolchain, pinning on first use, and pins given by the user out of band, and they can be combined.

Quorum certificates over releases resemble the threshold-signed roles of The Update Framework, which let a repository survive the compromise of some of its keys⁶. Sigstore takes a different route, binding a short-lived signing certificate to a developer's existing account identity and recording each signature in a public transparency log⁷. In PatLang's model a publisher is a member of a group and nothing more, and no step of verification needs anyone's real-world identity.

Where the cryptography runs

The packages side builds the shared parts first, since it needs no network: the record reader, the view and transition checks and the signature calls, which the ensemble then reuses. All of it is PatLang compiled by v2, with one rule about secrets. PatLang integers are tagged and grow into bignums, so an operation's time can depend on the value it works on, and code that handles a secret key could leak it through timing. Until that changes, no secret-handling operation is written in PatLang.

A key never enters PatLang as bytes. It stays inside the operating system or the browser, and PatLang code holds an opaque handle to it (a BCRYPT_KEY_HANDLE, a CryptoKey); destroying the handle is how a key is erased.

Cryptography in PatLang itself

The route to signing and key exchange written in PatLang is a language feature: integers modulo n as a built-in type in the numeric tower. A modular value's modulus is fixed when it is made, which fixes its width. It never promotes to a bignum, and every operation on it is a fixed loop over a fixed number of limbs, so its time depends on n alone. Fixed-width machine words are the case n = 2^k: SHA-256 and ChaCha work modulo 2³², and bignum limbs modulo 2⁶⁴. The field under Ed25519 and X25519 is the case n = 2²⁵⁵ − 19, and Ed25519 signatures also work modulo the group's order.

The specification is to promise that an operation's time depends only on n, and v2's tests are to check that no branch or memory access in the compiled routines depends on a value. With that in place, Ed25519, X25519 and ChaCha20-Poly1305 can be written in PatLang, checked against the published test vectors, and replace the operating system calls. Whether those calls are built first or the trust work waits for modular integers is still to be decided.

Where zero knowledge fits

A zero-knowledge proof, as Goldwasser, Micali and Rackoff defined it, convinces a verifier that a statement is true while conveying nothing beyond the fact that it is true⁹. In this model it has one precise job. Slots are group-relative and say nothing about who a member is, so a group already reveals no real-world identity. What a slot-signed certificate does reveal is which slots approved a release or a decision. The research phase hides that: each approval carries a nullifier and a zero-knowledge proof that the nullifier came from some member of the current view, so a verifier learns that a quorum of current members approved, and nothing about which. Semaphore is an existing protocol of this shape, in which a member proves membership of a group and publishes a nullifier that prevents signalling twice on the same topic¹⁰.

Such a proof needs a SNARK or a linkable ring signature. Neither the operating system nor the browser provides one, so anonymous approval waits for modular integers and a reviewed construction that can be written in PatLang on them. The record formats already leave room for it, as a new certificate kind with the release statement unchanged. The same ordering runs through both designs: start with explicit approvals that are easy to inspect, get admission, agreement, exclusion, replay protection and persistence right first, and only then swap the approval representation for a more private one, with the PatLang-facing behaviour kept the same.

The toolchain as part of the trust story Applied / MethodologicalKnowledge with a 5–10 year half-life — stable practice

AA signature on source code says nothing about the compiler that turns it into machine code. Thompson made the point memorably: a compiler can be altered to insert a backdoor into programs it compiles, including future copies of itself, leaving no trace in any source code¹¹. Two developments in PatLang's compiler bear on that.

First, builds are deterministic. The swarm-structured v2 compiler produces byte-identical executables from sequential and parallel builds, and from two builds sharing one artefact store. Reproducible builds of this kind let anyone check that a published binary matches its source by building it again and comparing bytes, which Lamb and Zacchiroli present as a way to raise the integrity of software supply chains¹².

Second, the compiler can be rebuilt by a second, independent route. v2 writes its own IR as text, and a short reader in Python, using only its standard library, builds the compiler from that IR; the compiler it produces rebuilds itself, and the results are byte-identical. Wheeler's diverse double-compiling counters Thompson's attack by compiling a compiler's source twice, first with a second, trusted compiler and then with the result, and checking that the final output is bit-for-bit identical to the compiler being tested¹³. The Python reader resembles that second compiler, with one limit that our reading has to state: the IR it reads was itself produced by v2, so the check covers the step from IR to executable and leaves the step from source to IR to be checked another way. What it does give is a bootstrap with no saved seed binary, whose trusted base is a text file and a reader short enough for a person to audit.

See also

Presence,Presence, discovery and non-blocking spawn describes the same-machine discovery mechanism whose self-reported descriptions the trust work has to address. Goal-oriented programming runs the backward-chaining resolver and GOAP planner that resolution and installation are designed around. The swarm compiler and Blocks, ownership and memory cover the compiler and runtime whose determinism the reproducibility argument rests on.