blog.ganska.latRSS

One declaration, two languages: making a silent no-op a build error

Fifteen automations run on one Fairphone, in place of Tasker. An arriving SMS is mirrored to a private ntfy topic and shown as a notification, and a message whose body contains the word locate is answered with the zone the phone is currently in. Crossing the geofence around home announces it. Three daily alarms fire at 07:00, 08:30 and 20:00, and the middle one only reminds anyone to leave if the phone is still at home when it goes off. A walk, detected by the handset’s own motion sensors rather than by polling GPS, switches the system location setting on, holds a fix open and starts a GPSLogger track, then switches all three back off once the phone has been still for ninety seconds.

None of that is written in a GUI. Every rule is typed Python, compiled to a validated JSON artifact, baked into an unsigned APK by Nix, then signed and installed by a CLI. The phone decides locally; the fleet is reachable but never required. Tasker’s UI-automation tier, driving other apps’ screens through an accessibility service, is deliberately out of scope.

The primitive everything else composes from is this: every trigger, action and condition operator is declared exactly once, in Python, and every place the Kotlin side needs a branch for it is generated from that declaration into a when with no else. A name that exists on one side and not the other is not a rule that quietly never fires. It is a compiler error.

One real dispatch, from the phone’s own trace file, when a message reading Locate arrived while the phone was inside the home geofence:

seq 9-3  state={"location.zone":"home"}  body=Locate
  sms-locate          MATCHED -> ntfy "fairphone is at home" => posting to 'phones'
  sms-locate-unknown  skipped (location.zone: expected {exists: false}, got "home")

Both rules are triggered by the same message and split on whether the phone’s zone is known, so exactly one of them can fire. And the other half of the primitive, the output of adding one string to a seven-element Python tuple and rebuilding:

src/Match.kt:93:78: error: 'when' expression must be exhaustive. Add the 'regex' branch or an 'else' branch.

Component versions

The behaviour described here was observed with these:

Component Version Where the number comes from
Artifact schema 2 VERSION = 2 in the compiler; SUPPORTED_VERSION = 2L in the Kotlin parser
Android build-tools 35.0.0 buildToolsVersion in the APK derivation
Android platform 35 platformVersion = "35" in the APK derivation, source of android.jar
Android cmdline-tools 13.0 cmdLineToolsVersion in the APK derivation
minSdkVersion 30 the manifest
targetSdkVersion 36 the manifest
d8 minimum API 30 d8 --min-api 30
nixpkgs 2fcb964de67fcf60b43471c55d5d99e61a9ccb5a the flake lockfile
Ruff target py312 target-version in the project file
mypy target Python 3.12 python_version in the project file

Three numbers are absent, because they cannot be read from a file. The JDK and Kotlin compiler enter both derivations as bare nixpkgs attributes (pkgs.jdk, pkgs.kotlin, and pkgs.jdk21 for the APK), so the exact releases are whatever the pinned nixpkgs revision holds. There is no compileSdk attribute anywhere; the compile target is implied by the android.jar passed to aapt2 and kotlinc.

The vocabulary, and the fifteen rules built from it

The whole system’s expressive power is six triggers, six actions and two declared states. That is the entire surface an author writes against.

Trigger Delivery Fires when Selector Permissions
sms.onReceived cold any inbound SMS arrives none RECEIVE_SMS
location.onEnter pendingIntent the phone crosses into a declared zone zone FINE and BACKGROUND location
location.onExit pendingIntent the phone crosses out of one zone FINE and BACKGROUND location
time.at alarm a daily wall-clock HH:MM comes round when USE_EXACT_ALARM
motion.onSteps fgs a walking burst passes a step count a rule named threshold ACTIVITY_RECOGNITION
motion.onStill fgs the walk is called over none none

Each declares its event fields and their types, and those field names are the only things a condition or a placeholder may name. An SMS event carries from, body, timestamp, subscriptionId and slot. A motion event carries threshold, steps, cadence and since. A location event carries zone and timestamp and deliberately no coordinates, because a zone name is the honest answer to “where is this phone” and a latitude is more than the geofence actually knows.

The six actions: notify posts a local notification, ntfy POSTs to a private ntfy server, requestLocation and releaseLocation open and close a bounded location request, setLocationEnabled writes the system-wide location setting through a secure-settings grant, and startGpsLogger broadcasts a start or stop to a separate track-logging app.

Two more actions exist in the source and are deliberately not exported from the package. Importing a module runs its decorator and registers it, and a registered action with no runtime branch used to compile, validate, simulate and then silently drop on the phone. They get re-exported in the same commit that adds their Kotlin branch, not before, because from that moment the generated enum makes the APK refuse to build until the branch exists.

