Powered by OpenAIRE graph
Found an issue? Give us feedback
ZENODOarrow_drop_down
ZENODO
Article . 2026
License: CC BY
Data sources: Datacite
ZENODO
Article . 2026
License: CC BY
Data sources: Datacite
addClaim

Correct but Unauditable: Boundary Evidence in Distributed Hosts

Authors: Simas, Tristan;

Correct but Unauditable: Boundary Evidence in Distributed Hosts

Abstract

A controlled timestamp-only projection of an ABD-style multiwriter quorum-register tag leaves completed reads current, exact, and linearizable while omitting the writer-identity component of the full protocol tag. Correctness therefore does not imply auditability at a distributed read boundary. A deterministic five-state host gives the protocol-independent companion: four sequential operations are totally ordered in real time, yet the read boundary exposes no source evidence. For an external specification fixed before the realization is chosen, zero-error boundary recovery exists exactly when all co-encoding locations agree and native source evidence aligns with the specified source and derivation relation. Under edit-generated source semantics, boundary agreement is equivalent to temporal zero-delay synchronization. Disjoint audited systems compose, but two independently verified services can assign incompatible roles to one shared location. Value projection likewise fails to preserve auditability; a certified refinement law transports it. A CAP partition carrier induces the corresponding read-boundary discriminator, but carrier data alone cannot supply the scheduler continuations required for an FLP transport. Finite DLS histories yield an exact stabilization-certificate bound and exclude one fixed evidence budget across all horizons. Protocol and replicated-storage rows illustrate the criterion across distributed boundaries. The substrate-independent ledger records the broader scope. Lean 4 verifies the finite models, reductions, abstraction maps, and internal bounds; the premises linking named systems to those models remain documentary.

Keywords

distributed systems, formal methods, language design, Single Source of Truth, encoding systems

  • BIP!
    Impact byBIP!
    selected citations
    These citations are derived from selected sources.
    This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    0
    popularity
    This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
    Average
    influence
    This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
    Average
    impulse
    This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
    Average
Powered by OpenAIRE graph
Found an issue? Give us feedback
selected citations
These citations are derived from selected sources.
This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Citations provided by BIP!
popularity
This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.
BIP!Popularity provided by BIP!
influence
This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).
BIP!Influence provided by BIP!
impulse
This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.
BIP!Impulse provided by BIP!
0
Average
Average
Average
Upload OA version
Are you the author of this publication? Upload your Open Access version to Zenodo!
It’s fast and easy, just two clicks!