test: add property coverage for grid snaps, backoff, notes

Pure-function invariants that example tests can't express at scale:

- Weather.round_to_iemre_grid/2, HrrrClient.nearest_hrrr_hour/1,
  NexradClient.round_to_5min/1, NarrClient.snap_to_analysis_hour/1:
  each is idempotent, its output satisfies a grid/slot-membership
  predicate, and lies within a bounded distance of the input.
- NarrClient.in_coverage?/1: coverage_end is an exclusive upper
  bound; any timestamp after it is out of coverage.
- IemreFetchWorker.backoff/1: result is in [120, 21_600], monotonic
  non-decreasing in attempt, equals 120*2^(attempt-1) pre-cap.
- Contact submission_changeset notes field: every non-blank string
  up to 2000 chars validates; any longer string is rejected.

22 new properties (139 → 161 including existing); all 2,300 tests
green, credo clean.

test/microwaveprop/radio/contact_submission_test.exs

@@ -1,5 +1,6 @@
 defmodule Microwaveprop.Radio.ContactSubmissionTest do
   use Microwaveprop.DataCase, async: true
+  use ExUnitProperties
 
   alias Microwaveprop.Radio.Contact
 
@@ -138,6 +139,36 @@ defmodule Microwaveprop.Radio.ContactSubmissionTest do
       refute changeset.valid?
       assert errors_on(changeset)[:notes]
     end
+
+    property "accepts any non-blank string up to 2000 graphemes" do
+      check all(
+              len <- integer(1..2000),
+              notes <- string(:printable, length: len),
+              String.trim(notes) != ""
+            ) do
+        attrs = Map.put(@valid_attrs, :notes, notes)
+        changeset = Contact.submission_changeset(%Contact{}, attrs)
+
+        assert changeset.valid?,
+               "expected #{len}-char notes to validate, got errors: " <>
+                 inspect(errors_on(changeset))
+      end
+    end
+
+    property "rejects any notes string longer than 2000 characters" do
+      check all(
+              overage <- integer(1..500),
+              notes <- string(:alphanumeric, length: 2000 + overage)
+            ) do
+        attrs = Map.put(@valid_attrs, :notes, notes)
+        changeset = Contact.submission_changeset(%Contact{}, attrs)
+
+        refute changeset.valid?,
+               "expected #{String.length(notes)}-char notes to be rejected"
+
+        assert errors_on(changeset)[:notes]
+      end
+    end
   end
 
   describe "create_contact/1 deduplication" do

test/microwaveprop/weather/grid_snap_property_test.exs

