Add property-based testing: Hypothesis (Python) and Bombadil (TypeScript)

.eslintrc.cjs

@@ -30,6 +30,15 @@ module.exports = {
                 'import/no-extraneous-dependencies': 'off', // Test deps (vitest, etc.) are devDependencies
                 'sort-keys': 'off'                          // Test objects are ordered for readability, not alphabetically
             }
+        },
+        {
+            files: ['pbt/**/*.ts'],
+            parserOptions: {
+                project: ['./pbt/tsconfig.json']
+            },
+            rules: {
+                'import/no-extraneous-dependencies': 'off' // bombadil is a devDependency
+            }
         }
     ],
     parser: '@typescript-eslint/parser',

.github/workflows/bombadil.yml

@@ -0,0 +1,37 @@
+---
+name: Bombadil property tests
+
+# GHA requires bare `on:` which yamllint sees as boolean
+# yamllint disable-line rule:truthy
+on:
+  schedule:
+    - cron: "17 8 * * *"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  bombadil:
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@v7
+      - name: Set up Node
+        uses: actions/setup-node@v7
+        with:
+          node-version: lts/jod
+          cache: yarn
+      - name: Install dependencies
+        run: yarn install --frozen-lockfile
+      - name: Run Bombadil exploration
+        env:
+          BOMBADIL_HEADLESS: "1"
+          BOMBADIL_TIME_LIMIT: 5m
+        run: yarn test:pbt
+      - name: Upload trace on violation
+        if: failure()
+        uses: actions/upload-artifact@v4
+        with:
+          name: bombadil-output
+          path: pbt-output/

.github/workflows/python-checks.yml

@@ -91,6 +91,8 @@ jobs:
         run: uv pip install --system -r requirements_dev.txt pytest-cov pytest-github-actions-annotate-failures
       - name: Run tests and generate coverage report
         run: pytest ./tests/ --cov=custom_components/lock_code_manager/ --cov-report=xml --junitxml=junit.xml
+        env:
+          HYPOTHESIS_PROFILE: ci
       - name: Upload coverage to Codecov
         if: matrix.python-version == needs.setup.outputs.target-python
         uses: codecov/codecov-action@v7

.gitignore

@@ -7,6 +7,7 @@ venv
 .codex
 .coverage
 coverage/
+.hypothesis/
 .pytest_cache
 .mypy_cache
 .ruff_cache
@@ -22,3 +23,4 @@ docs/
 .github/hooks/
 .opencode/
 junit.xml
+pbt-output/

AGENTS.md

@@ -316,6 +316,29 @@ tests/providers/
 - Provider `async_setup` must be idempotent — tests verify it can be called multiple times.
 - Don't use `MagicMock()` for coordinators when the real coordinator can be used.
 
+## Property-based testing
+
+Two complementary layers exist alongside the example-based suites:
+
+- **Python (Hypothesis)** — `tests/properties/` runs as part of the normal
+  `pytest tests/` invocation. The default `dev` profile uses 15 examples to
+  keep the suite fast; CI sets `HYPOTHESIS_PROFILE=ci` (200 examples). Run
+  the deep profile locally with `HYPOTHESIS_PROFILE=ci pytest tests/properties/`.
+  `test_credential_machine.py` is a stateful machine driving the real
+  BaseLock write orchestration against `MockLCMLock`.
+- **TypeScript (Bombadil)** — `pbt/` contains a browser harness that mounts
+  the built cards with a scripted mock `hass` plus a chaos panel, and a
+  Bombadil spec (`pbt/spec.ts`) with temporal-logic properties (no PIN leaks
+  from masked cards, chip counts match the model, pushed data eventually
+  renders). Run locally with `yarn test:pbt` (env knobs:
+  `BOMBADIL_TIME_LIMIT`, `BOMBADIL_HEADLESS=1`). CI runs it nightly and on
+  manual dispatch (`bombadil.yml`), never on pull requests. Inspect
+  violations with `yarn bombadil browser inspect pbt-output`.
+
+Counterexample triage: a found counterexample is a deliverable. Either fix
+the code, or — only for documented contract edges — narrow the strategy
+with a comment citing the contract. Never silence one by rerunning.
+
 ## Adding Lock Provider Support
 
 1. Create new file in `providers/` (e.g., `my_provider.py`)

custom_components/lock_code_manager/providers/_util.py

@@ -98,7 +98,8 @@ def parse_slot_num(value: object) -> int | None:
     Convert a slot identifier to an int, or return None if not convertible.
 
     Mirrors ``int(value)`` while collapsing the ``TypeError``/``ValueError``
