LAWS.bend source

LAWS.bend on the hub · documented module

# 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 Baseimport 0xc6ecb72f45a1b2f83318765698582f7f/lib.bend as Colorimport 0xfd7037736e4fa1794a671d0278638da7/lib.bend as Prngimport ./lib.bend as CSdef 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 }