LAWS.bend open laws/TODOs

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

Definitional laws for Color layer 1.

Honest scope: Base F32 primitives (add/mul/div/show/cmp/clamp/...) are opaque to definitional equality. Therefore rgb_to_hsl / hsl_to_rgb roundtrips, F32.clamp-based field updates, and Color.range_valid (which uses F32.is_le on alpha) are NOT stated as {==} laws. Runtime smoke for converts lives in main.bend. Laws below are only claims that normalize under Bend 2.0.2.

2 imports

import Base
import ./lib.bend as C

Laws

law rgb_ctor provedin PROOF.bendsource · line 12 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(10, 20, 30, 1.0) == 0xc6ecb72f45a1b2f83318765698582f7f/lib.Rgb{10, 20, 30, 1.0} : 0xc6ecb72f45a1b2f83318765698582f7f/lib.Rgb}

Constructors equal their data literals.

law hsl_ctor provedin PROOF.bendsource · line 15 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl(120.0, 1.0, 0.5, 1.0) == 0xc6ecb72f45a1b2f83318765698582f7f/lib.Hsl{120.0, 1.0, 0.5, 1.0} : 0xc6ecb72f45a1b2f83318765698582f7f/lib.Hsl}

law range_ctor provedin PROOF.bendsource · line 18 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.range(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(0, 0, 0, 0.0), 0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(1, 2, 3, 1.0)) == 0xc6ecb72f45a1b2f83318765698582f7f/lib.ColorRange{0xc6ecb72f45a1b2f83318765698582f7f/lib.Rgb{0, 0, 0, 0.0}, 0xc6ecb72f45a1b2f83318765698582f7f/lib.Rgb{1, 2, 3, 1.0}} : 0xc6ecb72f45a1b2f83318765698582f7f/lib.ColorRange}

law rgb_r_proj provedin PROOF.bendsource · line 26 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_r(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(10, 20, 30, 1.0)) == 10 : U32}

Constructor projections.

law rgb_g_proj provedin PROOF.bendsource · line 29 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_g(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(10, 20, 30, 1.0)) == 20 : U32}

law rgb_b_proj provedin PROOF.bendsource · line 32 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_b(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(10, 20, 30, 1.0)) == 30 : U32}

law rgb_a_proj provedin PROOF.bendsource · line 35 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_a(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(10, 20, 30, 0.5)) == 0.5 : F32}

law hsl_h_proj provedin PROOF.bendsource · line 38 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl_h(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl(240.0, 0.25, 0.75, 1.0)) == 240.0 : F32}

law hsl_s_proj provedin PROOF.bendsource · line 41 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl_s(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl(240.0, 0.25, 0.75, 1.0)) == 0.25 : F32}

law hsl_l_proj provedin PROOF.bendsource · line 44 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl_l(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl(240.0, 0.25, 0.75, 1.0)) == 0.75 : F32}

law hsl_a_proj provedin PROOF.bendsource · line 47 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl_a(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl(240.0, 0.25, 0.75, 0.25)) == 0.25 : F32}

law clamp_u8_low provedin PROOF.bendsource · line 51 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.clamp_u8(0) == 0 : U32}

U32 clamp helpers.

law clamp_u8_mid provedin PROOF.bendsource · line 54 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.clamp_u8(128) == 128 : U32}

law clamp_u8_high provedin PROOF.bendsource · line 57 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.clamp_u8(255) == 255 : U32}

law clamp_u8_overflow provedin PROOF.bendsource · line 60 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.clamp_u8(300) == 255 : U32}

law clamp_u8_way_over provedin PROOF.bendsource · line 63 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.clamp_u8(1000) == 255 : U32}

law clamp_rgb_r_overflow provedin PROOF.bendsource · line 67 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_r(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.clamp_rgb(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(300, 10, 400, 1.0))) == 255 : U32}

clamp_rgb: only octet projections are definitional (alpha uses F32.clamp).

law clamp_rgb_g_ok provedin PROOF.bendsource · line 70 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_g(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.clamp_rgb(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(300, 10, 400, 1.0))) == 10 : U32}

law clamp_rgb_b_overflow provedin PROOF.bendsource · line 73 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb_b(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.clamp_rgb(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(300, 10, 400, 1.0))) == 255 : U32}

law rgba_string_red provedin PROOF.bendsource · line 78 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.to_rgba_string(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(255, 0, 0, 1.0)) == String.append("rgba(255,0,0,", String.append(F32.show(1.0), ")")) : String}

Stable rgba/hsla string shape. U32.show reduces; F32.show stays symbolic, so both sides keep matching F32.show calls.

law rgba_string_black provedin PROOF.bendsource · line 85 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.to_rgba_string(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(0, 0, 0, 0.0)) == String.append("rgba(0,0,0,", String.append(F32.show(0.0), ")")) : String}

law rgba_string_custom provedin PROOF.bendsource · line 92 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.to_rgba_string(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(12, 34, 56, 0.5)) == String.append("rgba(12,34,56,", String.append(F32.show(0.5), ")")) : String}

law rgba_starts_with_prefix provedin PROOF.bendsource · line 99 · raw

{String.starts_with(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.to_rgba_string(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.rgb(255, 128, 64, 1.0)), "rgba(") == True{} : Bool}

law hsla_string_green provedin PROOF.bendsource · line 108 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.to_hsla_string(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl(120.0, 1.0, 0.5, 1.0)) == String.append("hsla(", String.append(F32.show(120.0), String.append(",", String.append(F32.show(1.0), String.append(",", String.append(F32.show(0.5), String.append(",", String.append(F32.show(1.0), ")")))))))) : String}

law hsla_string_zero provedin PROOF.bendsource · line 116 · raw

{0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.to_hsla_string(0xc6ecb72f45a1b2f83318765698582f7f/lib.Color.hsl(0.0, 0.0, 0.0, 0.0)) == String.append("hsla(", String.append(F32.show(0.0), String.append(",", String.append(F32.show(0.0), String.append(",", String.append(F32.show(0.0), String.append(",", String.append(F32.show(0.0), ")")))))))) : String}