-    that providers otherwise catch when a lock reports a non-numeric slot key.
+    that providers otherwise catch when a lock reports a non-numeric slot key
+    (and ``OverflowError``, which ``int`` raises for infinite floats).
     JSON booleans are rejected rather than coerced (``int(True)`` is 1, so a
     malformed ``true`` would otherwise silently address slot 1).
     Call sites remain responsible for their own logging and skip/return flow.
@@ -107,5 +108,5 @@ def parse_slot_num(value: object) -> int | None:
         return None
     try:
         return int(value)  # type: ignore[call-overload]
-    except TypeError, ValueError:
+    except TypeError, ValueError, OverflowError:
         return None

package.json

@@ -14,11 +14,12 @@
   "scripts": {
     "build": "yarn install ; rollup -c",
     "watch": "rollup -c --watch",
-    "lint": "eslint --ext .ts ./ts",
+    "lint": "eslint --ext .ts ./ts ./pbt",
     "lint:fix": "yarn lint --fix",
     "test": "vitest run",
     "test:watch": "vitest",
-    "test:coverage": "vitest run --coverage"
+    "test:coverage": "vitest run --coverage",
+    "test:pbt": "yarn build && node pbt/run.mjs"
   },
   "dependencies": {
     "@mdi/js": "^7.4.47",
@@ -27,6 +28,7 @@
     "lit-html": "^3.3.3"
   },
   "devDependencies": {
+    "@antithesishq/bombadil": "0.6.1",
     "@babel/core": "^7.29.7",
     "@babel/preset-env": "^7.29.7",
     "@rollup/plugin-babel": "^7.1.0",

pbt/harness/harness.js

@@ -0,0 +1,222 @@
+/**
+ * Bombadil harness: mounts lcm-slot and lcm-lock-codes with a scripted mock
+ * hass. Plain JavaScript on purpose — no build step; served statically next
+ * to the built bundle. The model below is the single source of truth; chaos
+ * buttons mutate it and re-push through the subscription callbacks, the same
+ * path the real websocket API uses.
+ */
+
+const CONFIG_ENTRY_ID = 'pbt_entry';
+const LOCK_ENTITY_ID = 'lock.pbt_front_door';
+
+const model = {
+    revision: 0,
+    suspended: false,
+    slots: {
+        1: { active: true, enabled: true, inSync: true, name: 'Alice', pin: '4921' },
+        2: { active: false, enabled: false, inSync: true, name: 'Bob', pin: '8375' },
+        3: { active: true, enabled: true, inSync: false, name: 'Carol', pin: '6104' }
+    }
+};
+
+// Read-only window surface for spec extractors. Secret PINs deliberately
+// live here (JavaScript only), never in the DOM: the no-leak property greps
+// the rendered DOM for them.
+window.__lcmHarness = {
+    model,
+    secretPins: () => Object.values(model.slots).map((slot) => slot.pin)
+};
+
+/** Subscriptions keyed by an opaque id -> {message, callback}. */
+const subscriptions = new Map();
+let nextSubscriptionId = 1;
+
+function slotCardData(slotNum) {
+    const slot = model.slots[slotNum];
+    return {
+        active: slot.active,
+        conditions: {},
+        config_entry_id: CONFIG_ENTRY_ID,
+        config_entry_title: 'PBT Lock Manager',
+        enabled: slot.enabled,
+        entities: {
+            active: `binary_sensor.slot_${slotNum}_active`,
+            enabled: `switch.slot_${slotNum}_enabled`,
+            name: `text.slot_${slotNum}_name`,
+            pin: `text.slot_${slotNum}_pin`
+        },
+        locks: [
+            {
+                code: null,
+                code_length: slot.pin.length,
+                entity_id: LOCK_ENTITY_ID,
+                in_sync: slot.inSync,
+                name: 'Front Door',
+                sync_status: slot.inSync ? 'in_sync' : 'out_of_sync'
+            }
+        ],
+        name: slot.name,
+        // Harness cards run code_display: 'masked' — the PIN value never
+        // leaves the model; only its length does.
+        pin: null,
+        pin_length: slot.pin.length,
+        slot_num: slotNum
+    };
+}
+
+function lockCoordinatorData() {
+    return {
+        lock_entity_id: LOCK_ENTITY_ID,
+        lock_name: 'Front Door',
+        ...(model.suspended ? { sync_status: 'suspended' } : {}),
+        slots: Object.entries(model.slots).map(([slotNum, slot]) => ({
+            active: slot.active,
+            code: null,
+            code_length: slot.pin.length,
+            config_entry_id: CONFIG_ENTRY_ID,
+            config_entry_title: 'PBT Lock Manager',
+            in_sync: slot.inSync,
+            // ts/types.ts LockCoordinatorSlotData names this `managed`
+            // (lock-codes-card.ts reads `slot.managed` throughout); the
+            // original draft used `is_managed`, which the card would have
+            // silently ignored.
+            managed: true,
+            name: slot.name,
+            slot: Number(slotNum)
+        }))
+    };
+}
+
+function payloadFor(message) {
+    if (message.type === 'lock_code_manager/subscribe_code_slot') {
+        return model.slots[message.slot] ? slotCardData(message.slot) : null;
+    }
+    if (message.type === 'lock_code_manager/subscribe_lock_codes') {
+        return lockCoordinatorData();
+    }
+    return null;
+}
+
+function pushAll() {
+    model.revision += 1;
+    for (const { callback, message } of subscriptions.values()) {
+        const payload = payloadFor(message);
+        if (payload !== null) {
+            callback(payload);
+        }
+    }
+}
+
+const mockHass = {
+    callService: (domain, service, data) => {
+        // Card-initiated edits loop back through the model like the real
+        // backend would.
+        pushAll();
+        return Promise.resolve({ domain, data, service });
+    },
+    callWS: () => Promise.resolve({}),
+    connection: {
+        subscribeMessage: (callback, message) => {
+            const id = nextSubscriptionId;
+            nextSubscriptionId += 1;
+            subscriptions.set(id, { callback, message });
+            const payload = payloadFor(message);
+            if (payload !== null) {
+                callback(payload);
+            }
+            return Promise.resolve(() => subscriptions.delete(id));
+        }
+    },
+    states: {
+        [LOCK_ENTITY_ID]: {
+            attributes: { friendly_name: 'Front Door' },
+            entity_id: LOCK_ENTITY_ID,
+            state: 'locked'
+        }
+    }
+};
+
+function mountCards() {
+    for (const slotNum of Object.keys(model.slots)) {
+        const card = document.createElement('lcm-slot');
+        card.setConfig({
+            code_display: 'masked',
+            config_entry_id: CONFIG_ENTRY_ID,
+            slot: Number(slotNum),
+            type: 'custom:lcm-slot'
+        });
+        card.hass = mockHass;
+        document.getElementById('masked-zone').appendChild(card);
+    }
+    const lockCodes = document.createElement('lcm-lock-codes');
+    lockCodes.setConfig({
+        code_display: 'masked',
+        lock_entity_id: LOCK_ENTITY_ID,
+        type: 'custom:lcm-lock-codes'
+    });
+    lockCodes.hass = mockHass;
+    document.getElementById('lock-codes-zone').appendChild(lockCodes);
+}
+
+function randomPin() {
+    return String(Math.floor(1000 + Math.random() * 9000));
+}
+
+function randomSlotNum() {
+    const nums = Object.keys(model.slots);
+    return Number(nums[Math.floor(Math.random() * nums.length)]);
+}
+
+const chaosHandlers = {
+    'chaos-add-slot': () => {
+        const next = [1, 2, 3, 4, 5, 6].find((n) => !model.slots[n]);
+        if (next) {
+            model.slots[next] = {
+                active: true,
+                enabled: true,
+                inSync: false,
+                name: `User ${next}`,
+                pin: randomPin()
+            };
+        }
+    },
+    'chaos-clear-slot': () => {
+        const nums = Object.keys(model.slots);
+        if (nums.length > 1) {
+            delete model.slots[randomSlotNum()];
+        }
+    },
+    'chaos-external-pin': () => {
+        model.slots[randomSlotNum()].pin = randomPin();
+    },
+    'chaos-rename': () => {
+        const slot = model.slots[randomSlotNum()];
+        // Digit-free label: a numeric revision could collide with a live
+        // secret PIN and falsely trip the no-leak property.
+        slot.name = `Renamed ${String(model.revision).replace(/\d/g, (d) => 'ABCDEFGHIJ'[Number(d)])}`;
+    },
+    'chaos-toggle-active': () => {
+        const slot = model.slots[randomSlotNum()];
+        slot.active = !slot.active;
+    },
+    'chaos-toggle-enabled': () => {
+        const slot = model.slots[randomSlotNum()];
+        slot.enabled = !slot.enabled;
+    },
+    'chaos-toggle-suspended': () => {
+        model.suspended = !model.suspended;
+    },
+    'chaos-toggle-sync': () => {
+        const slot = model.slots[randomSlotNum()];
+        slot.inSync = !slot.inSync;
+    }
+};
+
+for (const [id, handler] of Object.entries(chaosHandlers)) {
+    document.getElementById(id).addEventListener('click', () => {
+        handler();
+        pushAll();
+    });
+}
+
+mountCards();