prometeu-runtime/docs/specs/pbs/files/PRs para Junie.md

PR-02 — PBS Prelude: Add SAFE builtins for Color / ButtonState / Pad / Touch (bounded)

Goal

Expose hardware types to PBS scripts as value structs using bounded (no u16).

Required PBS definitions (in prelude / hardware module)

Put these in the standard library surface that PBS sees without user creating them.

pub declare struct Color(value: bounded)
[
  (r: int, g: int, b: int): (0b) as rgb
  {
    ...
  }
]
[[
  BLACK: (...) {}
  WHITE: (...) {}
  RED: (...) {}
  GREEN: (...) {}
  BLUE: (...) {}
  MAGENTA: (...) {}
  TRANSPARENT: (...) {}
  COLOR_KEY: (...) {}
]]
{
  pub fn raw(self: Color): bounded;
}

pub declare struct ButtonState(
  pressed: bool,
  released: bool,
  down: bool,
  hold_frames: bounded
)

pub declare struct Pad(
  up: ButtonState,
  down: ButtonState,
  left: ButtonState,
  right: ButtonState,
  a: ButtonState,
  b: ButtonState,
  x: ButtonState,
  y: ButtonState,
  l: ButtonState,
  r: ButtonState,
  start: ButtonState,
  select: ButtonState
)
{
  pub fn any(self: Pad): bool;
}

pub declare struct Touch(
  f: ButtonState,
  x: int,
  y: int
)

Semantics / constraints

• Color.value stores the hardware RGB565 raw as bounded.
• hold_frames is bounded.
• x/y remain int.

Implementation notes (binding)

• Color.rgb(r,g,b) must clamp inputs to 0..255 and then pack to RGB565.
• Color.raw() returns the internal bounded.
• Pad.any() must be a pure SAFE function compiled normally (no hostcall).

Tests (mandatory)

• FE/typecheck: Color.WHITE is a Color.
• FE/typecheck: Gfx.clear(Color.WHITE) typechecks.
• FE/typecheck: let p: Pad = Input.pad(); if p.any() { } typechecks.

Non-goals

• No heap types
• No gates

---

PR-03 — Lowering: Host Contracts for Gfx/Input using deterministic syscalls

Goal

Map PBS host contracts to stable syscalls with a deterministic ABI.

Required host contracts in PBS surface

pub declare contract Gfx host
{
  fn clear(color: Color): void;
}

pub declare contract Input host
{
  fn pad(): Pad;
  fn touch(): Touch;
}

Required lowering rules

1. Gfx.clear(color)

• Emit SYSCALL_GFX_CLEAR
• ABI: args = [Color.raw] as bounded
• returns: void

2. Input.pad()

• Emit SYSCALL_INPUT_PAD
• args: none
• returns: flattened Pad in field order as declared

3. Input.touch()

• Emit SYSCALL_INPUT_TOUCH
• args: none
• returns: flattened Touch in field order as declared

Flattening order (binding)

ButtonState returns 4 slots in order:

1. pressed (bool)
2. released (bool)
3. down (bool)
4. hold_frames (bounded)

Pad returns 12 ButtonState blocks in this exact order: up, down, left, right, a, b, x, y, l, r, start, select

Touch returns:

1. f (ButtonState block)
2. x (int)
3. y (int)

Tests (mandatory)

• Lowering golden test: Gfx.clear(Color.WHITE) emits SYSCALL_GFX_CLEAR with 1 arg.
• Lowering golden test: Input.pad() emits SYSCALL_INPUT_PAD and assigns to local.
• Lowering golden test: Input.touch() emits SYSCALL_INPUT_TOUCH.

Non-goals

• No runtime changes
• No VM heap

---

PR-04 — Runtime: Implement syscalls for Color/Gfx and Input pad/touch + integration cartridge

Goal

Make the new syscalls actually work and prove them with an integration test cartridge.

Required syscall implementations

1) SYSCALL_GFX_CLEAR

• Read 1 arg: bounded raw color

• Convert to u16 internally (runtime-only)

  • If raw > 0xFFFF, trap TRAP_OOB or TRAP_TYPE (choose one and document)

• Fill framebuffer with that RGB565 value

2) SYSCALL_INPUT_PAD

• No args

• Snapshot the current runtime Pad and push a flattened Pad return:

  • For each button: pressed, released, down, hold_frames
  • hold_frames pushed as bounded

3) SYSCALL_INPUT_TOUCH

• No args

• Snapshot Touch and push flattened Touch return:

  • f ButtonState
  • x int
  • y int

Integration cartridge (mandatory)

Add test-cartridges/hw_hello (or similar) with:

fn frame(): void
{
  // 1) clear screen white
  Gfx.clear(Color.WHITE);

  // 2) read pad and branch
  let p: Pad = Input.pad();
  if p.any() {
    Gfx.clear(Color.MAGENTA);
  }

  // 3) read touch and branch on f.down
  let t: Touch = Input.touch();
  if t.f.down {
    // choose a third color to prove the struct returned correctly
    Gfx.clear(Color.BLUE);
  }
}

Acceptance criteria

• Cartridge runs without VM faults.
• With no input: screen is WHITE.
• With any pad button held: screen becomes MAGENTA.
• With touch f.down: screen becomes BLUE.

Tests (mandatory)

• Runtime unit test: SYSCALL_GFX_CLEAR rejects raw > 0xFFFF deterministically.
• Runtime unit test: SYSCALL_INPUT_PAD returns correct number of stack slots (48).
• Runtime unit test: SYSCALL_INPUT_TOUCH returns correct number of stack slots (4 + 2 = 6).

---