# Definitional laws for ColorSample (concrete seeds / ranges).
#
# Alpha uses opaque F32 ops (next_f32 + lerp), so laws target U32 channels,
# Maybe shape, and reflexivity. Color.range_valid is not used in the gate
# (F32.is_le); see ColorSample.range_ok_u32.
import Base
import 0xc6ecb72f45a1b2f83318765698582f7f/lib.bend as Color
import 0xfd7037736e4fa1794a671d0278638da7/lib.bend as Prng
import ./lib.bend as CS

def full_range() -> Color.ColorRange:
  Color.Color.range(Color.Color.rgb(0, 0, 0, 1.0), Color.Color.rgb(255, 255, 255, 1.0))

def narrow() -> Color.ColorRange:
  Color.Color.range(Color.Color.rgb(10, 20, 30, 0.0), Color.Color.rgb(20, 40, 50, 1.0))

def bad_range() -> Color.ColorRange:
  Color.Color.range(Color.Color.rgb(10, 0, 0, 1.0), Color.Color.rgb(5, 0, 0, 1.0))

def point() -> Color.ColorRange:
  Color.Color.range(Color.Color.rgb(7, 8, 9, 1.0), Color.Color.rgb(7, 8, 9, 1.0))

# Invalid U32 range → None (PRNG unused).
law invalid_is_none:
  {
    CS.ColorSample.rgb(bad_range(), Prng.Prng.seed(1)) == None{}
    : Maybe<&1, Color.Rgb & Prng.Prng>
  }

# Determinism: same seed + range → identical first sample.
law same_seed_same_first:
  {
    CS.ColorSample.rgb(full_range(), Prng.Prng.seed(42))
      == CS.ColorSample.rgb(full_range(), Prng.Prng.seed(42))
    : Maybe<&1, Color.Rgb & Prng.Prng>
  }

# Concrete full-range channels for seed 42 (xorshift32 / next_bounded refs).
law seed42_full_r:
  {
    Color.Color.rgb_r(
      CS.ColorSample.unwrap_rgb(
        CS.ColorSample.rgb(full_range(), Prng.Prng.seed(42))))
      == 40
    : U32
  }

law seed42_full_g:
  {
    Color.Color.rgb_g(
      CS.ColorSample.unwrap_rgb(
        CS.ColorSample.rgb(full_range(), Prng.Prng.seed(42))))
      == 172
    : U32
  }

law seed42_full_b:
  {
    Color.Color.rgb_b(
      CS.ColorSample.unwrap_rgb(
        CS.ColorSample.rgb(full_range(), Prng.Prng.seed(42))))
      == 3
    : U32
  }

# Narrow range: channels stay inside lo..=hi (concrete expected values).
law seed42_narrow_r:
  {
    Color.Color.rgb_r(
      CS.ColorSample.unwrap_rgb(
        CS.ColorSample.rgb(narrow(), Prng.Prng.seed(42))))
      == 10
    : U32
  }

law seed42_narrow_g:
  {
    Color.Color.rgb_g(
      CS.ColorSample.unwrap_rgb(
        CS.ColorSample.rgb(narrow(), Prng.Prng.seed(42))))
      == 36
    : U32
  }

law seed42_narrow_b:
  {
    Color.Color.rgb_b(
      CS.ColorSample.unwrap_rgb(
        CS.ColorSample.rgb(narrow(), Prng.Prng.seed(42))))
      == 36
    : U32
  }

# Degenerate range min==max yields that point (span 1 → next_bounded 0).
law point_r:
  {
    Color.Color.rgb_r(
      CS.ColorSample.unwrap_rgb(
        CS.ColorSample.rgb(point(), Prng.Prng.seed(7))))
      == 7
    : U32
  }

law point_g:
  {
    Color.Color.rgb_g(
      CS.ColorSample.unwrap_rgb(
        CS.ColorSample.rgb(point(), Prng.Prng.seed(7))))
      == 8
    : U32
  }

law point_b:
  {
    Color.Color.rgb_b(
      CS.ColorSample.unwrap_rgb(
        CS.ColorSample.rgb(point(), Prng.Prng.seed(7))))
      == 9
    : U32
  }

law range_ok_good:
  { CS.ColorSample.range_ok_u32(full_range()) == True{} : Bool }

law range_ok_bad:
  { CS.ColorSample.range_ok_u32(bad_range()) == False{} : Bool }