@@ -0,0 +1,210 @@
+defmodule Microwaveprop.Weather.GridSnapPropertyTest do
+  @moduledoc """
+  Property tests for the coarse-grid / time-slot snapping helpers that
+  scattered across the Weather layer. Each of these functions maps a
+  continuous input onto a discrete set (the IEMRE 0.125° grid, top-of-hour
+  HRRR slots, 5-minute NEXRAD frames, 3-hourly NARR analyses). The
+  invariants every such snap must satisfy are idempotence, bounded
+  distance from the input, and grid-membership of the output.
+  """
+  use ExUnit.Case, async: true
+  use ExUnitProperties
+
+  alias Microwaveprop.Weather
+  alias Microwaveprop.Weather.HrrrClient
+  alias Microwaveprop.Weather.NarrClient
+  alias Microwaveprop.Weather.NexradClient
+
+  describe "Weather.round_to_iemre_grid/2" do
+    property "is idempotent" do
+      check all(
+              lat <- float(min: -89.9, max: 89.9),
+              lon <- float(min: -179.9, max: 179.9)
+            ) do
+        once = Weather.round_to_iemre_grid(lat, lon)
+        twice = then(once, fn {la, lo} -> Weather.round_to_iemre_grid(la, lo) end)
+        assert once == twice
+      end
+    end
+
+    property "output coordinates are multiples of 0.125°" do
+      check all(
+              lat <- float(min: -89.9, max: 89.9),
+              lon <- float(min: -179.9, max: 179.9)
+            ) do
+        {rlat, rlon} = Weather.round_to_iemre_grid(lat, lon)
+        # 0.125 = 1/8, so 8 * coord must be an integer.
+        assert abs(rlat * 8 - round(rlat * 8)) < 1.0e-9
+        assert abs(rlon * 8 - round(rlon * 8)) < 1.0e-9
+      end
+    end
+
+    property "output is within half a grid cell (0.0625°) of the input" do
+      check all(
+              lat <- float(min: -89.9, max: 89.9),
+              lon <- float(min: -179.9, max: 179.9)
+            ) do
+        {rlat, rlon} = Weather.round_to_iemre_grid(lat, lon)
+        # Float.round uses banker's rounding so the worst-case gap is
+        # exactly 0.0625; allow a tiny float epsilon.
+        assert abs(rlat - lat) <= 0.0625 + 1.0e-9
+        assert abs(rlon - lon) <= 0.0625 + 1.0e-9
+      end
+    end
+  end
+
+  describe "HrrrClient.nearest_hrrr_hour/1" do
+    property "is idempotent — once snapped, always snapped" do
+      check all(dt <- datetime_generator()) do
+        once = HrrrClient.nearest_hrrr_hour(dt)
+        twice = HrrrClient.nearest_hrrr_hour(once)
+        assert DateTime.compare(once, twice) == :eq
+      end
+    end
+
+    property "output is always exactly on the hour" do
+      check all(dt <- datetime_generator()) do
+        result = HrrrClient.nearest_hrrr_hour(dt)
+        assert result.minute == 0
+        assert result.second == 0
+      end
+    end
+
+    property "output is within 30 minutes of the input" do
+      check all(dt <- datetime_generator()) do
+        result = HrrrClient.nearest_hrrr_hour(dt)
+        delta_sec = abs(DateTime.diff(result, dt, :second))
+        # Input minute < 30 rounds down; >= 30 rounds up. Worst-case
+        # gap is exactly 30:00.
+        assert delta_sec <= 30 * 60
+      end
+    end
+
+    property "rounds minute >= 30 up to next hour" do
+      check all(dt <- datetime_generator(minute_range: 30..59)) do
+        result = HrrrClient.nearest_hrrr_hour(dt)
+        # result hour is strictly greater than input hour (modulo day/month rollover).
+        assert DateTime.after?(result, dt)
+      end
+    end
+  end
+
+  describe "NexradClient.round_to_5min/1" do
+    property "is idempotent" do
+      check all(dt <- datetime_generator()) do
+        once = NexradClient.round_to_5min(dt)
+        twice = NexradClient.round_to_5min(once)
+        assert DateTime.compare(once, twice) == :eq
+      end
+    end
+
+    property "output minute is a multiple of 5" do
+      check all(dt <- datetime_generator()) do
+        result = NexradClient.round_to_5min(dt)
+        assert rem(result.minute, 5) == 0
+        assert result.second == 0
+      end
+    end
+
+    property "output is never later than the input (floor, not round)" do
+      check all(dt <- datetime_generator()) do
+        result = NexradClient.round_to_5min(dt)
+        assert DateTime.compare(result, dt) in [:lt, :eq]
+      end
+    end
+
+    property "output is within 5 minutes of input" do
+      check all(dt <- datetime_generator()) do
+        result = NexradClient.round_to_5min(dt)
+        delta_sec = DateTime.diff(dt, result, :second)
+        assert delta_sec >= 0
+        assert delta_sec < 5 * 60
+      end
+    end
+  end
+
+  describe "NarrClient.snap_to_analysis_hour/1" do
+    property "is idempotent" do
+      check all(dt <- datetime_generator()) do
+        once = NarrClient.snap_to_analysis_hour(dt)
+        twice = NarrClient.snap_to_analysis_hour(once)
+        assert DateTime.compare(once, twice) == :eq
+      end
+    end
+
+    property "output hour is in {0, 3, 6, 9, 12, 15, 18, 21}" do
+      check all(dt <- datetime_generator()) do
+        result = NarrClient.snap_to_analysis_hour(dt)
+        assert result.hour in [0, 3, 6, 9, 12, 15, 18, 21]
+        assert result.minute == 0
+        assert result.second == 0
+      end
+    end
+
+    property "output is never later than the input (floors to slot)" do
+      check all(dt <- datetime_generator()) do
+        result = NarrClient.snap_to_analysis_hour(dt)
+        assert DateTime.compare(result, dt) in [:lt, :eq]
+      end
+    end
+
+    property "output is within 3 hours of input" do
+      check all(dt <- datetime_generator()) do
+        result = NarrClient.snap_to_analysis_hour(dt)
+        delta_sec = DateTime.diff(dt, result, :second)
+        assert delta_sec >= 0
+        assert delta_sec < 3 * 3600
+      end
+    end
+  end
+
+  describe "NarrClient.in_coverage?/1" do
+    property "coverage_end is the first excluded timestamp (exclusive upper bound)" do
+      coverage_end = NarrClient.coverage_end()
+      refute NarrClient.in_coverage?(coverage_end)
+      one_sec_before = DateTime.add(coverage_end, -1, :second)
+      assert NarrClient.in_coverage?(one_sec_before)
+    end
+
+    property "any DateTime after coverage_end is out of coverage" do
+      coverage_end = NarrClient.coverage_end()
+
+      check all(seconds_after <- integer(1..100_000_000)) do
+        dt = DateTime.add(coverage_end, seconds_after, :second)
+        refute NarrClient.in_coverage?(dt)
+      end
+    end
+  end
+
+  # Generate DateTimes across the HRRR archive era. Avoiding DST
+  # discontinuities and month-boundary edge cases by staying well inside
+  # a single month — snap_to_analysis_hour / nearest_hrrr_hour are
+  # purely field-arithmetic on the DateTime struct, so this is enough
+  # to exercise every branch.
+  defp datetime_generator(opts \\ []) do
+    minute_range = Keyword.get(opts, :minute_range, 0..59)
+
+    gen all(
+          year <- integer(2019..2030),
+          month <- integer(1..12),
+          day <- integer(1..28),
+          hour <- integer(0..23),
+          minute <- integer(minute_range),
+          second <- integer(0..59)
+        ) do
+      %DateTime{
+        year: year,
+        month: month,
+        day: day,
+        hour: hour,
+        minute: minute,
+        second: second,
+        microsecond: {0, 0},
+        std_offset: 0,
+        utc_offset: 0,
+        zone_abbr: "UTC",
+        time_zone: "Etc/UTC"
+      }
+    end
+  end
+end