One state is declared and referenced: location.zone, a string folded out of the two geofence triggers, set on enter and cleared on exit. A second, motion.walking, is declared in the vocabulary and named by no current rule, so it does not appear in the compiled artifact at all.

The fifteen rules those pieces build, as they run today:

Rule Trigger Condition Does
sms-to-fleet any SMS none ntfy the sender and body to the fleet
sms-notify any SMS none local notification
sms-at-home any SMS zone is home notification titled with the zone
sms-from-known any SMS sender is one specific number notification, and the sender filter’s live proof
sms-locate any SMS body contains locate, zone known ntfy the zone back
sms-locate-unknown any SMS body contains locate, zone unknown ntfy that the position is unknown
parcel-notice any SMS sender in a list of four carriers ntfy the body
arriving-home enter home none ntfy the fleet
leaving-home exit home none local notification
morning-briefing 07:00 none notification
leaving-soon 08:30 zone is home notification
medicine 20:00 none ntfy at priority 5
gps-when-walking 35 steps cadence between 40 and 180 per minute location on, hold a GPS fix, start the track
gps-when-still walk ended the burst reached 35 steps release the hold, stop the track, location off
stop-tracking-at-home enter home none the same three, whatever the steps say

Three things in that table are the design rather than the content. The locate pair is split into two rules on whether the zone is known, rather than written as one rule with an optional value, because an unresolved placeholder is left in the text verbatim and “the phone is at ${location.zone}” is the wrong thing to send someone who is looking for it. Tracking is switched on by one rule and off by two, and the asymmetry is deliberate: walking is the only reason to start, while standing still and arriving somewhere known are both reasons to stop, so a failure of either stop path is covered by the other. And gps-when-walking gates on cadence rather than on steps alone, because significant motion fires for a handset picked up off a desk, and 35 steps of pottering about a flat is otherwise indistinguishable from the start of a walk.

Data flow

One rule, followed from the file a human edits to the notification on the screen. The rule is an SMS automation predicated on a state that no SMS carries:

    Automation(
        name="sms-at-home",
        description="Notify differently for an SMS arriving while the phone is at home",
        mode="parallel",
        # location.zone is a state, not a field of sms.onReceived: it is folded
        # from the geofence crossings and survives process death. Until the
        # first crossing after a reboot it is unknown and this rule skips
        # saying so, which is why the two rules above stay unconditional.
        condition={"location": {"zone": "home"}},
        trigger=sms.on_received(),
        action=[notify(title="SMS at ${location.zone}", body="${sms.body}")],
    ),

The build pipeline: the device files, the registry and the operator tuple feed validation and then compilation into one artifact; the registry and the operator tuple separately render the two generated Kotlin enums, the artifact generates the manifest blocks, kotlinc combines the engine, the generated enums and the app sources into the APK, and the artifact and the engine jar feed the simulate and coverage gates.

The build verb resolves the device to a package path, imports it, and hands the resulting DeviceConfig to build, which calls check before anything else. The import is load-bearing: the registry dictionaries are module-level globals populated as a side effect of importing the device’s modules, so nothing exists to validate against until the device file has been executed.

check returns a list of strings rather than raising, so a device file with four mistakes reports four. build then computes the artifact, render serialises it with sort_keys=True and a trailing newline, and the result is a JSON document with a version field the Kotlin parser refuses to read if it disagrees.

Nix takes that document three ways at once. The compiler is invoked a second time to render the registry as Kotlin enums, a third time to render the operator tuple as another Kotlin enum, and jq reads the artifact’s permissions and queries arrays out of the copy already baked into the APK’s assets to generate two blocks of manifest XML. One kotlinc invocation then compiles the engine sources, the generated enums and the app sources together.

On the phone, the manifest receiver builds an Event carrying exactly the field names the trigger declared, Dispatcher folds the state forward before matching, matchAutomation checks the trigger argument against the selector and then walks the condition, ActionRunner dispatches on the generated ActionName, and every dispatch is appended to a trace file synchronously. For sms-at-home, location.zone is read from the persisted state map rather than from the event, ${location.zone} interpolates from the same map, and if nothing has set it since the process started, the rule skips with not known yet, nothing has set it since this process started rather than with a comparison failure.

What runs on the handset

Twenty-one Kotlin files make up the app side, and none of them contains a rule. They are the adapters between Android’s delivery mechanisms and the engine, plus the arming table and the three subsystems it drives.

The runtime: a boot or a package replace starts the foreground service, which arms geofences, alarms and sensors; each of those and the SMS receiver produce an Event, which the dispatcher folds state into, matches, runs actions for, and traces.

