app_triangle_2d: PROOF.bend passes after an edit that stops presses on the triangle from counting #1981

What you did

bend PROOF.bend in demos/app_triangle_2d, after editing only main.bend. This is the follow-up #1931 left for its own issue. LAWS.bend and PROOF.bend are unchanged.

@@ -17,10 +17,13 @@
 def Tri.side(+ax: U32, +ay: U32, bx: U32, by: U32, px: U32, py: U32) -> Bool:
   ((bx - ax) * (py - ay) - (by - ay) * (px - ax) > 2147483647 : U32)
 
-def Tri.inside(+x: U32, +y: U32) -> Bool:
+def Tri.shape(+x: U32, +y: U32) -> Bool:
   (Tri.side(256, 64, 64, 448, x, y) && Tri.side(64, 448, 448, 448, x, y)
     && Tri.side(448, 448, 256, 64, x, y))
 
+def Tri.inside(+x: U32, +y: U32) -> Bool:
+  False{}
+
 def Tri.out(
   +ax: U32, +ay: U32, +bx: U32, +by: U32, +x0: U32, +y0: U32, +x1: U32,
   +y1: U32
@@ -29,7 +32,7 @@
     || Tri.side(ax, ay, bx, by, x0, y1) || Tri.side(ax, ay, bx, by, x1, y1)))
 
 def Tri.color(+x: U32, +y: U32, n: U32) -> U32:
-  Tri.pick(Tri.inside(x, y), 16744499,
+  Tri.pick(Tri.shape(x, y), 16744499,
     Tri.pick(((y < 8) && (x < 16 * n) && U32.is_eq((x .&. 8 : U32), 0) : U32),
       16777215, 3362125))
 
@@ -39,8 +42,8 @@
   +y1 = (y0 + s : U32)
   +strip = ((y0 < 8) && (x0 < 16 * n) : U32)
   (strip && (s <= 8 : U32)) || (Bool.not(strip)
-    && ((Tri.inside(x0, y0) && Tri.inside(x1, y0) && Tri.inside(x0, y1)
-        && Tri.inside(x1, y1))
+    && ((Tri.shape(x0, y0) && Tri.shape(x1, y0) && Tri.shape(x0, y1)
+        && Tri.shape(x1, y1))
       || Tri.out(256, 64, 64, 448, x0, y0, x1, y1)
       || Tri.out(64, 448, 448, 448, x0, y0, x1, y1)
       || Tri.out(448, 448, 256, 64, x0, y0, x1, y1)))

What happened

On main at 9e8d7b7:

$ bend PROOF.bend
ALL PROOFS CHECK
$ bend PROOF.bend --verdict
ALL PROOFS CHECK
$ bend PIXEL.bend
(256, 300) drawn orange, press -> count 0
(440, 300) drawn teal, press -> count 0

PIXEL.bend reads each color from the quadtree Tri.view draws. The page still draws the triangle at (256, 300), but a press there no longer counts. On the unedited demo, the first line ends in count 1.

Why it happens

Both click laws state their hypothesis with App.Tri.inside, the test main.bend itself uses, and PROOF.bend rewrites with that hypothesis. So the laws hold whatever Tri.inside is. #1915 and #1932 fixed the same shape in four other demos; #1931 left this one out because it needed a choice: the drawing lives in main.bend too.

The file

import Base
import ./main.bend as App

def at.pick(right: Bool, down: Bool, tl: Image, tr: Image, bl: Image, br: Image) -> Image:
  match right down:
    case False{} False{}:
      tl
    case True{} False{}:
      tr
    case False{} True{}:
      bl
    case True{} True{}:
      br

# the color the page draws at (x, y), read from the quadtree of depth d
def at(d: Nat, img: Image, +x: U32, +y: U32) -> U32:
  match d img:
    case _ Pix{c}:
      c
    case 0n Qua{tl, tr, bl, br}:
      0
    case 1n++e Qua{tl, tr, bl, br}:
      +h = U32.shln(1, e)
      at(e, at.pick((x >= h : U32), (y >= h : U32), tl, tr, bl, br),
        (x .&. (h - 1) : U32), (y .&. (h - 1) : U32))

def name.if(orange: Bool, teal: Bool) -> String:
  match orange teal:
    case True{} _:
      "orange"
    case False{} True{}:
      "teal"
    case False{} False{}:
      "other"

def name(+c: U32) -> String:
  name.if(U32.is_eq(c, 16744499), U32.is_eq(c, 3362125))

def drawn.at(+x: U32, +y: U32, v: U32 & Image) -> String:
  (n, img) = v
  name(at(9n, img, x, y))

def drawn(+x: U32, +y: U32) -> String:
  drawn.at(x, y, App.Tri.view(0))

def counted(r: Maybe<U32>) -> String:
  match r:
    case Some{n}: U32.show(n)
    case None{}: "quit"

def main() -> IO(Unit):
  do IO<Unit>:
    IO.print("(256, 300) drawn " ++ drawn(256, 300) ++ ", press -> count " ++ counted(App.Tri.event(Press{0, Tool.Mouse{}, 256.0, 300.0, 0, 0, True{}}, 0)))
    IO.print("(440, 300) drawn " ++ drawn(440, 300) ++ ", press -> count " ++ counted(App.Tri.event(Press{0, Tool.Mouse{}, 440.0, 300.0, 0, 0, True{}}, 0)))

A fix, and what it leaves

#1982 adds SPEC.bend with the triangle's corners and points both laws at Spec.inside. main.bend keeps its own Tri.inside. I considered having main.bend import Spec.inside instead, and went with 1570e07's direction, where pure_par_sum kept its own pow2 so that "SPEC.bend no longer reaches into the program". PROOF.bend doesn't change: the checker unfolds Spec.inside and Tri.inside to the same expression, so the rewrite still applies, and the edit above now fails at Laws.click_inside.

What it leaves: the laws pin which presses count, not where the triangle is drawn. Moving only the drawing still checks. With Tri.color testing Tri.inside((x - 100 : U32), y), PIXEL.bend prints (256, 300) drawn teal, press -> count 1 and (440, 300) drawn orange, press -> count 0. Pinning the picture would take a law about Tri.view's quadtree, which means proving that every cell Tri.flat paints in one color lies inside the triangle. That looks out of reach to me, so the PR narrows the two law comments to "SPEC.bend's triangle", as #1915 scoped the flag law.

pure_hvm5_mini and app_slash_boss_3d, also named in #1931, are still to check. I'll file them separately if they have the same gap.

bend version

Bend 2.0.39 (main at 9e8d7b7)

uname -sm

Darwin arm64

clang --version (the first line)

Apple clang version 21.0.0 (clang-2100.1.1.101)