@@ -154,8 +154,8 @@ programs are generated, and each one is compiled two ways and run.
 | File | Property |
 |---|---|
 | `test_int_expressions.py` | Random straight-line programs over every ctypes integer type and `c_bool`: `+ - * / // % << >> & \| ^`, comparisons as values, unary `-`, `not`, constructor casts, typed and untyped temporaries, nested. The worked examples of `integers.md` are pinned with `@example`. |
-| `test_int_operators.py` | Every binary operator on every pair of operand types, values drawn edge-first. Random trees rarely reach a negative dividend under a signed `%` and return it undisturbed; this property always does. |
-| `test_int_conversions.py` | Every (source type, destination type, site) triple, where a site is each place a conversion happens: constructor call, declaration, reassignment, untyped local, global store, `return`, global initialiser, and each augmented assignment. |
+| `test_int_operators.py` | Every binary operator, parametrized by the left operand's type, with the right type and both values drawn (edge values first). Random trees rarely reach a negative dividend under a signed `%` and return it undisturbed; this property always does. |
+| `test_int_conversions.py` | Every conversion site, parametrized by the destination type: constructor call, declaration, reassignment, untyped local, global store, `return`, global initialiser, and each augmented assignment. The converted value is read back through an expression whose result depends on its sign and width, not just returned, so a value stored with the right bits but the wrong type is caught too. |
 | `test_known_gaps.py` | Each known divergence's smallest program, as a strict xfail. |
 
 ### Known gaps
@@ -164,8 +164,10 @@ programs are generated, and each one is compiled two ways and run.
 had fixed. Each has a predicate, so the properties step around it and keep
 finding *new* bugs, and a pinned program that `test_known_gaps.py` runs as a
 strict xfail. A fix makes that test XPASS, failing the run until the gap is
-deleted, at which point the properties cover that ground again. A failing
-conversion site is a strict xfail on its parameter instead.
+deleted, at which point the properties cover that ground again. The
+operator and conversion properties step around a gap by drawing only what
+avoids it (not by filtering, which Hypothesis rightly complains about), with
+a comment naming the gap.
 
 ### Running
 
