jonnify·bcs /bcs/elixir-core/property-stores/chronology-without-a-column

B2.2 · dive 2 — chronology without a column

The order theorem as a read path.

Three hundred ORD mints across real wall time; the newest five by byte order equal the last five minted, and a half-open window [lo, hi) built from two synthetic cursors returns 100 of 100 expected, ascending by key. No timestamp column. No sort call.

Source: content/bcs2.2.md, quoting bcs_rung_2_2_check.out (lines P3, P4); the select runs in property_store.ex, grown by window/3.

The tail walk — a model. Twelve mints across four minutes (the rung's own run minted three hundred). Each instant is encoded into a real ORD id by the contract's arithmetic; choose n and read the newest page.
114:29:12 214:29:48 314:30:02 414:30:15 514:30:31 614:30:59 714:31:08 814:31:26 914:31:44 1014:31:58 1114:32:21 1214:32:47
readout · Choose a page size. The walk starts at :ets.last and steps :ets.prev; the keys it returns are compared as bytes, and the newest n by byte order equal the last n minted — no timestamp consulted. The rung's own gate did this over three hundred mints and five.
§1

The transcript

bcs_rung_2_2_check.out · lines P3–P4 · verbatim
content/echo_data/runtimes/elixir/bcs_rung_2_2_check.out · lines P3–P4frozen
P3 order ok -- newest five by byte order equal the last five minted: no timestamp column consulted
P4 window ok -- window [tA,tB) by synthetic cursors returned 100 of 100 expected, ascending by key

P3: three hundred ORD mints spread across real wall time, then the newest five — page_desc/2 walking the table tail, the order theorem as a read path. P4 is the chapter's center: two wall-clock instants captured mid-mint, two synthetic cursors built by the same min_for arithmetic every runtime shares (Chapter 1.5), and the new window/3 answering — exactly the mints between the instants, by construction and by gate.

§2

The match spec

property_store.ex · verbatim 
def handle_call({:window, lo, hi}, _from, s) do
  with {:ok, _} <- EchoData.Bcs.gate(lo, s.ns),
       {:ok, _} <- EchoData.Bcs.gate(hi, s.ns) do
    spec = [{{:"$1", :_}, [{:>=, :"$1", {:const, lo}}, {:<, :"$1", {:const, hi}}], [:"$1"]}]
    {:reply, {:ok, :ets.select(s.table, spec)}, s}
  else
    {:error, _} = err -> {:reply, err, s}
  end
end

Both bounds pass through the gate first — window bounds are ingress, and a bound in the wrong namespace is refused before the table is touched. Term order over binaries is byte order, so the theorem does the sorting and the guards do the cutting; the result order is the table's, not a sort call's.

Correctness is gated; range cost is not — :ets.select with comparison guards is not promised to seek to the lower bound, so very large tables earn a seeded :ets.next/2 walk from lo as the optimization lane, carried as a follow-up rather than smuggled into this rung.

§3

The window, exercised

a model over the same twelve mints

Pick a half-open window over the same twelve model mints. The two cursors are synthesized by min_for — the floor id of the instant, node 0, seq 0 — and the membership test is two byte comparisons per key: lo <= key < hi. The rung's own gate did this with two instants captured mid-mint and read back 100 of 100 expected, ascending by key.

The window selector. Select a window; the readout prints both synthesized cursors and the keys in range.
114:29:12 214:29:48 314:30:02 414:30:15 514:30:31 614:30:59 714:31:08 814:31:26 914:31:44 1014:31:58 1114:32:21 1214:32:47
readout · Select a window. Static results over the model: [14:30, 14:32) → 8 of 12; [14:29, 14:30) → 2 of 12 — the half-open right end excludes the 14:30 floor itself; [14:31, 14:33) → 6 of 12; [14:31, 14:31) → 0 — [lo, lo) is empty by construction.
§4

The Go counterpart

content/bcs2.2.md · How · verbatim

The owner goroutine from Chapter 1.1 keeps its keys in a sorted slice, and the window is two binary searches and a copy — the same cursor arithmetic shared from Chapter 1.5:

lo := brandedid.MustEncode("ORD", minFor(t0))
hi := brandedid.MustEncode("ORD", minFor(t1))
i := sort.SearchStrings(keys, lo)
j := sort.SearchStrings(keys, hi)
window := append([]string(nil), keys[i:j]...) // [lo, hi), ascending

Same grammar, same bytes, same half-open contract on both sides of the bus.

§5

References

sources · related

Sources

Related