Design direction and unresolved guarantees
As a contributor, distinguish the project's agreed direction from decisions still requiring a concrete contract and evidence.
Recorded direction
The following direction was established in the project discussion on 3 October 2026. These are design inputs, not claims of implemented or formally verified behavior.
| Direction | Earlier alternative | Why it changed |
|---|---|---|
| Work at project level in Lockness | Extend one repository's asset endpoint in isolation | Trust publication, retained views and terminal verification cross component boundaries. |
| Terminals are lightweight Web2 applications with cryptographic capabilities | Require application adoption to include operating chain infrastructure | Purpose and risk guide verification policy; the user can build transactions or consume verified data off-chain. |
| Terminals consume anchored data before acting | Accept the data provider's answer as authoritative | Verification connects the answer to an independently accepted root; data providers and proof builders remain replaceable. |
| Own anchor is the optimal deal for trust independence | Equate independent verification with running every data service locally | Keep local root establishment while outsourcing ledger capacity. |
| Institutional publications are a first-class operational offer | Require each terminal operator to maintain an anchor | Obtain roots at low local operating cost under explicit institutional trust. |
| Applications purchase provider availability | Bundle correctness authority with purchased data capacity | Price delivery while terminals verify claims independently. |
| Require provider interoperability and switching evidence | Claim an optimal market from the architecture alone | Market-driven scaling needs practical substitution and measurable service commitments. |
| Anchors emit signed commitments for every block | Anchors choose and retain terminal query sessions | Publication and data-serving availability are independent responsibilities. |
| Terminals use a selected published chainpoint | Terminals ask anchors to coordinate each query | Signed streams supply commitments independently of data retrieval. |
| Chainpoint-bound proof-bearing API | Duplicate Koios response shapes as the governing contract | Query compatibility alone does not establish coherent multi-query reads. |
| Serve complete transaction CBOR as reconstruction material | Define a smaller application-neutral transaction projection now | Sufficiency is application dependent; preserving information precedes optimization. |
| Optional application proof services | Either trust an application backend or do everything locally | Proof construction can be delegated and checked locally. |
Open full size · Mermaid source
Named deployment roles
The project names the roles lockness-anchors and lockness-ledgers, plural because any number of instances is expected. Anchors run nodes and serve signed roots. Ledgers run nodes and serve data and proofs. The lockness-applications role serves application proofs using retrieved ledger history. The lockness-terminals role consumes roots, proofs and data, verifies them, and builds transactions or drives real-world effects from verified facts. These are component boundaries, not a command to create separate repositories now.
Words that constrain the design
Project rulings, paraphrased for readability:
- Separate immutable, hash-addressed content from chainpoint indexes.
- Anchors publish a signed root for every block independently of query sessions.
- The API is governed by chainpoint coherence and evidence sufficient for verification, rather than Koios response compatibility.
The later discussion refined the last statement: historical transactions can be untrusted reconstruction material, while claims used as authoritative ledger or application facts need verification. The precise endpoint claim inventory is still open.
Ledger and application proofs have distinct destinations: ledger witnesses are verified off-chain by terminals and are not carried into transactions. Application proofs are carried in redeemers and checked by application validators. Cardano enforces transaction validity against its own ledger state. This distinction does not stop anchors publishing signed roots.
The temporal distinction is an explicit project ruling:
"the ledger proofs are about on-chain validity (present), application proofs are about on-chain validation (future)"
Here the present is the selected chainpoint. For the UTxO commitment, the proof establishes output membership under the accepted root, not an independent execution of transaction-validity rules. An application proof is intended for checking a proposed transition on-chain; its availability is not a promise of future transaction acceptance.
The verdict layer
The terminal classifies each outcome as verified, refused or unverified. The verdict is the terminal's own classification around acceptance, never a wire object, and it carries no payload of its own. Verified carries exactly the claim acceptance returned. Refused carries acceptance's own refusal at the selected point. Unverified carries only a reason.
The weakest and the strongest deployments are instances of the same types. At the weakest end, an unbound provider offers data without witnesses, and the terminal labels everything it receives unverified. At the strongest end, a session bound to the selected point offers witnesses that the terminal checks against independently accepted anchors, and only then is a claim verified. Nothing in between needs a different interface: the provider declares its binding and whether it offers a witness or a completeness answer, and the policy declares whether the terminal has a verifier and whether it requires completeness.
Unverified arises only from a declared absence of all evidence: no verifier configured, a session declared unbound, or a session bound to the selected point whose answer carries neither a witness nor a completeness answer. With a verifier configured, anything present and wrong is refused, including a witness that fails under the accepted root, a completeness answer offered on a session bound to the selected point that fails its check, and a session declaring a binding to a point other than the one it offers. Otherwise a provider could turn a refusal into a softer outcome by misdeclaring. An answer without a witness is never promoted to verified; the model proves this for every policy, provider and builder, and a compiled mutant that lets an absent witness pass refutes it.
| Decision | Alternative | Why |
|---|---|---|
| Classify around the unchanged acceptance | Change acceptance's result or put the verdict on the wire | Acceptance and its guarantees stay intact; providers make offers, terminals judge them |
| Unverified only for a declared absence of all evidence | Treat every evidence failure as unverified, or every answer without a witness | A misdeclared binding, a wrong witness or a wrong completeness answer must not soften a refusal |
| Reconstruction material is its own type, carried and never evidence | Reuse witness bytes or check reconstruction | It cannot be confused with evidence, and replacing it never changes a verdict |
The act step, described below, consumes the verdict. The wire encoding of the binding, the witness and the reconstruction belongs to issue #17. The verdict model page lists the guarantees, the seven scenarios and the named limits.
The operating context
A terminal runs in one declared operating context: a network identifier and the commitment schemes it accepts, each scheme identifier carrying its version. The context is the terminal's policy, not something the provider declares, and the terminal's trusted keys are trusted only inside it. A selected point on another network, or a root under a scheme the context does not accept, is present and wrong evidence, so a terminal with a verifier configured refuses it at the selected point and never reports it as unverified. A terminal without a verifier consults nothing and reports every outcome, this one included, as unverified with reason no verifier. A publication from another network is ignored, never a veto: it cannot endorse a point on this network, and because the publication list is untrusted input it must not be able to block a selection either. That a signed message encodes its publication's point and root is a hypothesis, exactly as signature validity is; the concrete message encoding, and with it the encoding of network identifiers, belongs to issue #17.
| Decision | Alternative | Why |
|---|---|---|
| One context per terminal policy, scoping its trusted keys | Let the provider declare the network, or keep trust independent of the network | The terminal decides what it trusts; a provider's declaration is untrusted data |
| With a verifier configured, out of context is refused, never unverified | Report a mismatch as unverified | The evidence is present and wrong; a softer outcome would let a provider downgrade a refusal |
| A foreign publication is ignored | Refuse the whole selection when any fetched publication is on another network | One junk entry in an untrusted list would otherwise refuse every selection, and one key may honestly publish on two networks |
| Message binding is an assumed hypothesis | Compute it from a concrete message format now | The wire encoding is not yet agreed; the model states exactly what it needs from it |
The model covers network and scheme membership only. It does not cover genesis or era identity; concrete network identifiers belong to issue #17. It does not model protocol parameters: every use, including transaction construction, belongs to the implementation milestones. Validator script hashes belong to the implementation milestones. With no verifier configured an out-of-context selection is unverified with reason no verifier; the act step refuses every effect on it and allows construction only when the policy's action rule admits that reason. The operating context model section lists the guarantees, the five scenarios and the named limits.
The act step and settlement
As a terminal, build a transaction from a verified fact as soon as it is accepted, but drive an external effect only once the selected point is settled on the chain the terminal follows, and otherwise receive a refusal at the selected point.
The act step comes last, after the verdict, and follows one action rule. Construction needs a verified claim at the selected point, or an unverified reason that the terminal's policy admits for construction; in that case the offer acquired at the selected point is construction material, never evidence. An external effect needs a verified claim at the selected point, an offer bound to that point and the policy's settlement observation on the terminal's chain view. An effect on unverified data is always refused, including when no verifier is configured and the selected point is on another network. Every refusal is one of the three existing refusals and carries the selected point.
Settlement is a conditional guarantee. The settlement observation is executable. The continued-ancestry hypothesis says that a point the observation accepts stays canonical in every possible future that a consensus model admits. Neither the hypothesis nor the consensus model is computed, and no settlement depth is fixed. Under both, a successful effect keeps the selected point canonical in every admitted future. Without the consensus premise that statement is false on the real act step, because a settled point can be rolled back deeper than consensus admits.
A light terminal runs no chain follower. The chain view it uses is derived from accepted anchor publications: later points endorsed under the terminal's policy and context, which establish continued ancestry, as the external effects and settlement section of the architecture describes for later accepted publications. How that derivation is encoded and checked is an open contract owned by issue #17 and the implementation milestones. The settlement guarantee is therefore conditional on continued ancestry, on the consensus assumption, and on the view being the one those anchors attest.
Nothing a provider returns enters the chain view or the settlement observation. The act step reads the provider only through acquisition at the selected point, and the observation reads only the point and the view. So no provider, builder or publication can promote a point to settled, and nothing a third party fetches can veto settlement. A provider can still make its own effect fail, by withholding its offer or declaring it unbound; that is the provider's own availability, which is never trusted, not a veto over the terminal's evidence.
| Decision | Alternative | Why |
|---|---|---|
| The chain view is the terminal's own input, its faithfulness folded into continued ancestry | A separate view argument with its own faithfulness hypothesis | One hypothesis states what is needed; a second adds an argument to every statement and no executable distinction |
| An unsettled effect is refused as evidence failure | Refuse it as an unavailable point | The point is available; the evidence of continued ancestry is insufficient |
| Construction never reads the chain or the settlement observation | Refuse construction at a point no longer canonical | Construction is allowed at any accepted point and asserts nothing about finality; Cardano revalidates the transaction |
| A session is abandoned only from active | Also abandon an expired session | An expired or closed session already refuses its reads |
| Protocol parameters stay outside the model | Compute fees, sizes and parameter-dependent validity during construction | The model authorizes construction; the implementation milestones own the use of protocol parameters |
The limits are named. An unsettled effect and wrong evidence share the evidence-failure refusal, so a terminal cannot tell "not settled yet, retry later" from "wrong evidence" by the refusal alone; issue #11 may propose an outcome distinction, and issue #17 owns any wire reason code. The chain view is an input, the guarantee is conditional, and no depth or anchor count is chosen. Protocol parameters in transaction construction belong to the implementation milestones: the model computes no fees, sizes or parameter-dependent validity. The act model section lists the theorems, the five scenarios and the hypotheses.
Completeness proofs
As a terminal, learn every entry stored under a key prefix, or that the output carrying your asset is the only one, without trusting the asset's minting policy to be one-shot, and receive a refusal at the selected point when the listing is wrong.
Completeness is a proof kind beside the witness. A completeness answer carries a key prefix, every object stored under it as exact object bytes, and a proof; it travels inside the ledger answer offered at the selected point. The terminal checks it only under the root bound by root acceptance and only for a prefix it chose itself: the requested prefix for an all-entries claim, the policy's asset prefix for the state output. Provider roots and the answer's own prefix are data, never authority. CompletenessSound is an abstract hypothesis beside WitnessSound: a proof that checks under the honest root lists exactly the object bytes stored under the prefix at that point. The model computes it nowhere.
The key layout is an assumption, stated as a parameter. Today cardano-utxo-csmt indexes outputs by address, so an address prefix lists the outputs at an address. An asset prefix, which lists every output carrying an asset, needs the asset layout proposed in lambdasistemi/cardano-utxo-csmt#242, chosen by issue #35; AssetKeyLayout states that every output carrying the policy's asset is stored under its asset prefix. The model also assumes the completeness proof checks under the same accepted root as the witness; whether an asset index is committed under that root or a second anchored root, one root or several per publication, is open in issue #35. Nothing in the model bounds a listing, and a large prefix needs a large proof; pagination or summarised counts are issue #35's.
A terminal chooses between two guarantees for its state output, and the provider never chooses for it. A terminal that trusts the minting policy relies on OneShot when no completeness answer is offered. A terminal that does not requires completeness in its policy; an answer without it is then refused, and uniqueness rests on CompletenessSound, AssetKeyLayout and the encoding, observation and honest-root premises, not on OneShot, whatever the provider sends.
| Decision | Alternative | Why |
|---|---|---|
| The completeness answer travels in the ledger answer | A separate session field | It is acquired at the selected point under the existing no-substitution guarantee |
| Check under the accepted root and the terminal's own prefix | Check under the provider's root or the answer's prefix | A provider cannot endorse its own evidence or narrow the question |
| The key layout is a parameter | Fix the address or asset layout now | One statement covers today's address index and the proposed asset index |
| The policy can require completeness | Fall back to one-shot whenever the answer is absent | Untrusted input must not choose which hypothesis the terminal relies on |
| All-entries claims stop at acceptance | Add a verdict arm for them | A new verdict and reason are a wire and classification contract owned by issue #35 and issue #17 |
The completeness model section lists the theorems with their premises, the six scenarios, the seven mutants and the named limits. No CSMT proof format or key encoding is part of the model; those belong to issue #17 and haskell-mts.
Claims and evidence boundaries
| Design claim | Evidence boundary |
|---|---|
| Terminals verify data against independently accepted ledger roots | Executable root acceptance, session, ledger, application verification, verdict, operating context, act and completeness model with explicit verification and correspondence hypotheses; no full-system verifier or end-to-end deployment |
| Terminals accept application claims only through checked nested roots | The model proves claim soundness for the whole fold under honest-root correspondence, the ledger premises, application proof soundness and faithful nesting, and provider invariance under the same root, ledger and application proof premises plus functional application content; without functional content two builders can yield different accepted claims; no proof format, validator or implemented terminal |
| Terminals act only inside their declared operating context | The model proves that every accepted or verified claim is on the context network under an accepted scheme, that a mismatch is refused and never unverified with a verifier configured, and that appended foreign publications change nothing; context soundness assumes message binding; compiled mutants without the network guard or the scheme guard verify an out-of-context claim and refute the unchanged context soundness; one without the verdict's context branch reports an out-of-context unbound offer as unverified and breaks the never-unverified proof; removing the binding premise yields a statement that is false on the real verdict, while the unchanged statement rejects that counterexample, and no executable changes; no concrete network identifier, message encoding or implemented terminal |
| Terminals never present unverified data as verified | The model proves no promotion without hypotheses and soundness and provider invariance of verified claims under the acceptance premises; a compiled absent-witness mutant refutes both; no implemented terminal, verifier or witness format |
| Terminals drive external effects only from verified, settled facts | The model proves that an effect needs a verified claim at the selected point, an offer bound to that point and the settlement observation, that an effect on unverified data is always refused, and, under continued ancestry and the consensus premise, that the selected point stays canonical in every admitted future; a compiled mutant without the settlement guard authorizes an effect at an unsettled point and refutes the unchanged settlement stability through an admitted rollback; mutants allowing an unverified effect, removing the binding check or ignoring the action rule each break the unchanged proofs that constrain them and a scenario; removing the consensus premise yields a statement that is false on the real act step, while the unchanged statement rejects that counterexample, and no executable changes; no chain-view derivation, settlement depth or implemented terminal |
| Own anchors preserve trust independence; institutional publications reduce local infrastructure | These are trust and operating choices, not measured price rankings; no institution is claimed to participate today |
| Providers compete on computation and availability | No interoperable provider market or globally optimal pricing demonstrated |
| CSMT-UTXO supplies existing commitment machinery | Retained views, history coverage, leases and publication contracts require additional work; see existing projects |
| Ledger proofs authenticate their stated claims at a chainpoint | The ledger model proves unique-output/datum-root soundness under separate honest-root, witness, encoding, asset/datum and OneShot premises; membership alone does not establish uniqueness, completeness, canonicality or settlement |
| Terminals learn every entry under a prefix, and a unique state output without trusting the minting policy | The model proves that an accepted all-entries claim lists exactly the selected point's ledger entries under the requested prefix, under honest-root correspondence, CompletenessSound and faithful encoding; and that an accepted state output is the only output carrying the asset, with no OneShot premise, under CompletenessSound, AssetKeyLayout, faithful encoding, sound asset and datum observations and an honest accepted root, when a completeness answer is present or the policy requires one; with a verifier configured and a session bound to the selected point, an answer carrying a completeness answer is never unverified; compiled mutants that drop the completeness check, take the prefix from the answer, check under the provider root, drop the ledger completeness check, ignore the requirement or revert the classification each break the proofs the gate names and a scenario; removing CompletenessSound yields a statement that is false on the real acceptance; all-entries claims have no verdict arm, and no proof format, key encoding, listing bound or implemented index |
| Application services can reconstruct state and build proofs | Transaction-CBOR replay and dependency coverage still need application-specific evidence |
What remains unproved
- Anchor operating cost and the additional cost of ledger archives, retained views and proof-serving capacity need separate measurements.
- Provider switching, evidence interoperability and observable availability commitments need concrete contracts and acceptance evidence; market efficiency is a design thesis.
- The full commitment inventory: live UTxOs, asset sets and any historical indexes need separately stated proof guarantees.
- Completeness under a key prefix is modelled as a proof kind with an abstract
CompletenessSoundhypothesis and a key-layout parameter, for all entries under a requested prefix and for the unique state output. Still open: exclusion proofs and absence beyond an empty listing for a prefix; asset completeness in the index itself, which needs the asset layout of lambdasistemi/cardano-utxo-csmt#242 chosen by issue #35; whether that index is committed under the same root as the witness; a listing bound or pagination; a verdict for all-entries claims; and the proof format and key encoding, owned by issue #17 and haskell-mts. Inclusion proofs alone still do not establish a full result set. - Archive coverage must be selected before cost commitments; referenced-output retrieval must cover every dependency of a real application replay.
- The root model makes trusted-key membership and agreement explicit. Concrete anchor policy selection, key rotation, signed message encodings, freshness and rollback notices remain unspecified.
- A session whose selected block leaves the canonical branch of the terminal's chain view is abandoned, and its reads are refused at its own point. Bounded retention, leases and rollback notices on the wire remain unresolved.
- The ledger model binds the asset and exact witnessed-output datum to a selected-point accepted root under explicit assumptions. The application model binds the application, context, claim, point and nested roots abstractly; concrete proof formats, application replay and transition bindings still need their own contracts.
- Every application link is checked against one fixed query, and a session carries one ledger answer. Per-link queries are reviewed in issue #11; several ledger queries per session belong to later wire contracts.
- The invariance statement with the functional-content premise removed is copied by hand for its counterexample; its faithfulness is reviewed in issue #11.
- The verdict carries no payload; the act step takes construction material from the offer acquired at the selected point, never from the verdict. A witness offered on an unbound session is never checked, and a terminal without a verifier reports unverified even when nothing is offered. The verified soundness and invariance statements are hand copies of the acceptance statements, reviewed in issue #11.
- Settlement is modelled only as a guarantee conditional on continued ancestry and an abstract consensus model. How a light terminal derives its chain view from accepted anchor publications is an open contract owned by issue #17 and the implementation milestones, and no settlement depth or anchor count is chosen. Signatures or same-point anchor agreement alone do not establish settlement.
Evidence available today
The root acceptance, session, ledger, application verification, verdict, operating context, act and completeness model and simulator compile with a pinned Lean toolchain. Their proofs establish nonempty distinct trusted endorsement, exact point/root binding and selected-point refusal. Signature validity requires an explicit observation-soundness hypothesis; honest-ledger-root equality separately requires correspondence. Compiled counterexamples show untrusted-key refusal and failure of the general safety theorem after removing trusted-set checking. Session acquisition separately proves full-point no substitution for arbitrary providers and preserves the offered session unchanged; lifecycle scenarios show repeated reads, expiry refusal and release. A compiled production substitution mutation accepts a newer session and refutes the unchanged guarantee. Root trust is not established by acquisition. The ledger verifier checks the witness against the independently accepted root argument and binds the original object bytes to every asset and datum observation. Its universal proof identifies an honest member, actual asset, honest datum root and unique asset-bearing pair under separate selected-point correspondence, witness, encoding, interpretation and OneShot premises. Nontrivial honest fixtures inhabit all premises and acceptance together. A compiled provider-root substitution accepts an impostor and constructively refutes the unchanged guarantee; a two-member same-asset ledger refutes the complete unique-output guarantee when only OneShot is removed. All three ledger scenarios run through the real verifier. The application fold accepts a claim only after root acceptance, acquisition, ledger verification under the accepted root and every nested application link; the claimed root is compared before the proof is checked under the trusted root. Under honest-root correspondence, the ledger premises, application proof soundness and faithful nesting, its proofs show an accepted claim holds over the selected point's ledger; under the same root, ledger and application proof premises plus functional content, two providers and two builders cannot yield different claims. Compiled mutants that trust the claimed root or the session's root refute the unchanged soundness statement, and two values for one query refute invariance without the functional premise. The verdict layer classifies every outcome as verified, refused or unverified around that fold: a verified verdict requires a configured verifier, a session bound to the selected point, a present witness and acceptance's own claim, proved without hypotheses; unverified arises only from a declared absence; with a verifier configured, wrong evidence and misdeclared bindings are refused. A compiled mutant that lets an absent witness pass promotes an impostor and refutes the unchanged no-promotion and verified-soundness statements, and three further mutants each break an unchanged proof and a scenario. All seven verdict scenarios run through the real verdict and acceptance. The operating context guard refuses, at the selected point, a selected point on another network and a selected root under an unaccepted scheme, before acquisition and never as unverified with a verifier configured; appended publications from another network change nothing, and under observation soundness and message binding every verified claim is in context. Compiled mutants without the network guard or the scheme guard verify an out-of-context claim and refute the unchanged context soundness; a mutant without the verdict's context branch reports an out-of-context unbound offer as unverified and breaks the unchanged never-unverified proof. Removing the message-binding premise changes no executable: the statement without it is false on the real verdict, the unchanged statement rejects that counterexample, and its unchanged proof fails once the premise is gone. All five context scenarios run through the real verdict and acceptance. The act step authorizes construction on a verified claim at the selected point, or on an unverified reason the policy's action rule admits, and an external effect only on a verified claim with an offer bound to the selected point and the policy's settlement observation; an effect on unverified data is always refused, and every refusal carries the selected point. Under continued ancestry and the consensus premise, a successful effect keeps the selected point canonical in every admitted possible future, and a fixture inhabits both hypotheses together with a settled effect and an unsettled tip. A compiled mutant without the settlement guard authorizes an effect at the unsettled tip and refutes the unchanged settlement stability through an admitted rollback; mutants allowing an unverified effect, removing the binding check or ignoring the action rule each break unchanged proofs and a scenario; the statement without the consensus premise is false on the real act step, and the unchanged statement rejects that counterexample. A session whose selected block is rolled back is abandoned, with its reads refused at its own point. All five act scenarios run through the real verdict and act step. A completeness answer is checked under the accepted root and for the terminal's own prefix only. Under honest-root correspondence, CompletenessSound and faithful encoding, an accepted all-entries claim lists exactly the selected point's ledger entries under the requested prefix; under CompletenessSound, AssetKeyLayout, faithful encoding, sound asset and datum observations and an honest accepted root, an accepted state output with a completeness answer present or required is the only output carrying the asset, with no OneShot premise. With a verifier configured and a session bound to the selected point, an answer carrying a completeness answer is never unverified; with root acceptance succeeding, a wrong one, or a witnessed answer missing a completeness answer the policy requires, is refused at the selected point. A fixture inhabits every premise of these statements together; seven compiled mutants each break the proofs the gate names, the six executable ones also a scenario, and the statement without CompletenessSound is false on the real acceptance. All six completeness scenarios run through the real acceptance, ledger step and verdict. Lease and retention policy remain open. This is model evidence; independent acceptance, remote CI, implementation and deployment need their own revision-bound results.
MPFS's facts verifier already anchors a state output and checks the root reconstructed from returned facts. It is useful prior implementation, not evidence that the proposed transaction-retrieval architecture is delivered.
The inspected Koios asset query and Blockfrost API do not expose the required shared chainpoint session contract for the relevant UTxO queries. This is a finding about those published interfaces, not their internal database capabilities.
CSMT root-signing work is related work. Its existence does not establish an accepted anchor publication protocol.