hydo-assert: the Python assertion SDK

A Python program running under hydo (the deterministic hypervisor of github.com/kakoc/hydo) uses this package to say what must be true and what should happen at least once. It writes the same console records as the Go SDK (sdk/go), byte for byte, with the same deduplication rules, so hydo run and the explorer (hydo explore) read them unchanged. The wire format and the verdict rules are in hydo/ASSERTIONS.md of that repository; paths below are relative to it.

• Distribution name hydo-assert, import name hydo_assert.
• Standard library only; Python 3.8 or later; thread-safe and safe to call from asyncio code.
• Install it from PyPI (pip install hydo-assert), or from a checkout (pip install ./sdk/python), or put sdk/python/src on PYTHONPATH, or copy src/hydo_assert/ into the guest image (the hydo/onboard/examples/python-kv example does that).

Use

import hydo_assert as ha

# Declare at module level: the catalog is complete once the module is imported.
ACKED = ha.always("kv.acked_durable", "every acknowledged PUT reads back with its value")
PARSES = ha.always_or_unreachable("kv.log_parses", "every complete log line parses on replay")
SIZE = ha.always("kv.log_size", "the log holds at most 10000 entries")
REPLAYED = ha.sometimes("kv.recovered", "the server replayed a non-empty log at start")
TORN = ha.reachable("kv.torn_tail", "the log ended in a partial line")
BAD = ha.unreachable("kv.bad_command", "the server got a command it does not know")
BACK = ha.eventually("kv.back", "the server answers within 5 s", 5.0)        # seconds or timedelta
LOST = ha.buggify("kv.put.lost_reply", "the PUT is logged but its reply is lost")

ha.catalog()                                       # once, early: the HYDO-ASSERT-DECL lines
ACKED.check(got == want, {"key": k, "got": got})   # returns bool(cond)
REPLAYED.check(n > 0, {"entries": n})
TORN.hit({"bytes": len(tail)})
BAD.hit()
SIZE.cmp(n, "<=", 10000)                           # details: left, op, right
if LOST.fire({"key": k}):                          # BUGGIFY fault point
    return
BACK.await_cond(lambda: ping() == "PONG", poll=0.2)   # blocks; one record
w = BACK.begin(); ...; w.done()                    # or: anchor now, condition true now / w.expire()
ha.setup_complete()                                # HYDO-SETUP-COMPLETE

In asyncio code use await BACK.await_async(cond, poll): cond may be a plain function or an async def, and the wait between checks is asyncio.sleep. Every other call is a short write to the console under one process-wide lock that is never held across a blocking call or an await, so it is safe from coroutines and from threads.

The naming follows the other SDKs (sdk/js, sdk/rust): the Go names in Python's snake case, and await_cond / await_async for Go's Await. That table, Liveness, Watch and Point (the classes the calls return) and the history recorder below are the whole API: a comparison has one form, cmp with its operator, and names that start with _ (the modules _core, _buggify, _eventually, _json, _sink) are the package's own.

Records, deduplication, catalog

• Records go to /dev/ttyS0 (opened once, O_WRONLY|O_APPEND|O_NOCTTY, one write per record). HYDO_ASSERT_OUT=<path> writes to that existing file, stderr to standard error (plain logging outside hydo), off nowhere, and logging (Python only) logs each record line at INFO on the logger hydo_assert. If the file cannot be opened, standard error is used.
• A process writes each (assertion, outcome) pair once: the first pass and the first failure, with the details of that evaluation. A sometimes that evaluated false is never written. unreachable is written with ok:false. A record whose details hold a NaN or an infinity is not written at all, but still counts as written (as in Go, where json.Marshal fails after the pair was marked).
• The catalog (catalog()) lists every declared assertion in declaration order: the order in which the declaring statements ran, which for module-level declarations is the import order. A module that is never imported contributes nothing; import it before calling catalog(). Call catalog() in the process whose console output is collected for each run (for a server started before the explorer's snapshot point, that is a client or the oracle, not the server; see the example).
• Details are encoded exactly as Go's encoding/json encodes the equivalent Go value: keys in UTF-8 byte order, <, >, &, U+2028 and U+2029 escaped, other non-ASCII text raw, Go's float format (1e+21, 1.5e-7, 3 for 3.0, -0). The caller's dict is never changed (Go adds left/op/right, hit, elapsed_ms to the caller's map; Python adds them to a copy, which gives the same record).
• Python values Go has no form for: a tuple is an array; bytes is a base64 string (as Go encodes []byte); a set is an array sorted by encoded element; integer dict keys are written in decimal; any other object is the string str(obj). A lone surrogate (an undecodable byte read with surrogateescape) is written as \ufffd, as the pinned guest Go 1.26.5 writes an invalid UTF-8 byte (Go 1.27 writes a raw U+FFFD instead).
• details that is not a mapping is wrapped as {"value": details}.
• After os.fork() the child keeps the parent's deduplication state (it is one program's history) and gets fresh locks.

BUGGIFY

