~/bend-docscommunity

LAWS.bend open laws/TODOs

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

Definitional laws for Vec2.

Base F32 arithmetic is opaque to Bend's definitional equality. Therefore the exact laws below preserve F32.add/sub/mul/dot normal forms rather than making false claims that those primitives normalize to mathematical real arithmetic. They still lock down constructors, projections, component placement, and the concrete expansion of the usual vector identities.

2 imports
import Base
import ./lib.bend as V

Laws

law make_ctor provedin PROOF.bendsource · line 11 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(1.0, 2.0) == 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2{1.0, 2.0} : 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2}

law zero_ctor provedin PROOF.bendsource · line 14 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.zero == 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2{0.0, 0.0} : 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2}

law unit_x_ctor provedin PROOF.bendsource · line 17 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.unit_x == 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2{1.0, 0.0} : 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2}

law unit_y_ctor provedin PROOF.bendsource · line 20 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.unit_y == 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2{0.0, 1.0} : 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2}

law x_projection provedin PROOF.bendsource · line 23 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.x(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(3.0, 4.0)) == 3.0 : F32}

law y_projection provedin PROOF.bendsource · line 26 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.y(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(3.0, 4.0)) == 4.0 : F32}

law add_zero provedin PROOF.bendsource · line 30 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.add(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(3.0, 4.0), 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.zero) == 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2{F32.add(3.0, 0.0), F32.add(4.0, 0.0)} : 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2}

add zero, stated at the exact F32 normal form available to Base.

law scale_one provedin PROOF.bendsource · line 38 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.scale(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(3.0, 4.0), 1.0) == 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2{F32.mul(3.0, 1.0), F32.mul(4.0, 1.0)} : 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2}

scale one, stated at the exact F32 normal form available to Base.

law sub_self provedin PROOF.bendsource · line 45 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.sub(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(3.0, 4.0), 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(3.0, 4.0)) == 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2{F32.sub(3.0, 3.0), F32.sub(4.0, 4.0)} : 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2}

law dot provedin PROOF.bendsource · line 52 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.dot(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(3.0, 4.0), 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(2.0, 5.0)) == F32.add(F32.mul(3.0, 2.0), F32.mul(4.0, 5.0)) : F32}

law length_sq provedin PROOF.bendsource · line 59 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.length_sq(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(3.0, 4.0)) == F32.add(F32.mul(3.0, 3.0), F32.mul(4.0, 4.0)) : F32}

law lerp provedin PROOF.bendsource · line 66 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.lerp(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(0.0, 2.0), 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(10.0, 6.0), 0.25) == 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.add(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(0.0, 2.0), 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.scale(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.sub(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(10.0, 6.0), 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.make(0.0, 2.0)), 0.25)) : 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2}

law unit_x_dot_unit_y provedin PROOF.bendsource · line 77 · raw

{0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.dot(0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.unit_x, 0xab5b72f8eac09d083aa0b359ebe0a970/lib.Vec2.unit_y) == F32.add(F32.mul(1.0, 0.0), F32.mul(0.0, 1.0)) : F32}