test: pin GRIB2 Section parsing to its full contract

- identify_var: full round-trip across every known (discipline,
  category, number) triple, plus a property that any triple outside
  the 12-entry lookup falls back to the "cat:num" default.
- identify_level: hybrid-level and entire-atmosphere branches, plus
  two properties — pressure levels always render as
  `div(value_pa, 100) <> " mb"` and unknown surface types always
  render as `unknown:<type>:<value>` (generator samples only from
  types outside the 6-entry lookup set).
- sign_magnitude_16: round-trip property over [-32_767, 32_767] (±0
  both decode to 0 as intended) and a monotonicity property inside
  a single sign band.

Suite: 2,419 tests + 164 properties (was 2,416 + 159); credo strict
clean.

test/microwaveprop/weather/grib2/section_test.exs

@@ -1,5 +1,6 @@
 defmodule Microwaveprop.Weather.Grib2.SectionTest do
   use ExUnit.Case, async: true
+  use ExUnitProperties
 
   alias Microwaveprop.Weather.Grib2.Section
 
@@ -72,6 +73,44 @@ defmodule Microwaveprop.Weather.Grib2.SectionTest do
     test "returns category:number for unknown variables" do
       assert Section.identify_var(0, 99, 99) == "99:99"
     end
+
+    test "covers the full set of known variables" do
+      # Pin the complete lookup set so adding a new variable without
+      # a matching clause surfaces as a test failure, not a silent
+      # fallback to "cat:num".
+      known = [
+        {{0, 0, 0}, "TMP"},
+        {{0, 0, 6}, "DPT"},
+        {{0, 1, 0}, "SPFH"},
+        {{0, 1, 3}, "PWAT"},
+        {{0, 1, 8}, "APCP"},
+        {{0, 2, 2}, "UGRD"},
+        {{0, 2, 3}, "VGRD"},
+        {{0, 3, 0}, "PRES"},
+        {{0, 3, 5}, "HGT"},
+        {{0, 3, 18}, "HPBL"},
+        {{0, 6, 1}, "TCDC"},
+        {{0, 19, 11}, "TKE"}
+      ]
+
+      for {{d, c, n}, name} <- known do
+        assert Section.identify_var(d, c, n) == name
+      end
+    end
+
+    property "falls back to `cat:num` for every unknown (discipline, cat, num) triple" do
+      known_cat_nums =
+        MapSet.new([{0, 0}, {0, 6}, {1, 0}, {1, 3}, {1, 8}, {2, 2}, {2, 3}, {3, 0}, {3, 5}, {3, 18}, {6, 1}, {19, 11}])
+
+      check all(
+              discipline <- integer(0..50),
+              cat <- integer(0..50),
+              num <- integer(0..50),
+              not MapSet.member?(known_cat_nums, {cat, num})
+            ) do
+        assert Section.identify_var(discipline, cat, num) == "#{cat}:#{num}"
+      end
+    end
   end
 
   describe "level identification" do
@@ -98,6 +137,36 @@ defmodule Microwaveprop.Weather.Grib2.SectionTest do
     test "unknown level type" do
       assert Section.identify_level(255, 0) == "unknown:255:0"
     end
+
+    test "entire atmosphere (type 10)" do
+      assert Section.identify_level(10, 0) == "entire atmosphere"
+    end
+
+    test "hybrid level (type 105) carries the level index through" do
+      assert Section.identify_level(105, 1) == "1 hybrid level"
+      assert Section.identify_level(105, 50) == "50 hybrid level"
+    end
+
+    property "pressure levels always render as `<mb> mb` where mb = value_pa div 100" do
+      check all(value_pa <- integer(0..110_000)) do
+        assert Section.identify_level(100, value_pa) == "#{div(value_pa, 100)} mb"
+      end
+    end
+
+    property "unknown surface type always renders as `unknown:<type>:<value>`" do
+      # Pre-compute the unknown-type domain so the generator doesn't
+      # fight a 97% rejection rate trying to sample 6 known types out
+      # of 256.
+      known = MapSet.new([1, 10, 100, 103, 105, 200])
+      unknown_types = Enum.reject(0..255, &MapSet.member?(known, &1))
+
+      check all(
+              type <- member_of(unknown_types),
+              value <- integer(0..1_000_000)
+            ) do
+        assert Section.identify_level(type, value) == "unknown:#{type}:#{value}"
+      end
+    end
   end
 
   describe "sign_magnitude_16/1" do
@@ -112,6 +181,47 @@ defmodule Microwaveprop.Weather.Grib2.SectionTest do
     test "zero" do
       assert Section.sign_magnitude_16(<<0::16>>) == 0
     end
+
+    property "round-trips any |n| in 0..32_767 back to n through |magnitude| packing" do
+      # The 16-bit field has one sign bit and 15 magnitude bits, so
+      # the representable range is -32_767..32_767.
+      check all(n <- integer(-32_767..32_767)) do
+        mag = abs(n)
+
+        sign_bit =
+          cond do
+            n < 0 -> 1
+            n == 0 -> 0
+            true -> 0
+          end
+
+        packed = <<sign_bit::1, mag::15>>
+        decoded = Section.sign_magnitude_16(packed)
+
+        # Note: +0 and -0 both decode to 0 (sign bit is irrelevant
+        # when magnitude is zero) — that's the expected contract.
+        if n == 0, do: assert(decoded == 0), else: assert(decoded == n)
+      end
+    end
+
+    property "magnitude packing is monotonic in the magnitude bits (same sign)" do
+      check all(
+              sign_bit <- integer(0..1),
+              a <- integer(0..32_766),
+              delta <- integer(0..(32_767 - a))
+            ) do
+        b = a + delta
+        packed_a = <<sign_bit::1, a::15>>
+        packed_b = <<sign_bit::1, b::15>>
+
+        if sign_bit == 0 do
+          assert Section.sign_magnitude_16(packed_a) <= Section.sign_magnitude_16(packed_b)
+        else
+          # Negative magnitudes grow more negative as the magnitude bits grow.
+          assert Section.sign_magnitude_16(packed_a) >= Section.sign_magnitude_16(packed_b)
+        end
+      end
+    end
   end
 
   # --- Helpers ---