FrogNet Memory · the contract, first draft

What the memory promises. Marked honestly.

Written from the source, not from intent. Every clause is marked verified, implied, or undetermined, and nothing is filled in with something plausible — a contract needs a commitment, and code only has a behaviour. Three clauses were carried as undetermined for a while and are now settled, because the question each of them asked turned out to presuppose two values under one description. There is one. What remains open is one decision, about absence, and it is marked where it lives. Turning behaviour into a specification is a spec-editor's job →

Vocabulary rule: values, names, services, scopes, authority, observations, invariants — never hosts, senders, or receivers. The consequences of distance are in the contract; the mechanism of distance is not.

§01What is settled

Identity, observation, absence, departure.

verified

A value is identified by (service, var, scope) — and nothing else

No part of that identity names a machine. The writer's address is envelope data on the row: not part of the identity, not supplied by the caller, not required to read. The write is an upsert by name — a write under a description that already exists replaces the value there. Two executions writing under one description are not two messages to reconcile; they are writes to the same location, and the second replaces the first.

verified

get() observes the current value, subject to freshness — on the store's own clock

Freshness is judged on the row's update time, never on a timestamp inside the value. This is load-bearing and was learned expensively: when freshness compared a reader's clock against a writer's stamp, a machine two minutes slow vanished from every roster while publishing correctly, and the only symptom was an empty result. fresh_s=0 means no filter: observe the value whatever its age.

verifiedone decision open

Absence has three causes, and get() does not distinguish them

Never written; written and aged past fresh_s; not observable from here at this moment. A caller can separate the second from the others with fresh_s=0, and has no supported means to separate the first from the third. Whether that distinction should exist is the first thing the contract has to decide — a program that behaves differently depending on why a value is absent has reintroduced the topology; an application with a safety invariant must be able to tell "no reading" from "no contact". Both arguments are real.

verified

Ceasing to assert is how a thing leaves

A value ceases to be observable when nothing re-asserts it inside the freshness window the reader asks for. No delete must arrive; no reaper must run. Crashing is the same thing, slower — there is no cleanup path a failure can skip. A process may register its own writes for removal on exit (the courtesy, not the mechanism); own=False exists for writes that must outlive their writer and age out instead.

§02Ordering, authority, reunion

One value, so nothing to arbitrate.

These three were carried as open questions for a while, and they turned out to be the same question asked three ways. Each presupposes two values under one description. There is one store per connected network, one serialization point, one order — so the second value never exists, and the arbitration never has to happen.

verified

Which write won

Last write wins. The write is an upsert and the later write under a description replaces the earlier one, ordered at the one serialization point every write in the network arrives at. That is the contract, not merely the current behaviour.

What follows from it is stated rather than hidden: there is no ordering guarantee between writes that arrive concurrently from different places, and an application holding an invariant across two values has to maintain it itself. When a problem genuinely requires an order, elect for order and route the decision through the elected role — do not ask the shared picture to pretend it is one.

verified

Authority — there is none, and there cannot be

The question which value survives when two exist under one description presupposes two stores. There is one. A connected FrogNet has a single storage location for the whole tuple space and a single serialization point, kept singular by a deterministic election — so a description holds a value, never a field of candidates for something to choose between.

So there is no authority rule, no per-scope or per-value authority, and no such thing as a write made without authority. Not an unwritten rule — an absent one. Nothing arbitrates because nothing is ever presented with two answers.

verified

When part of the fabric cannot exchange state

Within a region that can still exchange state, values written there are observable there under the ordinary rules. Values last written elsewhere remain observable until they age past the reader’s freshness window — at which point they cease to be observable rather than becoming wrong.

On reunion, nothing merges. Each region elected its own host and held its own store; memory is not migrated and not reconciled, and there is no history to replay. Values do not travel with a node — rejoin a wider network and your writes land on its host; leave again and you are reading your own store once more. So two fresh values never meet under one description, and the reconciliation everyone expects to find here does not exist to be specified. The rule for a node whose world just changed shape is one line: write before you read. How the regions find each other again is the fabric’s business, not the contract’s.

§03Stated plainly

What the contract does not provide.

No transaction across two or more values. No single-writer region enforced by the substrate. No ordering guarantee between values under different descriptions. No consensus. And no authority primitive, because with one store there is never a second value for an authority to rule on.

An application needing any of these builds it, on top, using the memory. That is a supported thing to do, and the contract should stop pretending the question does not arise.

Three of these clauses — absence, ordering, authority — are the strongest argument for the spec-editor seat: everything else in the four planned documents is extraction, and these three are authorship. If you want to argue with a clause, bring an oracle — a demonstration that fails on the current code is how a decision gets made here.