Same decisions as the Go SDK: configured by $HYDO_BUGGIFY, or else the file $HYDO_BUGGIFY_FILE (default /tmp/hydo-buggify), holding <seed-hex>[,<enable-permille>[,<fire-permille>]] (defaults 250 and 250, FoundationDB's values), parsed as Go's strconv.ParseUint does (no 0x, no sign, no spaces inside a field; an unparsable seed leaves BUGGIFY off, an unparsable permille keeps its default). It is read once, at the first evaluation of any point, which also writes HYDO-BUGGIFY {"seed":..,"enable_pm":..,"fire_pm":..,"enabled":[..]}. A point is enabled for the run when splitmix64(seed ^ fnv1a(id)) % 1000 < enable; its k-th evaluation fires when splitmix64(splitmix64(seed ^ fnv1a(id)) + k·0x9e3779b97f4a7c15) % 1000 < fire. Each point is also a sometimes property buggify.<id> ("fault point fired: "), recorded at its first firing with {"hit": k}. Without a configuration every point returns False and has no other effect. Under hydo the schedule token B=<seed> (hydo explore --buggify) reaches the file through the guest init: an onboarded project gets it with buggify: true in its hydo.yaml (hydo/onboard/MANIFEST.md).

History recorder

The module hydo_assert.history records operation histories for hydo's host-side checkers (linearizability of a register or compare-and-set object per key, and Elle-style list-append; the format and the checkers are in hydo/HISTORIES.md). It writes the same HYDO-HIST lines as the Go recorder (sdk/go/hydohist), byte for byte except the time field. It is a separate module: import hydo_assert does not load it, so the assertion records are unchanged.

from hydo_assert import history as hh

kv = hh.History("kv")
op = kv.invoke(3, "write", "k1", hh.enc(v))      # process 3, before the request
try:
    rev = put("k1", v)
    op.ok("k1", hh.ver(v, rev))                  # the version the store assigned, if any
except Rejected:
    op.fail()                                    # it definitely had no effect
except Exception:
    op.info()                                    # a timeout: the outcome is unknown
kv.invoke(3, "read", "k1").ok("k1", hh.value_or_nil(get("k1")))   # None means absent

la = hh.History("la")
tx = la.invoke(4, "txn", hh.append_mop("x", "1"), hh.read_mop("y"))
tx.ok(hh.append_mop("x", "1"), hh.read_result_mop("y", "1", "2"))

• list_value has a longer name than Go's List so that it does not hide the builtin list for a program that uses from hydo_assert.history import *. The micro-op helpers have the Rust SDK's names.
• A process is an int or a token without spaces. Arguments are tokens: a str is written as it is (encode free-form values with enc), an int is written in decimal, and bytes are written as they are. Versions are int64 values; a value outside that range raises ValueError, and a value that is not an int (including bool) raises TypeError.
• Records go to /dev/console. HYDO_HIST_OUT=<path> appends to that file and creates it if it is missing (mode 0644), stderr writes to standard error, and off writes nothing. If the file cannot be opened, standard error is used. The setting is read once, at the first record, and is separate from HYDO_ASSERT_OUT.
• Each record is one os.write call made under a lock, so threads never interleave lines. The time field is time.monotonic_ns() (CLOCK_MONOTONIC on Linux, deterministic under hydo). It is read under the lock, so the times of successive lines never decrease; Go reads it just before its lock, and the line format is the same. A forked child gets a new lock and keeps the descriptor.
• Text is written as UTF-8. A str is encoded with the surrogateescape rule, so a string that came from bytes that way (os.fsdecode, sys.argv, os.environ, or enc of bytes) gives back its original bytes. Any other lone surrogate is written as U+FFFD. enc of bytes keeps invalid UTF-8 bytes as they are, as Go's Enc does, and returns them as surrogateescape characters.
• A process has at most one operation in flight: give each concurrent client (thread or task) its own process number. Record the invocation before sending the request and the completion after the reply, because the checkers order operations by the position of their records.

Determinism

The records are a pure function of the program's evaluation sequence: no clocks (except the guest's monotonic clock for eventually, which hvx makes deterministic), no host state, catalog in declaration order, sorted keys. A Python program is itself deterministic under hydo: the guest CRNG is seeded identically every run, so even the hash seed is the same; setting PYTHONHASHSEED=0 makes that independent of the CRNG. PYTHONDONTWRITEBYTECODE=1 avoids writing .pyc files on the guest's read-only root.

Tests

• python3 -m unittest discover -s sdk/python/tests: the encoder (Go's float and string forms), deduplication, details not mutated, NaN, catalog order, 16 threads writing 2000 evaluations each without an interleaved line, asyncio eventually, fork, BUGGIFY decisions and rates. Passes on Python 3.8.20 and 3.15.0.
• tests/test_cases.py (run by the same unittest command): the shared cases (sdk/cases, written by the reference SDK, sdk/rust; format and rules in sdk/rust/README.md, "The shared cases"). For every case and run it starts itself as a child process, makes the case's calls with this package and hydo_assert.history, and compares the bytes the sink received and the calls' results with the case's files: every assertion type, comparisons, details with tricky values (invalid UTF-8 as surrogateescape characters), the catalog, eventually, BUGGIFY under 18 configurations, HYDO_ASSERT_OUT, and the history records with every helper and HYDO_HIST_OUT setting. Cases that need a float32 (f32) are skipped and listed. To add a case, add it to the Rust SDK's tests/cases/defs.rs and run HYDO_BLESS=1 cargo test --test cases there; this test then runs it. A format change starts in the Rust SDK too: after it is blessed, this test fails on the lines this package must change. No other language is needed to run it. Passes on Python 3.8.20 and 3.15.0.
• tests/test_history.py (run by the same unittest command): the exact lines of the Go recorder's own unit test, the encoding of every byte class, the argument checks, the sink settings, one os.write per record, 8 threads writing 400 records each without an interleaved line, and fork.
• The files of src/hydo_assert/ are copied into the python-kv example's images, so a change to any of them changes those images' bytes and every python-kv fingerprint (the last such change, a reworded comment in _core.py, re-recorded them in milestone 157; docs/REBASELINE.md has the values).

Limits

• No call-site form that registers itself before it runs (the Rust SDK's macros do that with a linker section). A Python assertion is in the catalog once the statement that declares it has run, so declare at module level.
• cmp compares any two Python values that support the operator; values that cannot be compared evaluate to false. Go's Cmp takes only int64.