LAWS.bend open laws/TODOs

raw source on the hub · import 0xedb848fc7835fe5f9d34e575a7612788/LAWS.bend as LAWS

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.

4 imports

import Base
import 0xc6ecb72f45a1b2f83318765698582f7f/lib.bend as Color
import 0xfd7037736e4fa1794a671d0278638da7/lib.bend as Prng
import ./lib.bend as CS

Laws

law invalid_is_none provedin PROOF.bendsource · line 24 · raw

{0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(bad_range, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(1)) == None{} : Maybe<&1, Pair(0xc6ecb72f45a1b2f83318765698582f7f/lib.Rgb, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng)>}

Invalid U32 range → None (PRNG unused).

law same_seed_same_first provedin PROOF.bendsource · line 31 · raw

{0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(full_range, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)) == 0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(full_range, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)) : Maybe<&1, Pair(0xc6ecb72f45a1b2f83318765698582f7f/lib.Rgb, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng)>}

Determinism: same seed + range → identical first sample.

law seed42_full_r provedin PROOF.bendsource · line 39 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_r(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.unwrap_rgb(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(full_range, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)))) == 40 : U32}

Concrete full-range channels for seed 42 (xorshift32 / next_bounded refs).

law seed42_full_g provedin PROOF.bendsource · line 48 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_g(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.unwrap_rgb(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(full_range, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)))) == 172 : U32}

law seed42_full_b provedin PROOF.bendsource · line 57 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_b(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.unwrap_rgb(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(full_range, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)))) == 3 : U32}

law seed42_narrow_r provedin PROOF.bendsource · line 67 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_r(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.unwrap_rgb(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(narrow, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)))) == 10 : U32}

Narrow range: channels stay inside lo..=hi (concrete expected values).

law seed42_narrow_g provedin PROOF.bendsource · line 76 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_g(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.unwrap_rgb(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(narrow, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)))) == 36 : U32}

law seed42_narrow_b provedin PROOF.bendsource · line 85 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_b(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.unwrap_rgb(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(narrow, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(42)))) == 36 : U32}

law point_r provedin PROOF.bendsource · line 95 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_r(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.unwrap_rgb(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(point, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(7)))) == 7 : U32}

Degenerate range min==max yields that point (span 1 → next_bounded 0).

law point_g provedin PROOF.bendsource · line 104 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_g(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.unwrap_rgb(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(point, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(7)))) == 8 : U32}

law point_b provedin PROOF.bendsource · line 113 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_b(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.unwrap_rgb(0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.rgb(point, 0xfd7037736e4fa1794a671d0278638da7/lib.Prng.seed(7)))) == 9 : U32}

law range_ok_good provedin PROOF.bendsource · line 122 · raw

{0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.range_ok_u32(full_range) == True{} : Bool}

law range_ok_bad provedin PROOF.bendsource · line 125 · raw

{0xedb848fc7835fe5f9d34e575a7612788/lib.ColorSample.range_ok_u32(bad_range) == False{} : Bool}

Definitions

def full_range source · line 11 · raw

0xc6ecb72f45a1b2f83318765698582f7f/lib.ColorRange

def narrow source · line 14 · raw

0xc6ecb72f45a1b2f83318765698582f7f/lib.ColorRange

def bad_range source · line 17 · raw

0xc6ecb72f45a1b2f83318765698582f7f/lib.ColorRange

def point source · line 20 · raw

0xc6ecb72f45a1b2f83318765698582f7f/lib.ColorRange