A persistent foreground service of type specialUse is the arming point and the sensor holder. It is started when the launcher activity opens, and after a reboot or a package replacement by a receiver that takes exactly those two broadcasts. Arming is one exhaustive branch per trigger key:

        for (key in keys) {
            when (triggerKeyOf(key)) {
                TriggerKey.sms_onReceived -> {
                    // A manifest receiver the system starts for us. Nothing to
                    // arm, and that is a decision recorded rather than an
                    // omission.
                }
                TriggerKey.location_onEnter, TriggerKey.location_onExit -> {
                    if (!armedGeofences) {
                        Geofences.register(context)
                        armedGeofences = true
                    }
                }
                TriggerKey.time_at -> {
                    if (!armedAlarms) {
                        Alarms.schedule(context)
                        armedAlarms = true
                    }
                }

The loop iterates the artifact’s trigger table, not the automations’ trigger keys, which is what arms a trigger that exists only to maintain a state some rule reads. Each of the four delivery tiers behaves differently under process death, and that is the substance of the section. An SMS is a manifest receiver, so the system cold-starts the process to deliver it and there is nothing to arm; the empty branch is a decision recorded rather than an omission. A geofence is an AOSP proximity alert holding a PendingIntent, registered once per referenced zone with no expiry. An alarm is one exact alarm per distinct HH:MM, rescheduled before the dispatch rather than after it, and recomputed from the wall-clock string on every fire so it stays correct across a daylight-saving change. Sensors are the odd tier: the service holds them open, nothing survives the process, so they re-arm on every start rather than only after a reboot.

The movement chain is the most involved part of the runtime and the one that is cheapest to leave switched on. A walk is bracketed by two hardware one-shot sensors and measured by a third in between. Significant motion opens the burst, stationary detect closes it, and a batched step counter counts. Only the counter costs a permission, and the counting happens in the sensor hub rather than on the application processor, so standing still costs one armed hardware trigger and no application-processor time at all. The batch latency is ten seconds, which is the only real tuning knob: it bounds how late a crossing is noticed, against one wakeup per step if it were zero.

Thresholds are read out of the config, and each fires at most once per burst:

        val fired = firedSet(prefs)
        for (threshold in thresholds) {
            if (burst < threshold || threshold in fired) continue
            fired.add(threshold)
            writeFired(prefs, fired)

The write precedes the dispatch deliberately, so a process that dies inside the actions leaves the threshold spent rather than running them a second time. The threshold is given back only when the dispatch returns having matched nothing, because the gate that decides whether a crossing was real lives downstream in the rule’s cadence condition and this code sees that verdict only as a boolean. Stillness is not immediate either: the stationary-detect one-shot starts a 90-second timer rather than ending the walk, and a step arriving inside that window cancels it and re-arms the detector. The burst baseline, its start timestamp, the running count, the fired set and the start of the cadence window all live on disk rather than in memory, so a walk that outlives its process is resumed rather than restarted from zero.

A location hold is a bounded requestLocationUpdates at one second and zero metres, on the GPS provider or the fused one depending on an accuracy string. It exists because the proximity alert polls on a 30-minute balanced-accuracy interval, so without a hold the zone state can be half an hour stale. Its duration is an idle timeout rather than a deadline: every step batch pushes the expiry back out, so the only thing keeping the receiver open is movement, and a phone on a table produces none. It refuses to open at all when the system location switch is off, and says so in the trace rather than failing silently.

Everything the phone decides is written down. Each dispatch and each notable lifecycle event becomes one JSON object per line in a trace file under the app’s external files directory, capped at one megabyte with a single rotation, plus a 500-entry ring in memory for the screen. Writes are synchronous on the dispatch path, which is the opposite of the usual advice and correct here: a queued background writer would lose exactly the records that matter most, the ones from a cold-started process that Android kills the moment onReceive returns. Six screens render it, in a WebView over local assets that needs no network, no permission and no AndroidX: the trace with filters, the installed rules joined against their last sighting so a skipped rule shows its clause and reason, the persisted state, install status, the broadcast and notification probe, and live motion tiles.

The registry: the schema is the function signature

The registry consumes a decorated Python function and produces two things from it: a definition record used by the validator, the compiler and the enum generators, and a wrapper the author calls instead of the original function.

        for marker in markers:
            wanted = MARKER_TYPES.get(type(marker))
            if wanted is not None and hint is not wanted:
                raise TypeError(
                    f"{fn.__name__} parameter '{name}' is declared "
                    f"{hint.__name__} and carries {type(marker).__name__}, which bounds a "
                    f"{wanted.__name__}. validate guards each marker on the value's type, so "
                    f"this one would never be checked: declared and silently inert, which is "
                    f"the whole failure the markers exist to prevent."
                )
        out.append(
            Param(
                name,
                cast(type, hint),
                markers,
                p.default is inspect.Parameter.empty,
                outer or inner,
            )
        )
    return tuple(out)

Parameters are read with inspect.signature and get_type_hints(fn, include_extras=True). Declared types are restricted to str, int and bool, because an argument reaches the phone as JSON and the Kotlin parser has a branch for those three. Bounds a type cannot express travel in Annotated: Range(low, high), Pattern(regex), ZoneRef(). The loop above is the second-order check, and it is the load-bearing one: the validator guards each marker on the value’s runtime type, so a Range on a str parameter would never be evaluated, and a marker that is never evaluated is indistinguishable from no marker at all. Raising at import time puts the traceback on the declaration.

Optional types are peeled on both sides of the Annotated, because Annotated[int, Range(0, 1)] | None normalises to a typing.Union while a plain int | None is a types.UnionType. Testing only one origin is what once let a parameter register with no markers and a type nothing recognised.

The trigger decorator raises on four further conditions at import: more than one parameter, an argument with no selector naming the event field it selects on, a selector with no argument, and a selector that is not one of the declared fields. The second of those is the substantive one. Without a selector the argument is decorative, and every automation on that trigger fires on every one of its events. Registering a key twice also raises, naming the module and function that got there first, because the second registration would replace the definition and leave the old schema pointing at the new function’s parameters.

The consequence is that the callable an author writes with and the schema that validates it are one declaration. There is no second table to update, so the two cannot drift.

The condition language: a tree walk, not an expression evaluator

Conditions are patterns over the trigger’s declared fields and over declared states. They are data, deliberately: sibling keys AND, a list means OR, and a single-key dict naming an operator is a leaf.

OPERATORS = (
    "numeric",
    "prefix",
    "suffix",
    "contains",
    "containsIgnoreCase",
    "exists",
    "anythingBut",
)

Path = tuple[str, ...]


def is_operator(v: object) -> bool:
    """A single-key dict whose key names an operator. It terminates the walk
    because it is a leaf value, not more structure."""
    return isinstance(v, dict) and len(v) == 1 and next(iter(v)) in OPERATORS

That file is 35 lines and imports nothing, which is what allows the operator tuple to be rendered as Kotlin without loading any device. The flatten walk descends only into dicts that are not operators, and treats an empty dict below the root as a leaf rather than as nothing, so a condition written as {"sms": {}} is reported instead of vanishing.

The engine’s half of the language dispatches on the enum generated from that tuple:

private fun matchOperator(op: Operator, arg: Json, actual: Json?): Boolean = when (op) {
    Operator.exists -> (arg as? Json.Bool)?.value?.let { want -> (actual != null) == want } ?: false
    Operator.anythingBut -> actual != null && !matchLeaf(arg, actual)
    Operator.prefix -> stringsOf(arg, actual) { want, got -> got.startsWith(want) }
    Operator.suffix -> stringsOf(arg, actual) { want, got -> got.endsWith(want) }
    // Case-sensitive, like the two above.
    Operator.contains -> stringsOf(arg, actual) { want, got -> got.contains(want) }
    // And the one that is not. Measured 2026-08-12 on the fairphone: a rule
    // matching "locate" saw "Locate" arrive and skipped, because a phone
    // keyboard capitalises the first word of a message. Any rule keyed on a
    // command word a human types wants this one; a rule matching a substring
    // of machine-generated text wants the one above.
    Operator.containsIgnoreCase ->
        stringsOf(arg, actual) { want, got -> got.contains(want, ignoreCase = true) }
    Operator.numeric -> numeric(arg, actual)
}

Operator is not checked in anywhere. It exists only inside a Nix build sandbox, rendered from the Python tuple. The absence of an else branch is the whole mechanism: an operator declared in Python and unimplemented here fails kotlinc, in both the host engine jar and the APK.

The property that follows is narrow and worth stating exactly. The gate covers drift between the two lists, not comprehension of an arbitrary document. A leaf naming an operator neither side knows still falls through to literal equality against a scalar, which nothing satisfies, and that looks like an ordinary skip in the trace.

The validator: every problem, and one walk per argument

check takes the whole device configuration and returns every problem it can find, in one pass, as a list of strings naming the automation, the field and the fix.

def _decidable(value: object) -> bool:
    """Whether a leaf on the selector field can be compared to the trigger
    argument at all. A scalar can, a list of decidable leaves can, and
    anythingBut over a decidable leaf can. Every other operator asks about the
    value's shape rather than about which value it is, so it can neither rule
    the argument in nor out, and treating it as a contradiction rejects a rule
    that fires."""
    if isinstance(value, list):
        return bool(value) and all(_decidable(e) for e in value)
    if is_operator(value):
        assert isinstance(value, dict)
        op, operand = next(iter(value.items()))
        return op == "anythingBut" and _decidable(operand)
    return True

This function exists because of a build-rejecting check that lied. The contradiction check asks whether a condition on the trigger’s selector field can hold at the same time as the argument the trigger was called with, since the two are the same value. Its first version conflated “does not rule the argument out” with “cannot be decided at all”, and its anythingBut branch negated that result, so every operator it deliberately skipped became a contradiction once wrapped in anythingBut. A rule combining anythingBut with prefix was rejected with a message asserting it could never fire, which was the opposite of the truth.

Decidability is now separate from contradiction, and the two are ANDed. The generalisable rule is in the docstring: a check that rejects builds has to distinguish “I know this is false” from “I cannot tell”, because negating the second produces a confident lie.

The other structural piece here is _check_param, one walk over all four markers, called from both the trigger side and the action side. It was two functions, each having grown only the markers its first caller needed, and the resulting table was never a decision anyone made.

The compiler: what the artifact carries, and what it pulls in

build refuses to produce anything if check reported a problem, then computes the parts of the artifact that are not written by hand anywhere.

    state_keys = sorted({k for a in cfg.automations for k in referenced_states(a)})
    # A state is only ever set by the events of the triggers that maintain it,
    # so naming one in a condition pulls those triggers into the artifact even
    # when no automation is triggered by them. Without this the phone would
    # never arm the geofence, never see a crossing, and never set the state:
    # a rule that compiles, installs and silently never fires.
    maintainers = {t for k in state_keys for t in (*STATES[k].set_on, *STATES[k].clear_on)}
    trigger_keys = sorted({a.trigger.key for a in cfg.automations} | maintainers)
    action_names = sorted({c.name for a in cfg.automations for c in a.action})

    permissions = sorted(
        {p for k in trigger_keys for p in TRIGGERS[k].permissions}
        | {p for n in action_names for p in ACTIONS[n].permissions}
    )
    queries = sorted({p for n in action_names for p in ACTIONS[n].packages})

The closure that computes maintainers is the load-bearing line. A state is declared as two tables mapping a trigger key to the field carrying the value, and the only events that maintain it come from those triggers. An SMS rule reading location.zone therefore drags both geofence triggers, and their location permissions, into an artifact that has no location-triggered automation in it at all. Without that, the phone would arm nothing, see no crossing, never set the state, and every rule naming it would skip forever.

permissions and queries are unions over the transitive set, sorted. Sorting is not cosmetic: the compiled artifact is compared for equality against a checked-in golden file, and a list built from a set iterated in whatever order it happened to hash would make that comparison flap. The states table is emitted as the declaration itself, so there is no per-state code on either side of the wire.

Nothing in the artifact is authored twice. Permissions are not listed by a human; they are the union of what the referenced triggers and actions declared, and the manifest is generated from that union rather than compared against it.

The build plane: two generated enums and a welded manifest

Nix is where the generation edges are welded. The APK derivation copies the engine sources in, drops the generated Kotlin beside them, and substitutes two blocks into the manifest.

      # --replace-fail, not --replace: if a marker is ever edited away, this
      # stops the build rather than shipping an APK holding only the three
      # posture permissions, which would install cleanly and never fire.
      substitute ${./AndroidManifest.xml} AndroidManifest.xml \
        --replace-fail '<!-- @permissions@ -->' "$(cat perms.xml)" \
        --replace-fail '<!-- @queries@ -->' "$(cat queries.xml)"

perms.xml and queries.xml are produced by jq reading the artifact already copied into the APK’s assets, rather than by importing a Nix value out of a derivation. The queries pass emits the whole element or nothing, because a device whose actions address no other app would otherwise get an empty <queries></queries>.

The <queries> block exists because package visibility is the quietest failure Android has. Since API 30, an intent aimed at a package the manifest does not name is dropped with no exception, no log line, and no way to tell it apart from the app being uninstalled. So an action naming another app declares the package, the compiler unions those declarations, and the manifest is generated from the union. The runtime still resolves the package before broadcasting, which turns a filtered intent into a trace outcome rather than into silence.

Three permissions stay hand-written in the manifest, and the split is principled: they are runtime posture no automation implies, so no declaration can compute them.

The engine copy is one line with a deletion after it. engine/src/*.kt is copied wholesale into the APK build and the host-only CLI file is removed, because it calls exitProcess and has no reason to exist on a phone. That copy, rather than a reimplementation, is the entire basis for trusting the host simulator.

The engine, compiled twice

The same nine Kotlin files build into a host jar and into the APK. The host simulator and the phone therefore run one matcher, one interpolator and one state fold.

fun applyState(config: Config, state: Map<String, Json>, event: Event): Map<String, Json> {
    if (config.states.isEmpty()) return state
    val key = "${event.ns}.${event.event}"
    val out = state.toMutableMap()
    for ((name, def) in config.states) {
        def.setOn[key]?.let { field -> event.fields[field]?.let { out[name] = it } }
        def.clearOn[key]?.let { field ->
            val leaving = event.fields[field]
            if (leaving != null && out[name] == leaving) out.remove(name)
        }
    }
    return out
}

The fold is generic over the two tables the artifact carries, so adding a state adds no Kotlin. The clear is conditional on the state currently holding the value the event names, because leaving a zone the phone was never recorded as being in says nothing about where it is now, and wiping a correct reading on the strength of it would turn one spurious exit into an at-home rule that stops firing.

Two constraints fall out of that fold and are not obvious from the code. A state cannot gate the event that clears it, because the fold runs before anything matches, so a condition naming the state is always evaluated after it has gone. And a state folded from a monotonically increasing counter can never clear at all, since the clearing field would have to equal the stored value; a state maintained by a step counter therefore holds the burst’s start timestamp, which is fixed for the life of the burst, rather than the count.

Precedence is the other thing written twice on purpose. A field of the trigger that fired wins over a same-named state, so location.zone inside a geofence rule is the crossing’s own zone and the same path inside an SMS rule is where the phone is. The compiler’s resolve and the engine’s resolveField are that one rule in two languages, and nothing mechanical keeps them identical.

The replay path converges here. The simulate verb recompiles the artifact in process and runs it through the host jar, so it cannot replay a stale document, and the trace it emits shares its record definitions with the phone’s. Two build-gate checks stand on that: one replays a fixture and exits non-zero if any rule never fires, and one counts matched lines:

              matched=$(grep -c "  MATCHED  " trace.txt || true)
              if [ "$matched" -ne 6 ]; then
                echo "expected exactly 6 MATCHED lines, one per event, got $matched" >&2
                echo "more than 6 means an event fired a rule naming a different zone or time," >&2
                echo "or an SMS rule fired on a zone the phone was not in" >&2
                exit 1
              fi

Counting rather than trusting the exit status is not a style choice. Under-firing is what a non-zero exit catches. Cross-fire is over-firing, and when trigger arguments are ignored every rule still fires at least once, so the exit status is 0 in both the working and the broken world. That was measured by nulling every selector in a copy of the artifact: the exit status stayed 0 and the matched count went to 8.

Interfaces and formats

The artifact is the contract between the two languages. One instance, with the provenance of each field marked:

{
  "version": 2,
  "device": { "fleetName": "...", "package": "...", "secureSettings": false, "ntfy": { "server": "..." } },
  "permissions": ["android.permission.ACCESS_FINE_LOCATION", "..."],
  "queries": ["com.mendhak.gpslogger"],
  "zones": { "home": { "latitude": "57.70887", "longitude": "11.97456", "radius": 200 } },
  "triggers": {
    "location.onEnter": {
      "delivery": "pendingIntent",
      "permissions": ["android.permission.ACCESS_FINE_LOCATION"],
      "event": { "zone": "string", "timestamp": "long" },
      "selector": "zone"
    }
  },
  "states": {
    "location.zone": {
      "type": "string",
      "setOn": { "location.onEnter": "zone" },
      "clearOn": { "location.onExit": "zone" }
    }
  },
  "automations": {
    "sms-at-home": {
      "description": "...",
      "mode": "parallel",
      "persistence": "ephemeral",
      "trigger": { "sms": { "onReceived": null } },
      "condition": { "location": { "zone": "home" } },
      "action": [ { "notify": { "title": "...", "body": "..." } } ]
    }
  }
}

Two details in that shape carry weight. automations is an object keyed by rule name, not a list. And a zone’s latitude and longitude are strings, not JSON numbers: the artifact has no float type, so the declaration holds the decimal text and the Kotlin parser converts it to a Double on the way in. The validator rejects a coordinate written as a Python float, with a message saying to write it as a string, because rounding a coordinate is a geofence in the wrong place rather than a rounding error.

device, zones and automations are declared by the author. version, permissions, queries, triggers and states are computed: the first from a constant the parser range-checks, the next two by union over the transitive set of referenced triggers and actions, the last two by projection from the registry restricted to what the automations reach. selector is always present and null when the trigger takes no argument, so the parser reads it with the same required-key accessor as every other field rather than with a nullable lookup.

Placeholders are strictly ${namespace.field}. An unresolvable one is left in the text verbatim rather than rendered as empty, which is correct for a notification and wrong for a message someone is waiting on, which is why the two rules answering “where is this phone” are split on an exists condition instead of one rule with an optional zone.

The manifest’s two generated blocks are marked by HTML comments, <!-- @permissions@ --> and <!-- @queries@ -->, substituted with --replace-fail. A marker deleted by hand fails the build rather than shipping a manifest with the generated block silently missing.

Invariants and their enforcement

Invariant What checks it
Every registered action has a runtime Exhaustive when over the generated ActionName, no else; kotlinc fails
Every registered trigger has an arming decision Exhaustive when over the generated TriggerKey, no else
Every declared operator is implemented Exhaustive when over the generated Operator, in both the jar and the APK
Argument markers are enforced on both sides One _check_param walk called from the trigger and action paths
A marker bounds a type it can actually check TypeError at import from the registry
A trigger argument selects on something TypeError at import if selector is absent or not a declared field
A key is registered once TypeError at import naming the prior registrant
The artifact shape has not moved Equality against a checked-in golden file, in the test suite
Every rule is reachable by some event Replay fixture exits non-zero if a rule never fires
No rule fires on an event that is not its own Matched-line count against a two-zone, two-alarm fixture
Declared permissions are granted on the device The install verb re-reads the artifact and re-reads each grant
The manifest markers still exist --replace-fail in the substitution
The engine and the APK share a matcher The APK build copies engine/src rather than reimplementing it

Four invariants have nothing mechanical behind them, and they are the useful part of the table.

A cold-delivery trigger needs a manifest <receiver>, and nothing checks that it gained one. The natural arming branch for a cold trigger is an empty block, so a new one ships with a compiling APK and no delivery path, which is exactly the silent no-op the rest of the machinery exists to prevent. The artifact does carry delivery per trigger, so the check is possible; today it is a line in the contributor documentation.

mode and persistence are parsed and never read. Nothing enforces single, so a re-entrant trigger runs twice. That stopped being theoretical when a geofence at the edge of its radius delivered an enter and an exit for the same zone 22 seconds apart: the exit cleared the state, and every rule naming it skipped for the rest of that process. With a state in play, an unenforced mode loses information rather than duplicating a notification.

delivery is parsed and never read by any Kotlin code. It is the machine-readable half of the cold-receiver check, already sitting in the artifact, unused.

The numeric comparison operators are a hand-written pair of lists. The Python validator holds a tuple of five comparison strings and the engine holds a when over five string literals, with nothing tying them together. That is the same drift the generated operator enum was built to eliminate, one level down, still open.

Rejected designs

Nix as the authoring language. The first version of the compiler was a Nix module system, and the whole authoring layer was replaced by Python in 26 minutes of wall clock. The reason was concentrated in one file: the validator module, 414 lines at deletion and the most-churned file of that era at 12 commits. Six shipped bugs were found in it by review. Every error message in it had to be hand-written, because the module system’s own were unusable here. Five checks were then deleted rather than ported, because Python raises them earlier and with a line number: an unknown trigger or action is an ImportError or AttributeError, an unknown or missing action argument is a TypeError from Signature.bind, two triggers on one automation is unrepresentable, and a missing mode is a TypeError from the dataclass. What was given up is introspection: the flake no longer exposes the automations as an evaluable output, and the replacement is the artifact plus jq. The acceptance criterion was that the compiled artifact did not move, and it held: the golden file was captured from the Nix compiler’s output and no commit between that capture and the merge of the Python one touched it.

A cross-field anyOf operator. Designed, implemented, and removed 11 minutes after the matcher shipped. Written as the design described it, the operator-detection predicate fired structurally and the flattening walk stopped one level short, so the path never reached two segments. Written the one way the module system accepted it, nested under a field, the matcher had no branch for it and returned false for every event forever. Removing the trap beat implementing the redundancy.

One contains operator with a case-folding flag. Rejected on the grounds that a condition leaf is a value and has nowhere to put a flag, and on the grounds that the two cases want opposite defaults: a rule matching machine-generated text wants case sensitivity, and a rule matching a command word a human typed does not. The two operators are separate names, and a rule naming containsIgnoreCase says which of the two it meant.

Folding the operator enum into the app’s vocabulary enum. Rejected with a cost taken deliberately. The matcher is compiled into the host jar as well as the APK, so putting the operator enum in the app’s package would have made the engine need some device’s action list to know what prefix means. It is generated into its own file, in the engine’s package, and passed to both derivations. The price is that the engine is no longer buildable from its own directory alone.

A fixed-duration hold on the GPS receiver. The location hold took a duration in seconds, which was a deadline on the whole outing. The first walk that ran the chain end to end released the hold with nine seconds left of the 600 it had asked for, and the response was to raise the number to 1800, which moved the cliff to the half-hour mark rather than removing it. The duration is now an idle timeout pushed out by every step batch. The property the plain duration existed for survives, and it is why this was preferred over an unbounded hold released by a rule: the only thing holding the receiver open is movement, and a phone on a table produces none. The artifact did not move; the number is still 1800 and only its meaning changed.

Observed failure modes

Two hand-copied operator lists. The operator name set was a literal in the matcher, hand-copied from the Python tuple, with nothing tying them together. Adding an operator on the Python side alone produced a condition that validated, compiled, installed and then never matched: unrecognised by the engine, the lookup returned null and the leaf fell through to literal equality against a scalar. The generated enum closed it, and the closure was proven rather than asserted by adding a regex operator to the Python tuple and watching kotlinc refuse the non-exhaustive when.

A marker table nobody had decided. Trigger arguments and action arguments were checked by two functions written at different times, and the three Annotated markers ended up split across them: triggers checked Pattern and ZoneRef but not Range or the declared type, actions checked the type and Range but not Pattern or ZoneRef. Six configurations passed the entire build gate and could not work. Two are worth naming. The scaffolding generator, which renders a starting-point rule from the registry, printed a string literal into an int parameter for any argument carrying neither marker it knew about, and the arming code reads that argument with a cast that yields null, so the sensor was never asked to watch for the threshold. The tool added to make authoring safe emitted a rule that could never fire, and every gate stayed green. The sharpest of the six had no symptom at all: an action argument declaring a Pattern was never checked against it, and the runtime is a when on the accuracy string with an else falling back to the fused provider, so a typo silently downgraded a GPS hold and the trace still recorded the action as having succeeded.

A contradiction check that rejected rules that fire. Described above. It shipped and was corrected 23 minutes and 52 seconds later. It survived eight per-task reviews and was caught by a whole-branch review.

An OR over nothing. An empty list as a condition leaf built cleanly and never matched, because all([]) is True on the Python side and the matcher’s items.any {} is false on the Kotlin side. {"anythingBut": []} is the mirror image, and always matched.

A device module nobody imported. Splitting the single device file into a package created a way to add a module full of rules and have nothing notice. The artifact does not change, so the golden test passes. No rule goes missing, so the replay check passes. The validator never sees the module. Every gate stayed green and the rules never ran. Two tests now cover it, one per direction: a module whose rules never reach the package’s exported list, and an exported rule that lives in no module.

A case-sensitive contains, in production, for 36 minutes. The first real use of the operator sent the word Locate, a phone keyboard having capitalised the first word of the message, and it matched nothing, silently, exactly as designed. The case-folding operator was added beside it rather than replacing it.

Every install left the phone disarmed, and said it had succeeded. The install verb printed that every declared permission was granted and exited 0, and a process listing then showed no application process at all: no service, no sensor listeners, no geofence. Android does not send a boot broadcast after a package replacement over adb, and nothing else started the app, so every install disarmed the phone until a human opened it by hand. The success message was true about permissions and silent about the thing that mattered. The fix takes the package-replaced broadcast, which is delivered to the replaced package itself, and was verified by installing without ever opening the app and finding a 32-second-old process whose trace read service started, 15 automations loaded one second after start. The trap underneath it is the same rule one layer over: force-stopping the app before installing leaves the package flagged stopped, and a stopped package receives no broadcast without the include-stopped-packages flag, package-replaced included. That is the same rule that keeps SMS_RECEIVED out of a force-stopped app.

The one class of bug none of this catches. Nothing in the build compiles a web page or lays out a screen. Targeting API 36 is edge-to-edge, so the content frame is the whole window and the default action bar drew on top of the WebView rather than above it, covering the heading and the entire navigation row and leaving three of four screens unreachable. It was found by looking at the phone, which is the only place it could be found. The second half of that fix generalises: an inset listener set on a WebView is replaced by one the WebView installs itself, so it has to go on a wrapper, and the first attempt changed nothing on screen and looked exactly like insets of zero.

References