@@ -175,9 +177,10 @@ HYPOTHESIS_PROFILE=thorough pytest tests/property  # 3000 examples, for bug hunt
 ```
 
 CI uses the `ci` profile (100 examples, derandomized, so a failure always
-reproduces), about 90 seconds. The operator and conversion properties run a
-quarter of the profile's count per parameter. Profiles are registered in
-`conftest.py`. A failure prints both programs and the model's value;
+reproduces): about two and a half minutes on a 16-core machine. The
+operator and conversion properties are parametrized by type, so every type
+is tested on every run, and run a sixteenth of the profile's count per
+parameter. Profiles are registered in `conftest.py`. A failure prints both programs and the model's value;
 Hypothesis shrinks it to the smallest program that still fails.
 
 ### Plan
 
@@ -104,12 +104,16 @@ class Gap:
         ),
     ),
     Gap(
-        "untyped-copy-keeps-narrow-type",
-        "`t = a` gives t a's own type, so a c_bool/c_uint8/c_uint16 copy stays "
-        "narrow and promotes to int; integers.md says an undeclared local is "
-        "always 64 bits with the expression's sign (unsigned here). Code or "
-        "doc: a decision (pythonbpf/allocation_pass.py, _allocate_for_name)",
-        lambda p: any(isinstance(e, Var) and e.ty.bits < 32 for _, _, e in p.temps),
+        "untyped-copy-keeps-source-type",
+        "`t = a` gives t a's own type, whatever it is: a c_uint32 copy stays "
+        "u32 and a c_int8 copy stays narrow and promotes to int, while "
+        "integers.md says an undeclared local is always 64 bits with the "
+        "expression's sign. Only a 64-bit source is unaffected. Code or doc: "
+        "a decision (pythonbpf/allocation_pass.py, _allocate_for_name)",
+        lambda p: any(
+            isinstance(e, Var) and e.ty != untyped_local_type(e.ty)
+            for _, _, e in p.temps
+        ),
         # C, by integers.md: -128 + (u64)1 is a u64, so 0 < it holds. PythonBPF:
         # t1 stays a u8, the sum is the int -127, and the compare is false.
         ExpressionProgram(
 
@@ -11,7 +11,7 @@
 """
 
 import pytest
-from hypothesis import assume, given, settings
+from hypothesis import given, settings
 from hypothesis import strategies as st
 
 from tests.property.cints import (
@@ -29,8 +29,11 @@
 from tests.property.harness import CLANG, check_against_clang
 from tests.property.programs import (
     INT64_MAX,
-    INT64_MIN,
+    Bin,
+    Cast,
+    Lit,
     Program,
+    Var,
     as_literal,
     input_decl,
     literal_source,
@@ -39,70 +42,100 @@
 
 pytestmark = pytest.mark.skipif(CLANG is None, reason="clang is not installed")
 
-TYPES = st.sampled_from(ALL_TYPES)
+
+# How the converted value is read back. `return x` alone shows the value but
+# not the type it was stored as, and a later use depends on that type: these
+# read it through an operation whose result changes with its sign and width.
+PROBES = {
+    "value": lambda x: x,
+    # -1 in x's type (promoted), halved: 0 if signed, and u32 and u64 differ
+    "sign_and_width": lambda x: Bin("/", Bin("-", Bin("*", x, Lit(0)), Lit(1)), Lit(2)),
+    # INT_MAX + 1 wraps if x's type promotes to a 32-bit int, not if 64-bit
+    "int_overflow": lambda x: Bin(
+        "+", Bin("+", Bin("*", x, Lit(0)), Lit(2**31 - 1)), Lit(1)
+    ),
+}
 
 
-def _site_program(site, src, dst, value, other):
+def _site_program(site, src, dst, value, other, probe):
     """(Program, model) for converting `a0`, a `src` holding `value`, to `dst`
-    at `site`. `other` is a second value, used where a site needs one."""
+    at `site`, then returning probe(the converted value). `other` is a second
+    value, used where a site needs one."""
     decl_py, decl_c = input_decl("a0", src, value)
-    as_i64 = lambda v: convert(v, C_INT64)  # noqa: E731 (prog returns c_int64)
+
+    def read_back(name, ty, stored, py, c, globals=()):
+        """Finish a program whose statements stored `stored` into `name`."""
+        expr = probe(Var(name, ty))
+        program = Program(
+            py + [f"return {expr.py()}"],
+            c + [f"return {expr.c()};"],
+            globals=list(globals),
+        )
+        return program, lambda: convert(expr.eval({name: stored()}), C_INT64)
 
     if site == "constructor":
+        expr = probe(Cast(dst, Var("a0", src)))
         return Program(
-            [decl_py, f"return {dst.name}(a0)"],
-            [decl_c, f"return ({dst.c_name})a0;"],
-        ), lambda: as_i64(convert(value, dst))
+            [decl_py, f"return {expr.py()}"], [decl_c, f"return {expr.c()};"]
+        ), lambda: convert(expr.eval({"a0": value}), C_INT64)
     if site == "declare":
-        return Program(
-            [decl_py, f"x = {dst.name}(a0)", "return x"],
-            [decl_c, f"{dst.c_name} x = a0;", "return x;"],
-        ), lambda: as_i64(convert(value, dst))
+        return read_back(
+            "x",
+            dst,
+            lambda: convert(value, dst),
+            [decl_py, f"x = {dst.name}(a0)"],
+            [decl_c, f"{dst.c_name} x = a0;"],
+        )
     if site == "reassign":
-        return Program(
-            [decl_py, f"x = {dst.name}(0)", "x = a0", "return x"],
-            [decl_c, f"{dst.c_name} x = 0;", "x = a0;", "return x;"],
-        ), lambda: as_i64(convert(value, dst))
+        return read_back(
+            "x",
+            dst,
+            lambda: convert(value, dst),
+            [decl_py, f"x = {dst.name}(0)", "x = a0"],
+            [decl_c, f"{dst.c_name} x = 0;", "x = a0;"],
+        )
     if site == "untyped_local":
         # dst plays no part: an undeclared local is 64 bits with a0's sign
         local = untyped_local_type(src)
-        return Program(
-            [decl_py, "x = a0", "return x"],
-            [decl_c, f"{local.c_name} x = a0;", "return x;"],
-        ), lambda: as_i64(convert(value, local))
+        return read_back(
+            "x",
+            local,
+            lambda: convert(value, local),
+            [decl_py, "x = a0"],
+            [decl_c, f"{local.c_name} x = a0;"],
+        )
     if site == "global_store":
-        return Program(
-            [decl_py, "global out", "out = a0", "return out"],
-            [decl_c, "out = a0;", "return out;"],
+        return read_back(
+            "out",
+            dst,
+            lambda: convert(value, dst),
+            [decl_py, "global out", "out = a0"],
+            [decl_c, "out = a0;"],
             globals=[("out", dst, 0)],
-        ), lambda: as_i64(convert(value, dst))
+        )
     if site == "return":
+        # Read through the function's own return type, so no probe.
         return Program([decl_py, "return a0"], [decl_c, "return a0;"], ret=dst), (
             lambda: convert(value, dst)
         )
     if site == "global_init":
         # `value` is used as the initialiser literal itself
         lit = as_literal(value, src)
-        return Program(
-            ["return g"], ["return g;"], globals=[("g", dst, lit)]
-        ), lambda: as_i64(convert(lit, dst))
+        return read_back("g", dst, lambda: convert(lit, dst), [], [], [("g", dst, lit)])
     if site.startswith("augassign"):
         op = site.split(" ")[1]
         init = as_literal(other, dst)
-        return Program(
-            [
-                decl_py,
-                f"x = {dst.name}({literal_source(init)})",
-                f"x {op}= a0",
-                "return x",
-            ],
+        return read_back(
+            "x",
+            dst,
+            lambda: convert(binary(op, convert(init, dst), dst, value, src), dst),
+            [decl_py, f"x = {dst.name}({literal_source(init)})", f"x {op}= a0"],
             [
                 decl_c,
                 f"{dst.c_name} x = {literal_source(init)};",
                 f"x {'/' if op == '//' else op}= a0;",
-                "return x;",
             ],
-        ), lambda: as_i64(convert(binary(op, convert(init, dst), dst, value, src), dst))
+        )
     raise ValueError(site)
 
 
@@ -113,33 +146,48 @@ def _site_program(site, src, dst, value, other):
     "untyped_local",
     "global_store",
     "return",
-    pytest.param(
-        "global_init",
-        marks=pytest.mark.xfail(
-            strict=True,
-            raises=AssertionError,
-            reason="a @bpfglobal initialiser that is not a bare constant (as "
-            "c_int64(-5) is not: -5 is a UnaryOp) is emitted as 0, and a "
-            "constant is not converted to the type (c_bool(2) keeps the low "
-            "bit, 0, where C gives 1) (pythonbpf/globals_pass.py, _emit_global)",
-        ),
-    ),
+    "global_init",
 ] + [f"augassign {op}" for op in ARITH_OPS + DIV_OPS + SHIFT_OPS]
 
 
-# A quarter of the profile's examples per site: there are 18 sites, and each
-# example is cheap to state but costs a clang run (~40 ms).
+# Parametrized over the destination type as well as the site, so every type
+# gets examples on every run: drawn at random, a type-specific rule (such as
+# c_bool's `!= 0`) went untested in some runs. 162 parameters, so a
+# sixteenth of the profile's examples each.
+@pytest.mark.parametrize("dst", ALL_TYPES, ids=lambda t: t.name)
 @pytest.mark.parametrize("site", SITES)
-@settings(max_examples=max(10, settings.default.max_examples // 4))
-@given(src=TYPES, dst=TYPES, data=st.data())
-def test_conversion_matches_clang(site, src, dst, data):
-    value = data.draw(values_of(src), label="value")
-    other = data.draw(values_of(dst), label="other")
-    if site == "global_init":
-        value = data.draw(st.integers(INT64_MIN, INT64_MAX), label="initialiser")
+@settings(max_examples=max(5, settings.default.max_examples // 16))
+@given(data=st.data())
+def test_conversion_matches_clang(site, dst, data):
+    # Known gaps are stepped around by drawing only what avoids them, not by
+    # filtering (test_known_gaps.py pins each one):
+    sources = ALL_TYPES
+    if site in ("augassign <<", "augassign >>"):
+        # shift-result-type: `x >>= a` is typed by both operands, so only a
+        # source that leaves the type at x's own promoted type
+        sources = [t for t in ALL_TYPES if common_type(dst, t) == promote(dst)]
+    if site == "untyped_local":
+        # untyped-copy-keeps-source-type: `x = a0` keeps a0's type, which is
+        # right only for a 64-bit a0 (and dst plays no part here)
+        sources = [t for t in ALL_TYPES if untyped_local_type(t) == t]
+    if site == "global_init" and dst.is_bool:
+        pytest.skip("known gap global-initialiser: c_bool(2) keeps its low bit")
+    src = data.draw(st.sampled_from(sources), label="src")
+
     if site in ("augassign <<", "augassign >>"):
-        # known gap shift-result-type: `x >>= a` is typed by both operands
-        # (test_known_gaps.py pins this case)
-        assume(promote(dst) == common_type(dst, src))
-    program, expected = _site_program(site, src, dst, value, other)
+        # a count out of range is undefined in C
+        top = min(promote(dst).bits - 1, src.max)
+        value = data.draw(st.integers(0, top), label="count")
+    elif site == "global_init":
+        # global-initialiser: a negative initialiser is emitted as 0. `value`
+        # is the initialiser literal itself, out-of-range ones included.
+        value = data.draw(st.integers(0, INT64_MAX), label="initialiser")
+    else:
+        value = data.draw(values_of(src), label="value")
+    other = data.draw(values_of(dst), label="other")
+    # global_init's gap is the value itself, which the type probes multiply
+    # away (global_store reads a global's type through them)
+    probes = ["value"] if site == "global_init" else sorted(PROBES)
+    probe = data.draw(st.sampled_from(probes), label="probe")
+    program, expected = _site_program(site, src, dst, value, other, PROBES[probe])
     check_against_clang(program, expected)
@@ -32,10 +32,13 @@
 TYPES = st.sampled_from(ALL_TYPES)
 
 
-# A quarter of the profile's examples per operator, as there are 17 of them.
+# Parametrized over the left operand's type as well as the operator, so every
+# type gets examples on every run (153 parameters, a sixteenth of the
+# profile's examples each).
+@pytest.mark.parametrize("left_ty", ALL_TYPES, ids=lambda t: t.name)
 @pytest.mark.parametrize("op", ARITH_OPS + DIV_OPS + SHIFT_OPS + COMPARE_OPS)
-@settings(max_examples=max(10, settings.default.max_examples // 4))
-@given(left_ty=TYPES, right_ty=TYPES, data=st.data())
+@settings(max_examples=max(5, settings.default.max_examples // 16))
+@given(right_ty=TYPES, data=st.data())
 def test_binary_operator_matches_clang(op, left_ty, right_ty, data):
     left = data.draw(values_of(left_ty), label="left")
     if op in SHIFT_OPS:
 
@@ -6,7 +6,7 @@
 
 import pytest
 
-from tests.property.cints import C_INT64, convert
+from tests.property.cints import C_BOOL, C_INT64, convert
 from tests.property.harness import CLANG, check_against_clang
 from tests.property.known_gaps import GAPS
 from tests.property.programs import Program
@@ -44,3 +44,21 @@ def test_known_gap_augassign_shift():
         ["unsigned int a0 = 1;", "int x = -2147483648;", "x >>= a0;", "return x;"],
     )
     check_against_clang(program, lambda: convert(-(2**31) >> 1, C_INT64))
+
+
+GLOBAL_INIT_REASON = (
+    "global-initialiser: a @bpfglobal initialiser that is not a bare constant "
+    "(c_int64(-5) is not: -5 is a UnaryOp) is emitted as 0, and a constant is "
+    "not converted to the type, so c_bool(2) keeps the low bit, 0, where C "
+    "gives 1 (pythonbpf/globals_pass.py, _emit_global). "
+    "test_int_conversions' global_init site steps around both."
+)
+
+
+@pytest.mark.xfail(strict=True, raises=AssertionError, reason=GLOBAL_INIT_REASON)
+@pytest.mark.parametrize(
+    "ty, literal", [(C_INT64, -5), (C_BOOL, 2)], ids=["negative", "c_bool"]
+)
+def test_known_gap_global_initialiser(ty, literal):
+    program = Program(["return g"], ["return g;"], globals=[("g", ty, literal)])
+    check_against_clang(program, lambda: convert(convert(literal, ty), C_INT64))