test/microwaveprop/workers/iemre_fetch_worker_test.exs

@@ -1,5 +1,6 @@
 defmodule Microwaveprop.Workers.IemreFetchWorkerTest do
   use Microwaveprop.DataCase, async: true
+  use ExUnitProperties
 
   alias Microwaveprop.Weather
   alias Microwaveprop.Weather.IemClient
@@ -149,5 +150,34 @@ defmodule Microwaveprop.Workers.IemreFetchWorkerTest do
       assert IemreFetchWorker.backoff(%Oban.Job{attempt: 10}) == 21_600
       assert IemreFetchWorker.backoff(%Oban.Job{attempt: 20}) == 21_600
     end
+
+    property "is always in the [120, 21_600] interval" do
+      check all(attempt <- integer(1..100)) do
+        b = IemreFetchWorker.backoff(%Oban.Job{attempt: attempt})
+        assert b >= 120
+        assert b <= 21_600
+      end
+    end
+
+    property "is monotonic non-decreasing in attempt" do
+      check all(
+              a <- integer(1..50),
+              delta <- integer(0..50)
+            ) do
+        b = a + delta
+
+        assert IemreFetchWorker.backoff(%Oban.Job{attempt: a}) <=
+                 IemreFetchWorker.backoff(%Oban.Job{attempt: b})
+      end
+    end
+
+    property "matches 120 * 2^(attempt-1) before the cap kicks in" do
+      # cap = 21_600 = 120 * 180; 2^7 = 128 < 180 < 256 = 2^8, so
+      # attempts 1..7 are always pre-cap.
+      check all(attempt <- integer(1..7)) do
+        expected = 120 * Integer.pow(2, attempt - 1)
+        assert IemreFetchWorker.backoff(%Oban.Job{attempt: attempt}) == expected
+      end
+    end
   end
 end