Chip8-specification.kane

Stack
  empty    : Π(τ:U) Stack_(τ,Z)
  push     : Π(τ:U, t:τ, s:Stack_(τ,n)) Stack_(τ,n+1)
  pop      : Π(τ:U, s:Stack_(τ,S(n))) (τ × Stack_(τ,n))
  pop_push : Π(τ:U, s:Stack_(τ,n), i:τ) (pop ∘ push i) s ≡ i × s

Vector
  peek      : Π(τ:U, n:N, i:Fin_n, Vector_(τ,i)) τ
  poke      : Π(τ:U, n:N, i:Fin_n, t:τ, Vector_(τ,i)) Vector_(τ,i)
  peek_poke : Π(τ:U, n:N, i:Fin_n, v:Vector_(τ,i), t:τ) (peek i ∘ poke i t) v ≡ t

Chip8
  pc        : Chip8 → W_12
  i         : Chip8 → W_12
  st        : Chip8 → W_8
  dt        : Chip8 → W_8
  stack     : Chip8 → Stack_W12
  registers : Chip8 → Vector_(W_8,W_16)
  memory    : Chip8 → Vector_(W_8,Fin_4096)
  inputs    : Chip8 → Vector_(W_1,W_16)
  display   : Chip8 → Vector_(W_1,Fin_64 × Fin_32)

  nibbles : Π(c:Chip8) 
    let 
      b_0 ≜ peek (pc c) (memory c)
      b_1 ≜ peek (pc c + 1) (memory c)
    in  
      Σ(n:Vector_(W_4,4))
        × n 0 ≡ slice 0 4 b_0
        × n 1 ≡ slice 4 8 b_0
        × n 2 ≡ slice 0 4 b_1
        × n 3 ≡ slice 4 8 b_1

  step_pc : Π(c:Chip8, c':Chip8) 
    pc c' ≡ pc c + 2

  skip_pc : Π(c:Chip8, c':Chip8) 
    pc c' ≡ pc c + 4

  display_cleared : Π(c:Chip8, p:Fin_64 × Fin_32) 
    peek p (display c) ≡ 0

  sprite_rendered : Π(c:Chip8, c':Chip8, x:W_6, y:W_32, n:W_8) 
    Π(b:Fin_(8*n))
      let 
        x_n ≜ b%8
        y_n ≜ b/8
        p   ≜ x+x_n × y+y_n
        o   ≜ (i c)+y_n
      in  
        display p c' ≡ display p c ⊕ memory c o j

  unchanged : Π(τ:U, a:τ, b:τ, i:N, v:Vector_(Σ(σ:U) τ → σ, Fin i))
    Π(n:Fin i) 
      let 
        f ≜ π_2 (v n)
      in
        f a ≡ f b

  step : Chip8 → Chip8

  step_laws: 
    Π(c:Chip8)
      let 
        <a,x,y,z> ≜ π_1 (nibbles c)
        same      ≜ unchanged Chip8 c c'
        c8'       ≜ step c8
      in 
        -- 00E0 clear display
        + × <0,E,0> ≡ <a,y,z>
          × step_pc c c'
          × display_cleared c8'
          × same 7 <i,st,dt,stack,registers,memory,inputs>

        -- 00EE return from subroutine
        + × <0,E,E> ≡ <a,y,z>
          × <pc c',stack c'> ≡ pop (stack c)
          × same 6 <i,st,dt,registers,memory,inputs>
          
        -- 1NNN jump to nnn
        + × 1 ≡ a
          × pc c' ≡ x++y++z
          × same 8 <i,st,dt,stack,registers,memory,display,inputs>
          
        -- 2NNN call subroutine at nnn
        + × 2 ≡ a
          × stack c' ≡ push (pc c) (stack c)
          × pc c' ≡ x++y++z
          × same 7 <i,st,dt,registers,memory,display,inputs>

        -- 3XNN skip if vx == nn
        + × 3 ≡ a
          × + × registers c x ≡ y++z
              × skip_pc c c'
            + step_pc c c'
          × same 7 <i,st,dt,registers,memory,display,inputs>

        -- 4XNN skip if vx != nn
        + × 4 ≡ a
          × + × registers c x ≡ y++z
              × step_pc c c'
            + skip_pc c c'
          × same 7 <i,st,dt,registers,memory,display,inputs>

        -- 5XY0 skip if vx == vy
        + × 5 ≡ a
          × + × registers c x ≡ registers c y
              × skip_pc c c'
            + step_pc c c'
          × same 7 <i,st,dt,registers,memory,display,inputs>

        -- 6XNN vx = nn
        + × 6 ≡ a
          × step_pc c c'
          × registers c' x ≡ y++z
          × same 7 <i,st,dt,stack,memory,display,inputs>

        -- 7XNN vx = vx + nn
        + × 7 ≡ a
          × step_pc c c'
          × registers c' x ≡ registers c x + y++z
          × same 7 <i,st,dt,stack,memory,display,inputs>

        -- 8XY0 vx = vy
        + × <8,0> ≡ <a,z>
          × step_pc c c'
          × registers c' x ≡ registers c y 
          × same 7 <i,st,dt,stack,memory,display,inputs>

        -- 8XY1 vx = vx | vy
        + × <8,1> ≡ <a,z>
          × step_pc c c'
          × registers c' x ≡ registers c x | registers c y 
          × same 7 <i,st,dt,stack,memory,display,inputs>

        -- 8XY2 vx = vx & vy
        + × <8,2> ≡ <a,z>
          × step_pc c c'
          × registers c' x ≡ registers c x & registers c y 
          × same 7 <i,st,dt,stack,memory,display,inputs>

        -- 8XY3 vx = vx ⊕ vy
        + × <8,3> ≡ <a,z>
          × step_pc c c'
          × registers c' x ≡ registers c x ⊕ registers c y 
          × same 7 <i,st,dt,stack,memory,display,inputs>

        -- TODO: HANDLE CARRY BIT PORTION OF THIS THING
        -- 8XY4 vx = vx = vx + vy
        + × <8,4> ≡ <a,z>
          × step_pc c c'
          × registers c' x ≡ registers c x + registers c y 
          × same 7 <i,st,dt,stack,memory,display,inputs>

        -- TODO: HANDLE BORROW BIT PORTION OF THIS THING
        -- 8XY5 vx = vx = vx - vy
        + × <8,5> ≡ <a,z>
          × step_pc c c'
          × registers c' x ≡ registers c x - registers c y 
          × same 7 <i,st,dt,stack,memory,display,inputs>

        -- 8XY6 vx = vx >> 1. vf = lsb
        + × <8,6> ≡ <a,z>
          × step_pc c c'
          × registers c' x ≡ registers c x - registers c y 
          × same 7 <i,st,dt,stack,memory,display,inputs>
          
        -- ANNN i = nnn
        + × A ≡ a
          × step_pc c c'
          × i c' ≡ x++y++z
          × same 7 <st,dt,stack,memory,display,inputs>

        -- DXYN draw sprite of height n at x,y
        + × D ≡ a
          × step_pc c c'
          × sprite_rendered c c' x y z
          × same 7 <i,st,dt,stack,registers,memory,inputs
        ...