Tests: hypothesis invariants for matching rule 1

One property per bullet of MATCHING.md's invariants section, over a
small content pool chosen for dense claim and slot collisions: the
containment statement restated independently, reorder invariance
across inputs, outputs, and condition lists, monotonicity (removing
a claim never invalidates), the unmatchable-claim rejection, the
exactly-claimed-output removal and mutation metamorphics, and the
generalized theft property (k identical claims never fit k minus one
identical slots). Model preconditions (value conservation, duplicate
outpoints, empty sides, amount ranges) are pinned as ValueError,
distinct from spend invalidity.

Author: EvanWinget

python/tests/test_matching_invariants.py

@@ -0,0 +1,205 @@
+"""Property-based invariants for the matching layer.
+
+The matching rules have no external oracle, so these properties and
+the adversarial vectors in vectors/matching/ stand in for one. Each
+property here is one bullet of MATCHING.md's invariants section.
+
+Transactions are generated over a small content pool (three scripts,
+four amounts) so claim and slot collisions are dense, which is where
+rule 1 earns its keep.
+"""
+
+from collections import Counter
+
+import pytest
+from bitlisp import (
+    BitLispError,
+    CreateCoin,
+    Transaction,
+    TxInput,
+    TxOutput,
+    validate_transaction,
+)
+from hypothesis import given
+from hypothesis import strategies as st
+
+SCRIPTS = (b"\x51", b"\x52", b"\x53")
+AMOUNTS = (0, 1, 2, 3)
+UNMATCHABLE = b"\xff"  # never appears in generated outputs
+
+contents = st.tuples(st.sampled_from(SCRIPTS), st.sampled_from(AMOUNTS))
+claim_lists = st.lists(contents, max_size=3)
+output_lists = st.lists(contents, min_size=1, max_size=6)
+# None is a non-BitLisp input, a list is a BitLisp input's claims.
+input_specs = st.lists(st.one_of(st.none(), claim_lists), min_size=1, max_size=3)
+
+
+def build_tx(input_claims, outputs):
+    """A transaction whose first input funds all outputs, with
+    headroom so metamorphic amount bumps stay conserved."""
+    out_total = sum(amount for _, amount in outputs) + 10
+    inputs = []
+    for n, claims in enumerate(input_claims):
+        conditions = (
+            None
+            if claims is None
+            else tuple(CreateCoin(script, amount) for script, amount in claims)
+        )
+        inputs.append(
+            TxInput(
+                txid=bytes([n + 1]) * 32,
+                index=0,
+                script_pubkey=b"\x51",
+                amount=out_total if n == 0 else 0,
+                sequence=0xFFFFFFFF,
+                conditions=conditions,
+            )
+        )
+    return Transaction(
+        version=2,
+        locktime=0,
+        inputs=tuple(inputs),
+        outputs=tuple(TxOutput(script, amount) for script, amount in outputs),
+    )
+
+
+def is_valid(tx):
+    try:
+        validate_transaction(tx)
+        return True
+    except BitLispError as exc:
+        assert exc.code == "unsatisfied_output_claim"
+        return False
+
+
+def all_claims(input_claims):
+    return [c for claims in input_claims if claims is not None for c in claims]
+
+
+@given(input_specs, output_lists)
+def test_validity_is_multiset_containment(input_claims, outputs):
+    """Rule 1's spec statement, restated independently: valid exactly
+    when no content is claimed more times than slots carry it."""
+    tx = build_tx(input_claims, outputs)
+    claimed = Counter(all_claims(input_claims))
+    slots = Counter(outputs)
+    expected = all(count <= slots[content] for content, count in claimed.items())
+    assert is_valid(tx) == expected
+
+
+@given(input_specs, output_lists, st.randoms(use_true_random=False))
+def test_reordering_never_changes_the_outcome(input_claims, outputs, rng):
+    tx = build_tx(input_claims, outputs)
+    shuffled_inputs = list(input_claims)
+    rng.shuffle(shuffled_inputs)
+    shuffled_inputs = [
+        (None if claims is None else rng.sample(claims, len(claims)))
+        for claims in shuffled_inputs
+    ]
+    shuffled_outputs = rng.sample(outputs, len(outputs))
+    shuffled = build_tx(shuffled_inputs, shuffled_outputs)
+    assert is_valid(tx) == is_valid(shuffled)
+
+
+@given(input_specs, output_lists)
+def test_removing_a_condition_never_invalidates(input_claims, outputs):
+    """Constraints only tighten. Dropping any one claim from a valid
+    transaction leaves it valid."""
+    tx = build_tx(input_claims, outputs)
+    if not is_valid(tx):
+        return
+    for i, claims in enumerate(input_claims):
+        if not claims:
+            continue
+        for j in range(len(claims)):
+            reduced = list(input_claims)
+            reduced[i] = claims[:j] + claims[j + 1 :]
+            assert is_valid(build_tx(reduced, outputs))
+
+
+@given(input_specs, output_lists)
+def test_adding_an_unmatchable_claim_always_invalidates(input_claims, outputs):
+    augmented = list(input_claims)
+    augmented.append([(UNMATCHABLE, 1)])
+    assert not is_valid(build_tx(augmented, outputs))
+
+
+@given(input_specs, output_lists)
+def test_removing_an_exactly_claimed_output_invalidates(input_claims, outputs):
+    tx = build_tx(input_claims, outputs)
+    if not is_valid(tx) or len(outputs) < 2:
+        return
+    claimed = Counter(all_claims(input_claims))
+    slots = Counter(outputs)
+    for content, count in claimed.items():
+        if count == slots[content]:
+            reduced = list(outputs)
+            reduced.remove(content)
+            assert not is_valid(build_tx(input_claims, reduced))
+            break
+
+
+@given(input_specs, output_lists, st.sampled_from(["amount", "script"]))
+def test_mutating_an_exactly_claimed_output_invalidates(
+    input_claims, outputs, mutation
+):
+    """Metamorphic: bump the amount or flip a script byte on a slot
+    whose content is exactly covered by claims."""
+    tx = build_tx(input_claims, outputs)
+    if not is_valid(tx):
+        return
+    claimed = Counter(all_claims(input_claims))
+    slots = Counter(outputs)
+    for content, count in claimed.items():
+        if count == slots[content] and count > 0:
+            script, amount = content
+            if mutation == "amount":
+                mutated_content = (script, amount + 1)
+            else:
+                mutated_content = (bytes([script[0] ^ 0x01]), amount)
+            mutated = list(outputs)
+            mutated[mutated.index(content)] = mutated_content
+            assert not is_valid(build_tx(input_claims, mutated))
+            break
+
+
+@given(st.integers(min_value=2, max_value=5), contents)
+def test_k_claims_never_fit_k_minus_1_slots(k, content):
+    """The theft property, generalized: k identical claims are never
+    satisfied by k - 1 identical slots."""
+    input_claims = [[content] for _ in range(k)]
+    outputs = [content] * (k - 1)
+    assert not is_valid(build_tx(input_claims, outputs))
+    assert is_valid(build_tx(input_claims, outputs + [content]))
+
+
+# --- transaction-model preconditions ---------------------------------------
+# Value conservation is enforced at construction, so matching never
+# sees a transaction that creates value out of nothing.
+
+
+def test_model_rejects_value_creation():
+    tx_input = TxInput(b"\x01" * 32, 0, b"\x51", 4, 0)
+    with pytest.raises(ValueError, match="value not conserved"):
+        Transaction(2, 0, (tx_input,), (TxOutput(b"\x51", 5),))
+
+
+def test_model_rejects_duplicate_outpoints():
+    tx_input = TxInput(b"\x01" * 32, 0, b"\x51", 1, 0)
+    with pytest.raises(ValueError, match="duplicate input outpoint"):
+        Transaction(2, 0, (tx_input, tx_input), (TxOutput(b"\x51", 1),))
+
+
+def test_model_rejects_empty_sides():
+    tx_input = TxInput(b"\x01" * 32, 0, b"\x51", 1, 0)
+    with pytest.raises(ValueError, match="non-empty"):
+        Transaction(2, 0, (), (TxOutput(b"\x51", 1),))
+    with pytest.raises(ValueError, match="non-empty"):
+        Transaction(2, 0, (tx_input,), ())
+
+
+def test_model_rejects_out_of_range_amounts():
+    with pytest.raises(ValueError, match="amount out of range"):
+        TxOutput(b"\x51", -1)
+    with pytest.raises(ValueError, match="amount out of range"):
+        TxOutput(b"\x51", 2_100_000_000_000_001)