From c60d56281f95206afbb2db34994bf18d402841b8 Mon Sep 17 00:00:00 2001
From: Graham McIntire <graham@mcintire.me>
Date: Tue, 21 Apr 2026 13:57:12 -0500
Subject: [PATCH] test(property): add property tests for propagation scoring +
 CIDR matcher

---
 .../propagation/band_config_property_test.exs | 147 +++++++
 .../propagation/scorer_property_test.exs      | 416 ++++++++++++++++++
 .../propagation/scores_file_property_test.exs | 156 +++++++
 .../weather/sounding_params_property_test.exs | 196 +++++++++
 .../plugs/remote_ip_property_test.exs         | 141 ++++++
 5 files changed, 1056 insertions(+)
 create mode 100644 test/microwaveprop/propagation/band_config_property_test.exs
 create mode 100644 test/microwaveprop/propagation/scorer_property_test.exs
 create mode 100644 test/microwaveprop/propagation/scores_file_property_test.exs
 create mode 100644 test/microwaveprop/weather/sounding_params_property_test.exs
 create mode 100644 test/microwaveprop_web/plugs/remote_ip_property_test.exs

diff --git a/test/microwaveprop/propagation/band_config_property_test.exs b/test/microwaveprop/propagation/band_config_property_test.exs
new file mode 100644
index 00000000..8816f2d6
--- /dev/null
+++ b/test/microwaveprop/propagation/band_config_property_test.exs
@@ -0,0 +1,147 @@
+defmodule Microwaveprop.Propagation.BandConfigPropertyTest do
+  @moduledoc """
+  Property tests for `Microwaveprop.Propagation.BandConfig` —
+  exercises the data-driven invariants that the scorer relies on
+  (every band has the right shape; weights sum to 1.0; seasonal
+  tables cover all 12 months).
+  """
+
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Microwaveprop.Propagation.BandConfig
+
+  defp band_config_gen, do: StreamData.member_of(BandConfig.all_bands())
+  defp freq_gen, do: StreamData.member_of(BandConfig.all_freqs())
+  defp month_gen, do: StreamData.integer(1..12)
+
+  property "get/1 returns a well-formed struct for every supported frequency" do
+    check all(freq <- freq_gen()) do
+      band = BandConfig.get(freq)
+      assert is_map(band)
+      assert band.freq_mhz == freq
+      assert is_binary(band.label)
+      assert band.humidity_effect in [:beneficial, :harmful]
+      assert is_map(band.seasonal_base)
+      assert is_map(band.seasonal_adj)
+    end
+  end
+
+  property "every band's seasonal_base covers all 12 months with 0..100 integers" do
+    check all(band <- band_config_gen()) do
+      Enum.each(1..12, fn month ->
+        value = Map.fetch!(band.seasonal_base, month)
+        assert is_integer(value)
+        assert value in 0..100
+      end)
+    end
+  end
+
+  property "weights/1 returns a map whose values sum to ~1.0" do
+    check all(band <- band_config_gen()) do
+      weights = BandConfig.weights(band)
+      total = weights |> Map.values() |> Enum.sum()
+      assert_in_delta total, 1.0, 1.0e-3
+    end
+  end
+
+  property "weights/1 covers exactly the ten scoring factors" do
+    # The scorer reduces over a factors map with these keys; if a band
+    # ever dropped one, `Map.fetch!` in `composite_score/2` would crash.
+    expected = MapSet.new(~w(humidity time_of_day td_depression refractivity sky season wind rain pressure pwat)a)
+
+    check all(band <- band_config_gen()) do
+      keys = band |> BandConfig.weights() |> Map.keys() |> MapSet.new()
+      assert keys == expected
+    end
+  end
+
+  property "weights/1 accepts nil and maps without override, returning the global defaults" do
+    defaults = BandConfig.weights()
+
+    check all(band <- band_config_gen()) do
+      # A band without its own `:weights` falls through to defaults.
+      if Map.has_key?(band, :weights) do
+        assert is_map(BandConfig.weights(band))
+      else
+        assert BandConfig.weights(band) == defaults
+      end
+    end
+
+    assert BandConfig.weights(nil) == defaults
+  end
+
+  property "unknown frequencies return nil from get/1" do
+    known = MapSet.new(BandConfig.all_freqs())
+
+    check all(freq <- StreamData.integer(1..1_000_000), freq not in known) do
+      assert BandConfig.get(freq) == nil
+    end
+  end
+
+  property "sunrise_table returns 12 numeric entries in a plausible hour range" do
+    table = BandConfig.sunrise_table()
+    assert length(table) == 12
+
+    check all(idx <- StreamData.integer(0..11)) do
+      entry = Enum.at(table, idx)
+      assert is_number(entry)
+      assert entry >= 4.0 and entry <= 9.0
+    end
+  end
+
+  property "humidity_beneficial_thresholds are strictly increasing in the threshold value" do
+    thresholds = BandConfig.humidity_beneficial_thresholds()
+    cutoffs = Enum.map(thresholds, fn {cutoff, _score} -> cutoff end)
+    assert cutoffs == Enum.sort(cutoffs)
+    assert length(Enum.uniq(cutoffs)) == length(cutoffs)
+  end
+
+  property "refractivity_thresholds are strictly decreasing (more negative gradient first)" do
+    # `find_refractivity_threshold/3` walks the list and picks the
+    # first cutoff greater than the observed gradient — the ordering
+    # is what makes that correct.
+    cutoffs =
+      Enum.map(BandConfig.refractivity_thresholds(), fn {cutoff, _b, _h} -> cutoff end)
+
+    assert cutoffs == Enum.sort(cutoffs)
+    assert length(Enum.uniq(cutoffs)) == length(cutoffs)
+  end
+
+  property "tiers are ordered descending by min_score and cover 0..100" do
+    tiers = BandConfig.tiers()
+    min_scores = Enum.map(tiers, & &1.min_score)
+    assert min_scores == Enum.sort(min_scores, :desc)
+    assert List.last(min_scores) == 0
+    assert hd(min_scores) <= 100
+
+    check all(s <- StreamData.integer(0..100)) do
+      # Every score in 0..100 matches at least one tier.
+      assert Enum.any?(tiers, fn tier -> s >= tier.min_score end)
+    end
+  end
+
+  property "band_options pairs each band label with its stringified freq_mhz" do
+    options = BandConfig.band_options()
+    assert length(options) == length(BandConfig.all_bands())
+
+    check all({label, value} <- StreamData.member_of(options)) do
+      assert is_binary(label)
+      assert is_binary(value)
+      {freq, ""} = Integer.parse(value)
+      band = BandConfig.get(freq)
+      assert band.label == label
+    end
+  end
+
+  property "every month has a non-negative seasonal_adj value for every band" do
+    check all(band <- band_config_gen(), month <- month_gen()) do
+      # The adjustment map is sparse — nil for missing entries is fine,
+      # but any explicit entry must be a number.
+      case Map.get(band.seasonal_adj, month) do
+        nil -> :ok
+        value -> assert is_number(value)
+      end
+    end
+  end
+end
diff --git a/test/microwaveprop/propagation/scorer_property_test.exs b/test/microwaveprop/propagation/scorer_property_test.exs
new file mode 100644
index 00000000..3241832a
--- /dev/null
+++ b/test/microwaveprop/propagation/scorer_property_test.exs
@@ -0,0 +1,416 @@
+defmodule Microwaveprop.Propagation.ScorerPropertyTest do
+  @moduledoc """
+  Property tests for the pure scoring functions in
+  `Microwaveprop.Propagation.Scorer`. Each property exercises ONE
+  invariant — composite score bounds, per-factor bounds, monotonicity
+  where expected, and the nil-handling contract.
+  """
+
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Microwaveprop.Propagation.BandConfig
+  alias Microwaveprop.Propagation.Scorer
+
+  # ── Generators ──────────────────────────────────────────────────
+
+  # All configured bands — harmful (24+ GHz) and beneficial (10 GHz and
+  # below) are both represented. A property that needs the opposite
+  # humidity effect can filter after generating.
+  defp band_config_gen do
+    StreamData.member_of(BandConfig.all_bands())
+  end
+
+  defp beneficial_band_gen do
+    StreamData.bind(band_config_gen(), fn band ->
+      if band.humidity_effect == :beneficial do
+        StreamData.constant(band)
+      else
+        StreamData.filter(band_config_gen(), &(&1.humidity_effect == :beneficial))
+      end
+    end)
+  end
+
+  defp harmful_band_gen do
+    StreamData.bind(band_config_gen(), fn band ->
+      if band.humidity_effect == :harmful do
+        StreamData.constant(band)
+      else
+        StreamData.filter(band_config_gen(), &(&1.humidity_effect == :harmful))
+      end
+    end)
+  end
+
+  defp latitude_gen, do: StreamData.float(min: 25.0, max: 50.0)
+  defp longitude_gen, do: StreamData.float(min: -125.0, max: -66.0)
+  defp month_gen, do: StreamData.integer(1..12)
+  defp hour_gen, do: StreamData.integer(0..23)
+  defp minute_gen, do: StreamData.integer(0..59)
+
+  # A self-consistent conditions map accepted by `composite_score/2`.
+  # Dewpoint is bounded above by temperature so the T-Td depression
+  # never goes negative.
+  defp conditions_gen do
+    gen all(
+          temp_f <- StreamData.float(min: -20.0, max: 110.0),
+          # 0..60°F spread
+          depression <- StreamData.float(min: 0.0, max: 60.0),
+          wind_ms <- StreamData.float(min: 0.0, max: 40.0),
+          sky_pct <- StreamData.float(min: 0.0, max: 100.0),
+          pressure_mb <- StreamData.float(min: 950.0, max: 1050.0),
+          rain_mmhr <- StreamData.float(min: 0.0, max: 80.0),
+          pwat_mm <- StreamData.float(min: 0.0, max: 60.0),
+          grad <- StreamData.float(min: -400.0, max: 50.0),
+          hpbl <- StreamData.float(min: 50.0, max: 3000.0),
+          month <- month_gen(),
+          hour <- hour_gen(),
+          minute <- minute_gen(),
+          lat <- latitude_gen(),
+          lon <- longitude_gen()
+        ) do
+      dewpoint_f = temp_f - depression
+      temp_c = (temp_f - 32) * 5 / 9
+      dew_c = (dewpoint_f - 32) * 5 / 9
+
+      %{
+        abs_humidity: Scorer.absolute_humidity(temp_c, dew_c),
+        temp_f: temp_f,
+        dewpoint_f: dewpoint_f,
+        wind_speed_kts: wind_ms * 1.94384,
+        sky_cover_pct: sky_pct,
+        utc_hour: hour,
+        utc_minute: minute,
+        month: month,
+        latitude: lat,
+        longitude: lon,
+        pressure_mb: pressure_mb,
+        prev_pressure_mb: nil,
+        rain_rate_mmhr: rain_mmhr,
+        min_refractivity_gradient: grad,
+        bl_depth_m: hpbl,
+        pwat_mm: pwat_mm
+      }
+    end
+  end
+
+  # ── score_humidity/2 ────────────────────────────────────────────
+
+  property "score_humidity is always in 0..100 (beneficial bands)" do
+    check all(
+            ah <- StreamData.float(min: 0.0, max: 40.0),
+            band <- beneficial_band_gen()
+          ) do
+      score = Scorer.score_humidity(ah, band)
+      assert is_integer(score)
+      assert score in 0..100
+    end
+  end
+
+  property "score_humidity is always in 0..100 (harmful bands)" do
+    check all(
+            ah <- StreamData.float(min: 0.0, max: 40.0),
+            band <- harmful_band_gen()
+          ) do
+      score = Scorer.score_humidity(ah, band)
+      assert is_integer(score)
+      assert score in 0..100
+    end
+  end
+
+  property "score_humidity is monotonically non-increasing in humidity (harmful bands)" do
+    # More absolute humidity → more absorption → never a higher score.
+    check all(
+            band <- harmful_band_gen(),
+            ah_lo <- StreamData.float(min: 0.0, max: 20.0),
+            delta <- StreamData.float(min: 0.0, max: 20.0)
+          ) do
+      ah_hi = ah_lo + delta
+      assert Scorer.score_humidity(ah_hi, band) <= Scorer.score_humidity(ah_lo, band)
+    end
+  end
+
+  # ── score_td_depression/3 ───────────────────────────────────────
+
+  property "score_td_depression always in 0..100 for any band" do
+    check all(
+            temp_f <- StreamData.float(min: -40.0, max: 120.0),
+            dewpoint_f <- StreamData.float(min: -50.0, max: 120.0),
+            band <- band_config_gen()
+          ) do
+      score = Scorer.score_td_depression(temp_f, dewpoint_f, band)
+      assert is_integer(score)
+      assert score in 0..100
+    end
+  end
+
+  property "score_td_depression is monotonically non-decreasing in depression (harmful bands)" do
+    # Dry air (wide T-Td depression) reduces water-vapour absorption.
+    check all(
+            band <- harmful_band_gen(),
+            temp_f <- StreamData.float(min: 20.0, max: 100.0),
+            dep_lo <- StreamData.float(min: 0.0, max: 30.0),
+            delta <- StreamData.float(min: 0.0, max: 20.0)
+          ) do
+      dep_hi = dep_lo + delta
+      score_lo = Scorer.score_td_depression(temp_f, temp_f - dep_lo, band)
+      score_hi = Scorer.score_td_depression(temp_f, temp_f - dep_hi, band)
+      assert score_hi >= score_lo
+    end
+  end
+
+  # ── score_refractivity/4,5 ──────────────────────────────────────
+
+  property "score_refractivity returns 50 for nil gradient regardless of other inputs" do
+    check all(
+            bl <- StreamData.one_of([StreamData.constant(nil), StreamData.float(min: 0.0, max: 3000.0)]),
+            band <- band_config_gen()
+          ) do
+      assert Scorer.score_refractivity(nil, bl, band) == 50
+    end
+  end
+
+  property "score_refractivity is in 0..100 for any gradient / band / HPBL / duct / richardson" do
+    check all(
+            grad <- StreamData.float(min: -800.0, max: 200.0),
+            bl <- StreamData.one_of([StreamData.constant(nil), StreamData.float(min: 0.0, max: 3000.0)]),
+            duct_ghz <- StreamData.one_of([StreamData.constant(nil), StreamData.float(min: 0.0, max: 300.0)]),
+            richardson <-
+              StreamData.one_of([StreamData.constant(nil), StreamData.float(min: 0.0, max: 100.0)]),
+            band <- band_config_gen()
+          ) do
+      score = Scorer.score_refractivity(grad, bl, duct_ghz, richardson, band)
+      assert is_integer(score)
+      assert score in 0..100
+    end
+  end
+
+  # ── score_sky/1 ─────────────────────────────────────────────────
+
+  property "score_sky always in 0..100 and monotonically non-increasing in cloudiness" do
+    check all(
+            pct_lo <- StreamData.float(min: 0.0, max: 100.0),
+            delta <- StreamData.float(min: 0.0, max: 100.0)
+          ) do
+      pct_hi = min(100.0, pct_lo + delta)
+      s_lo = Scorer.score_sky(pct_lo)
+      s_hi = Scorer.score_sky(pct_hi)
+      assert s_lo in 0..100
+      assert s_hi in 0..100
+      assert s_hi <= s_lo
+    end
+  end
+
+  # ── score_wind/1 ────────────────────────────────────────────────
+
+  property "score_wind always in 0..100 and monotonically non-increasing in wind speed" do
+    check all(
+            lo <- StreamData.float(min: 0.0, max: 60.0),
+            delta <- StreamData.float(min: 0.0, max: 60.0)
+          ) do
+      hi = lo + delta
+      s_lo = Scorer.score_wind(lo)
+      s_hi = Scorer.score_wind(hi)
+      assert s_lo in 0..100
+      assert s_hi in 0..100
+      assert s_hi <= s_lo
+    end
+  end
+
+  # ── score_rain/2 ────────────────────────────────────────────────
+
+  property "score_rain returns 100 for no rain (nil or 0) across every band" do
+    check all(band <- band_config_gen()) do
+      assert Scorer.score_rain(nil, band) == 100
+      assert Scorer.score_rain(0, band) == 100
+      assert Scorer.score_rain(0.0, band) == 100
+    end
+  end
+
+  property "score_rain always in 0..100 and monotonically non-increasing in rain rate" do
+    check all(
+            band <- band_config_gen(),
+            rate_lo <- StreamData.float(min: 0.0, max: 40.0),
+            delta <- StreamData.float(min: 0.0, max: 40.0)
+          ) do
+      rate_hi = rate_lo + delta
+      s_lo = Scorer.score_rain(rate_lo, band)
+      s_hi = Scorer.score_rain(rate_hi, band)
+      assert s_lo in 0..100
+      assert s_hi in 0..100
+      assert s_hi <= s_lo
+    end
+  end
+
+  # ── score_pwat/2 ────────────────────────────────────────────────
+
+  property "score_pwat always in 0..100 for any band" do
+    check all(
+            pwat <- StreamData.float(min: 0.0, max: 80.0),
+            band <- band_config_gen()
+          ) do
+      score = Scorer.score_pwat(pwat, band)
+      assert is_integer(score)
+      assert score in 0..100
+    end
+  end
+
+  property "score_pwat returns 60 for nil input on every band" do
+    check all(band <- band_config_gen()) do
+      assert Scorer.score_pwat(nil, band) == 60
+    end
+  end
+
+  # ── score_pressure/2 ────────────────────────────────────────────
+
+  property "score_pressure always in 0..100" do
+    check all(
+            current <- StreamData.one_of([StreamData.constant(nil), StreamData.float(min: 900.0, max: 1080.0)]),
+            previous <- StreamData.one_of([StreamData.constant(nil), StreamData.float(min: 900.0, max: 1080.0)])
+          ) do
+      score = Scorer.score_pressure(current, previous)
+      assert is_integer(score)
+      assert score in 0..100
+    end
+  end
+
+  # ── score_season/4 ──────────────────────────────────────────────
+
+  property "score_season always in 0..100 for any band/month/point" do
+    check all(
+            month <- month_gen(),
+            lat <- latitude_gen(),
+            lon <- longitude_gen(),
+            band <- band_config_gen()
+          ) do
+      score = Scorer.score_season(month, lat, lon, band)
+      assert is_integer(score)
+      assert score in 0..100
+    end
+  end
+
+  property "score_season accepts nil lat/lon (no regional adjustment)" do
+    check all(
+            month <- month_gen(),
+            band <- band_config_gen()
+          ) do
+      score = Scorer.score_season(month, nil, nil, band)
+      assert is_integer(score)
+      assert score in 0..100
+    end
+  end
+
+  # ── score_time_of_day/4 ─────────────────────────────────────────
+
+  property "score_time_of_day always in 0..100 and returns a string label" do
+    check all(
+            hour <- hour_gen(),
+            minute <- minute_gen(),
+            month <- month_gen(),
+            lon <- longitude_gen()
+          ) do
+      {score, label} = Scorer.score_time_of_day(hour, minute, month, lon)
+      assert score in 0..100
+      assert is_binary(label)
+      assert label != ""
+    end
+  end
+
+  # ── composite_score/2 ───────────────────────────────────────────
+
+  property "composite_score is integer in 0..100 with a factors map" do
+    check all(
+            conds <- conditions_gen(),
+            band <- band_config_gen()
+          ) do
+      %{score: score, factors: factors} = Scorer.composite_score(conds, band)
+      assert is_integer(score)
+      assert score in 0..100
+      assert is_map(factors)
+
+      Enum.each(factors, fn {_factor, value} ->
+        assert is_integer(value)
+        assert value in 0..100
+      end)
+    end
+  end
+
+  property "composite_score agrees regardless of whether band invariants are pre-computed" do
+    check all(
+            conds <- conditions_gen(),
+            band <- band_config_gen()
+          ) do
+      direct = Scorer.composite_score(conds, band)
+      hoisted_conds = Map.merge(conds, Scorer.precompute_band_invariants(conds))
+      via_hoist = Scorer.composite_score(hoisted_conds, band)
+
+      assert direct.score == via_hoist.score
+      assert direct.factors == via_hoist.factors
+    end
+  end
+
+  # ── commercial_link_boost/2 ─────────────────────────────────────
+
+  property "commercial_link_boost never decreases the score and stays in 0..100" do
+    check all(
+            base <- StreamData.integer(0..100),
+            db <- StreamData.float(min: 0.0, max: 30.0),
+            n_links <- StreamData.integer(0..10)
+          ) do
+      deg = %{degradation_db: db, n_links: n_links}
+      boosted = Scorer.commercial_link_boost(base, deg)
+      assert boosted in 0..100
+      assert boosted >= base
+    end
+  end
+
+  property "commercial_link_boost with nil or zero-link map is a no-op (clamped to 0..100)" do
+    check all(base <- StreamData.integer(-50..150)) do
+      expected = base |> max(0) |> min(100)
+      assert Scorer.commercial_link_boost(base, nil) == expected
+      assert Scorer.commercial_link_boost(base, %{n_links: 0}) == expected
+    end
+  end
+
+  # ── Helpers ─────────────────────────────────────────────────────
+
+  property "dbz_to_rain_rate_mmhr clips below 5 dBZ and caps at 150 mm/hr" do
+    check all(dbz <- StreamData.float(min: -20.0, max: 80.0)) do
+      rate = Scorer.dbz_to_rain_rate_mmhr(dbz)
+      assert is_float(rate)
+      assert rate >= 0.0
+      assert rate <= 150.0
+      if dbz < 5.0, do: assert(rate == 0.0)
+    end
+  end
+
+  property "precip_to_rate_mmhr is 0 for nil / non-positive and passes through positives" do
+    check all(mm <- StreamData.float(min: -10.0, max: 50.0)) do
+      rate = Scorer.precip_to_rate_mmhr(mm)
+      assert is_float(rate)
+      assert rate >= 0.0
+
+      if mm > 0 do
+        assert rate == mm / 1
+      else
+        assert rate == 0.0
+      end
+    end
+  end
+
+  property "f_to_c and c_to_f are mutual inverses" do
+    check all(f <- StreamData.float(min: -100.0, max: 200.0)) do
+      roundtrip = f |> Scorer.f_to_c() |> Scorer.c_to_f()
+      assert_in_delta roundtrip, f, 1.0e-9
+    end
+  end
+
+  property "wind_speed_kts scales with Euclidean norm of (u, v)" do
+    check all(
+            u <- StreamData.float(min: -30.0, max: 30.0),
+            v <- StreamData.float(min: -30.0, max: 30.0)
+          ) do
+      expected = :math.sqrt(u * u + v * v) * 1.94384
+      assert_in_delta Scorer.wind_speed_kts(u, v), expected, 1.0e-9
+    end
+  end
+end
diff --git a/test/microwaveprop/propagation/scores_file_property_test.exs b/test/microwaveprop/propagation/scores_file_property_test.exs
new file mode 100644
index 00000000..9e4a9bb3
--- /dev/null
+++ b/test/microwaveprop/propagation/scores_file_property_test.exs
@@ -0,0 +1,156 @@
+defmodule Microwaveprop.Propagation.ScoresFilePropertyTest do
+  @moduledoc """
+  Property tests for `Microwaveprop.Propagation.ScoresFile.extract_points/2`.
+
+  No IO: we construct the decoded-payload map directly (matching the
+  shape `decode/1` returns) so these tests stay in the pure regime.
+  """
+
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Microwaveprop.Propagation.ScoresFile
+
+  @no_data 255
+
+  # ── Generators ──────────────────────────────────────────────────
+
+  defp grid_gen do
+    gen all(
+          lat_min <- float(min: 20.0, max: 30.0),
+          lon_min <- float(min: -130.0, max: -100.0),
+          step <- member_of([0.125, 0.25, 0.5]),
+          n_rows <- integer(2..8),
+          n_cols <- integer(2..8)
+        ) do
+      %{lat_min: lat_min, lon_min: lon_min, step: step, n_rows: n_rows, n_cols: n_cols}
+    end
+  end
+
+  # Score bytes include the no-data sentinel (255) so `extract_points`
+  # has something to skip.
+  defp scores_body_gen(n_bytes) do
+    list_of(integer(0..255), length: n_bytes)
+  end
+
+  defp payload_gen do
+    gen all(
+          grid <- grid_gen(),
+          body_bytes <- scores_body_gen(grid.n_rows * grid.n_cols)
+        ) do
+      body = :erlang.list_to_binary(body_bytes)
+
+      %{
+        band_mhz: 10_000,
+        valid_time: ~U[2026-04-14 18:00:00Z],
+        lat_min: grid.lat_min,
+        lon_min: grid.lon_min,
+        step: grid.step,
+        n_rows: grid.n_rows,
+        n_cols: grid.n_cols,
+        scores: body
+      }
+    end
+  end
+
+  # ── Properties ──────────────────────────────────────────────────
+
+  property "extract_points returns every non-sentinel cell when bounds are nil" do
+    check all(payload <- payload_gen()) do
+      points = ScoresFile.extract_points(payload, nil)
+      expected_count = payload.scores |> :binary.bin_to_list() |> Enum.count(&(&1 != @no_data))
+      assert length(points) == expected_count
+    end
+  end
+
+  property "every returned point has an integer score in 0..100 and lands on the grid" do
+    check all(payload <- payload_gen()) do
+      points = ScoresFile.extract_points(payload, nil)
+
+      Enum.each(points, fn %{lat: lat, lon: lon, score: score} ->
+        assert is_integer(score)
+        # Bodies include 0..254 (we filter 255); 101..254 are permitted
+        # bytes even if the scoring pipeline never writes them. What we
+        # care about for extraction is that bytes round-trip unchanged.
+        assert score in 0..254
+
+        # lat/lon fall on the declared grid.
+        row = round((lat - payload.lat_min) / payload.step)
+        col = round((lon - payload.lon_min) / payload.step)
+        assert row in 0..(payload.n_rows - 1)
+        assert col in 0..(payload.n_cols - 1)
+      end)
+    end
+  end
+
+  property "extract_points is idempotent under lat/lon round-tripping back into byte offsets" do
+    check all(payload <- payload_gen()) do
+      points = ScoresFile.extract_points(payload, nil)
+
+      Enum.each(points, fn %{lat: lat, lon: lon, score: score} ->
+        row = round((lat - payload.lat_min) / payload.step)
+        col = round((lon - payload.lon_min) / payload.step)
+        offset = row * payload.n_cols + col
+        assert :binary.at(payload.scores, offset) == score
+      end)
+    end
+  end
+
+  property "bounds-filtered output is always a subset of the unbounded output" do
+    check all(
+            payload <- payload_gen(),
+            south_idx <- integer(0..7),
+            north_idx <- integer(0..7),
+            west_idx <- integer(0..7),
+            east_idx <- integer(0..7)
+          ) do
+      south = payload.lat_min + south_idx * payload.step
+      north = payload.lat_min + north_idx * payload.step
+      west = payload.lon_min + west_idx * payload.step
+      east = payload.lon_min + east_idx * payload.step
+
+      bounds = %{south: south, north: north, west: west, east: east}
+      all_points = ScoresFile.extract_points(payload, nil)
+      sub_points = ScoresFile.extract_points(payload, bounds)
+
+      all_set = MapSet.new(all_points)
+      sub_set = MapSet.new(sub_points)
+
+      assert MapSet.subset?(sub_set, all_set)
+    end
+  end
+
+  property "bounds with string keys behave identically to atom keys" do
+    check all(payload <- payload_gen()) do
+      south = payload.lat_min
+      north = payload.lat_min + (payload.n_rows - 1) * payload.step
+      west = payload.lon_min
+      east = payload.lon_min + (payload.n_cols - 1) * payload.step
+
+      atom_bounds = %{south: south, north: north, west: west, east: east}
+      string_bounds = %{"south" => south, "north" => north, "west" => west, "east" => east}
+
+      assert MapSet.new(ScoresFile.extract_points(payload, atom_bounds)) ==
+               MapSet.new(ScoresFile.extract_points(payload, string_bounds))
+    end
+  end
+
+  property "a grid whose body is entirely no-data yields an empty point list" do
+    check all(grid <- grid_gen()) do
+      empty_body = :binary.copy(<<@no_data>>, grid.n_rows * grid.n_cols)
+
+      payload = %{
+        band_mhz: 10_000,
+        valid_time: ~U[2026-04-14 18:00:00Z],
+        lat_min: grid.lat_min,
+        lon_min: grid.lon_min,
+        step: grid.step,
+        n_rows: grid.n_rows,
+        n_cols: grid.n_cols,
+        scores: empty_body
+      }
+
+      assert ScoresFile.extract_points(payload, nil) == []
+    end
+  end
+end
diff --git a/test/microwaveprop/weather/sounding_params_property_test.exs b/test/microwaveprop/weather/sounding_params_property_test.exs
new file mode 100644
index 00000000..ce3be6ec
--- /dev/null
+++ b/test/microwaveprop/weather/sounding_params_property_test.exs
@@ -0,0 +1,196 @@
+defmodule Microwaveprop.Weather.SoundingParamsPropertyTest do
+  @moduledoc """
+  Property tests for `Microwaveprop.Weather.SoundingParams` — exercises
+  the `derive/1` invariants on arbitrary (but physically-plausible)
+  sounding profiles.
+  """
+
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Microwaveprop.Weather.SoundingParams
+
+  # ── Generators ──────────────────────────────────────────────────
+
+  # A realistic mandatory-level pressure sequence: surface down to the
+  # upper troposphere. Pressures strictly decrease. We build it by
+  # walking down from a surface pressure, sampling a positive
+  # step between each level — cheaper than `uniq_list_of` at small
+  # generation sizes and guaranteed to avoid duplicates.
+  defp pressure_levels_gen(n) when n >= 0 do
+    gen all(
+          surface <- float(min: 900.0, max: 1020.0),
+          steps <- list_of(float(min: 5.0, max: 60.0), length: max(n - 1, 0))
+        ) do
+      {levels, _} =
+        Enum.reduce(steps, {[surface], surface}, fn step, {acc, prev} ->
+          next = prev - step
+          {[next | acc], next}
+        end)
+
+      levels
+      |> Enum.reverse()
+      |> Enum.take(n)
+    end
+  end
+
+  # A single level at a given pressure/height with temperature and
+  # dewpoint generated inside the level. `dwpc` is forced ≤ `tmpc` so
+  # the depression is physical.
+  defp level_gen(pres, hght) do
+    gen all(
+          tmpc <- float(min: -80.0, max: 40.0),
+          dep <- float(min: 0.0, max: 40.0)
+        ) do
+      %{
+        "pres" => pres,
+        "tmpc" => tmpc,
+        "dwpc" => tmpc - dep,
+        "hght" => hght,
+        "drct" => 0.0,
+        "sknt" => 0.0
+      }
+    end
+  end
+
+  # Profile generator: heights increase strictly as pressure decreases
+  # (the hydrostatic atmospheric convention). Built by pairing the
+  # sorted pressure sequence (desc) with a heights sequence (asc,
+  # starting at surface elevation), then generating temps/dewpoints per
+  # level.
+  defp profile_gen(min_levels, max_levels) do
+    gen all(
+          n <- integer(min_levels..max_levels),
+          pressures <- pressure_levels_gen(n),
+          surface_hght <- float(min: 0.0, max: 3000.0),
+          height_steps <- list_of(float(min: 50.0, max: 1500.0), length: max(n - 1, 0)),
+          levels <-
+            surface_hght
+            |> heights_from_surface(height_steps, n)
+            |> Enum.zip(pressures)
+            |> Enum.map(fn {h, p} -> level_gen(p, h) end)
+            |> fixed_list()
+        ) do
+      levels
+    end
+  end
+
+  defp heights_from_surface(surface, steps, n) do
+    {hs, _} =
+      Enum.reduce(steps, {[surface], surface}, fn step, {acc, prev} ->
+        next = prev + step
+        {[next | acc], next}
+      end)
+
+    hs |> Enum.reverse() |> Enum.take(n)
+  end
+
+  # ── derive/1 invariants ────────────────────────────────────────
+
+  property "derive/1 returns a result map whenever ≥3 valid levels are given" do
+    check all(profile <- profile_gen(3, 12)) do
+      assert %{} = result = SoundingParams.derive(profile)
+      assert result.level_count >= 3
+      assert result.level_count == length(profile)
+      assert is_list(result.profile)
+      assert is_list(result.inversions)
+      assert is_boolean(result.ducting_detected)
+    end
+  end
+
+  property "derive/1 returns nil when fewer than 3 valid levels are provided" do
+    check all(
+            n <- integer(0..2),
+            profile <- short_profile_gen(n)
+          ) do
+      assert SoundingParams.derive(profile) == nil
+    end
+  end
+
+  defp short_profile_gen(n) do
+    gen all(
+          pressures <- pressure_levels_gen(n),
+          surface_hght <- float(min: 0.0, max: 3000.0),
+          height_steps <- list_of(float(min: 50.0, max: 1500.0), length: max(n - 1, 0)),
+          levels <-
+            surface_hght
+            |> heights_from_surface(height_steps, n)
+            |> Enum.zip(pressures)
+            |> Enum.map(fn {h, p} -> level_gen(p, h) end)
+            |> fixed_list()
+        ) do
+      levels
+    end
+  end
+
+  property "precipitable_water_mm is non-negative when present" do
+    check all(profile <- profile_gen(4, 10)) do
+      %{precipitable_water_mm: pw} = SoundingParams.derive(profile)
+      assert is_number(pw)
+      assert pw >= 0.0
+    end
+  end
+
+  property "boundary_layer_depth_m is non-negative when it resolves" do
+    check all(profile <- profile_gen(4, 10)) do
+      case SoundingParams.derive(profile).boundary_layer_depth_m do
+        nil -> :ok
+        depth -> assert depth >= 0.0
+      end
+    end
+  end
+
+  property "ducting_detected agrees with duct_characteristics non-nilness" do
+    check all(profile <- profile_gen(4, 12)) do
+      %{ducting_detected: detected, duct_characteristics: chars} = SoundingParams.derive(profile)
+      # nil chars ⇔ no ducts detected
+      assert detected == (chars != nil)
+    end
+  end
+
+  property "derive/1 filters out levels missing pres/tmpc/hght before the count check" do
+    check all(
+            bad_level_count <- integer(0..3),
+            good_profile <- profile_gen(3, 6)
+          ) do
+      bad_levels =
+        List.duplicate(%{"pres" => nil, "tmpc" => nil, "hght" => nil, "dwpc" => 0.0}, bad_level_count)
+
+      merged = bad_levels ++ good_profile
+      # Good levels alone satisfy the ≥3 threshold, so adding garbage
+      # should not push the result to nil.
+      assert SoundingParams.derive(merged)
+    end
+  end
+
+  # ── sat_vap_pres / mixing_ratio helpers ─────────────────────────
+
+  property "sat_vap_pres is positive and monotonically increasing in temperature" do
+    check all(
+            t_lo <- float(min: -40.0, max: 30.0),
+            delta <- float(min: 0.1, max: 20.0)
+          ) do
+      t_hi = t_lo + delta
+      e_lo = SoundingParams.sat_vap_pres(t_lo)
+      e_hi = SoundingParams.sat_vap_pres(t_hi)
+
+      assert e_lo > 0.0
+      assert e_hi > 0.0
+      assert e_hi > e_lo
+    end
+  end
+
+  property "mixing_ratio is positive for temperatures well below pressure" do
+    # The formula hits a pole when saturation vapour pressure approaches
+    # the total pressure, which only happens at boiling-hot temperatures
+    # relative to pressure. Realistic weather stays comfortably away.
+    check all(
+            t_c <- float(min: -60.0, max: 30.0),
+            p_mb <- float(min: 300.0, max: 1020.0)
+          ) do
+      mr = SoundingParams.mixing_ratio(t_c, p_mb)
+      assert is_number(mr)
+      assert mr > 0.0
+    end
+  end
+end
diff --git a/test/microwaveprop_web/plugs/remote_ip_property_test.exs b/test/microwaveprop_web/plugs/remote_ip_property_test.exs
new file mode 100644
index 00000000..8e0224a8
--- /dev/null
+++ b/test/microwaveprop_web/plugs/remote_ip_property_test.exs
@@ -0,0 +1,141 @@
+defmodule MicrowavepropWeb.Plugs.RemoteIpPropertyTest do
+  @moduledoc """
+  Property tests for the CIDR-matching logic in
+  `MicrowavepropWeb.Plugs.RemoteIp`. The `peer_trusted?` helper is
+  private, so we exercise it via the plug's `init/1` + `call/2`
+  pipeline: set up a trusted-proxy list, hand the plug a conn whose
+  `remote_ip` we control, and assert whether the forwarded-IP header
+  was honoured.
+  """
+
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  import ExUnit.CaptureLog
+
+  alias MicrowavepropWeb.Plugs.RemoteIp
+
+  # The X-Forwarded-For value we supply whenever we want to check
+  # whether the peer was trusted.
+  @forwarded_ipv4 "198.51.100.7"
+  @forwarded_tuple {198, 51, 100, 7}
+
+  # ── Generators ──────────────────────────────────────────────────
+
+  defp ipv4_octet, do: integer(0..255)
+
+  defp ipv4_tuple_gen do
+    gen all(
+          a <- ipv4_octet(),
+          b <- ipv4_octet(),
+          c <- ipv4_octet(),
+          d <- ipv4_octet()
+        ) do
+      {a, b, c, d}
+    end
+  end
+
+  defp ipv4_string(tuple) do
+    tuple |> Tuple.to_list() |> Enum.join(".")
+  end
+
+  # ── Helpers ─────────────────────────────────────────────────────
+
+  defp call_plug(remote_ip, trusted_cidrs) do
+    opts = RemoteIp.init(trusted_proxies: trusted_cidrs)
+
+    conn =
+      Phoenix.ConnTest.build_conn()
+      |> Map.put(:remote_ip, remote_ip)
+      |> Plug.Conn.put_req_header("x-forwarded-for", @forwarded_ipv4)
+
+    RemoteIp.call(conn, opts)
+  end
+
+  defp trusted?(remote_ip, cidrs) do
+    call_plug(remote_ip, cidrs).remote_ip == @forwarded_tuple
+  end
+
+  defp in_cidr?({a, b, c, d}, {{na, nb, nc, nd}, prefix}) do
+    host = <<a, b, c, d>>
+    network = <<na, nb, nc, nd>>
+    <<host_prefix::bitstring-size(prefix), _::bitstring>> = host
+    <<net_prefix::bitstring-size(prefix), _::bitstring>> = network
+    host_prefix == net_prefix
+  end
+
+  # ── Properties ──────────────────────────────────────────────────
+
+  property "/0 trusts every IPv4 peer" do
+    check all(peer <- ipv4_tuple_gen()) do
+      assert trusted?(peer, ["0.0.0.0/0"])
+    end
+  end
+
+  property "/32 trusts only the exact IP" do
+    check all(
+            anchor <- ipv4_tuple_gen(),
+            other <- ipv4_tuple_gen(),
+            anchor != other
+          ) do
+      cidrs = [ipv4_string(anchor) <> "/32"]
+      assert trusted?(anchor, cidrs)
+      refute trusted?(other, cidrs)
+    end
+  end
+
+  property "every X.Y.Z.W in 10.0.0.0/8 is trusted; nothing outside is" do
+    cidrs = ["10.0.0.0/8"]
+
+    check all(ip <- ipv4_tuple_gen()) do
+      inside = in_cidr?(ip, {{10, 0, 0, 0}, 8})
+      assert trusted?(ip, cidrs) == inside
+    end
+  end
+
+  property "arbitrary /prefix CIDRs match iff the peer's high-order prefix bits agree" do
+    check all(
+            network <- ipv4_tuple_gen(),
+            prefix <- integer(1..32),
+            peer <- ipv4_tuple_gen()
+          ) do
+      cidr = ipv4_string(network) <> "/" <> Integer.to_string(prefix)
+      assert trusted?(peer, [cidr]) == in_cidr?(peer, {network, prefix})
+    end
+  end
+
+  property "union of multiple CIDRs matches the logical OR of each" do
+    check all(
+            a <- ipv4_tuple_gen(),
+            prefix_a <- integer(4..32),
+            b <- ipv4_tuple_gen(),
+            prefix_b <- integer(4..32),
+            peer <- ipv4_tuple_gen()
+          ) do
+      cidrs = [
+        ipv4_string(a) <> "/" <> Integer.to_string(prefix_a),
+        ipv4_string(b) <> "/" <> Integer.to_string(prefix_b)
+      ]
+
+      expected = in_cidr?(peer, {a, prefix_a}) or in_cidr?(peer, {b, prefix_b})
+      assert trusted?(peer, cidrs) == expected
+    end
+  end
+
+  property "/0 as the only CIDR still trusts everything even with bogus entries mixed in" do
+    # Invalid CIDR strings are dropped at init time with a warning;
+    # the surviving /0 should still match every peer.
+    capture_log(fn ->
+      check all(peer <- ipv4_tuple_gen()) do
+        assert trusted?(peer, ["0.0.0.0/0", "not-a-cidr", "999.999.999.999/24", "10.0.0.0/33"])
+      end
+    end)
+  end
+
+  property "an empty trusted-proxy list rejects every peer" do
+    check all(peer <- ipv4_tuple_gen()) do
+      # No CIDRs → the forwarded header must not flow through.
+      refute trusted?(peer, [])
+    end
+  end
+end