operational semantics for brainfuck

Stream: new members

[Stefan]

Hi!!! So I'm trying to define the operational semantics of Brainfuck, focusing on small step semantics at first, and I'm stuck on defining the core element of the state, which is a memory cell. This memory cell would be the equivalent of a byte, so a natural number strictly smaller than 256. How would I go about defining this in order to later be able to reason about it?

[Matt Diamond]

Fin 256, perhaps?

[Matt Diamond]

also consider docs#Std.BitVec

[Kyle Miller]

docs#UInt8 is Fin 256 but has compiler support where the runtime representation is a byte.

[Stefan]

Thank you for the suggestions!! I'll probably get stuck again and come back

[Stefan]

Hello! While proving a theorem using BigStep semantics I ran into the following case:

case mp
s t : State
h : BigStep (Op.pDec, s) t
⊢ t = State.pDec s

this can be proved with

cases h
. rfl

but it is really not clear to me why we can use cases here.
after using cases the goal and assumptions change to

case mp.pDec
s : State
⊢ State.pDec s = State.pDec s

and I can't really wrap my head around this.

For reference State is defined as follows:

structure BFBand : Type where
  before: List Nat
  current: Nat
  after: List Nat
  deriving Repr

structure State : Type where
  input: List Nat
  output: List String
  band: BFBand
  deriving Repr

pDec is defined as

namespace State

def pDec (s: State): State :=
  let b := s.band
  let newBand :=
    match b.before with
      | [] =>  ⟨[], 0, b.current :: b.after⟩
      | h :: t => ⟨t, h, b.current :: b.after⟩
  ⟨s.input, s.output, newBand⟩

end State

Op is defined as

inductive Op : Type where
  | nop        : Op
  | pInc       : Op
  | pDec       : Op
  | vInc       : Op
  | vDec       : Op
  | brakPair   : Op -> Op
  | seq        : Op -> Op -> Op
  | output     : Op
  | input      : Op

and BigStep.pDec is defined as:

inductive BigStep: Op × State → State → Prop where
| pDec (s: State): BigStep (Op.pDec, s) s.pDec

[Luigi Massacci]

Ignoring for a moment whether you have the right definitions., you can use case because BigStep is an inductive type, and case will essentially be “induction without the inductive hypothesis” (i.e. show that your proposition holds for any possible constructor of your inductive type). You have only one constructor, so Lean reasonably substitutes that in, and t is forced to be s.pDec because that is the only thing that it can be, according to your definition of BigStep.

[Stefan]

I can kind of get behind that, but I only gave the partial definition of BigStep to save some space. Here is the full definition for more context. Why is cases not trying to match the other constructors? Is it immediately obvious that only the pDec constructor can be matched?

inductive BigStep: Op × State → State → Prop where
  | nop  (s: State): BigStep (Op.nop, s)  s
  | pInc (s: State): BigStep (Op.pInc, s) s.pInc
  | pDec (s: State): BigStep (Op.pDec, s) s.pDec
  | vInc s:
      BigStep (Op.vInc, s) (
        let b := s.band
        ⟨s.input, s.output, ⟨b.before, b.current + 1, b.after⟩⟩)
  | vDec s:
      BigStep (Op.vDec, s) (
        let b := s.band
        ⟨s.input, s.output, ⟨b.before, b.current - 1, b.after⟩⟩)
  | brakPairTrue {ops} {s t u: State} (c: s.dereference ≠ 0)
    (body: BigStep (ops, s) t)
    (rest: BigStep ((Op.brakPair ops), t) u):
      BigStep (Op.brakPair ops, s) u
  | brakPairFalse ops (s: State) (c: s.dereference = 0):
      BigStep (Op.brakPair ops, s) s
  | seq (ops1 s ops2 t u)
    (h:  BigStep (ops1, s) t)
    (h': BigStep (ops2, t) u):
      BigStep ((Op.seq ops1 ops2), s) u
  | input s:
      BigStep (Op.input, s) (
        let b := s.band
        match s.input with
          | [] => ⟨[],
                   "<<error occurred: Not enough input>>" :: s.output,
                   ⟨b.before, 0, b.after⟩⟩
          | h :: t => ⟨t, s.output, ⟨b.before, h, b.after⟩⟩)
  | output s:
      BigStep (Op.output, s) (
        let b := s.band
        let c := (Char.ofNat b.current).toString
        ⟨s.input, c :: s.output, b⟩)

[Stefan]

Hi again! I have the big step semantics defined for my language and I'm trying to write a proof for a swap operation. More concretely, if the sequence of operations is OPS and the initial state is s := {[], 0, [x, y]}, then (OPS, s) ==> {[], 0, [y, x]}. Unfortunately I'm stuck midway through, proving the following lemma:

(OPS', { [0], k, [] }) ==> { [k], 0, [] } -> (OPS', { [1], k, [] }) ==> { [1 + k], 0, [] }

here OPS' is the form (Op.brakPair ops), which would be the equivalent of while (s.current != 0) { ops } in a C-like language and s.current is the non-list field of a state.

I don't really have any idea on how to approach this.

[Mario Carneiro]

I don't see any reason why that implication would be true

[Mario Carneiro]

It seems like you have the wrong inductive hypothesis

[Mario Carneiro]

Do you have a theorem statement?

[Stefan]

I suspect I wasn't clear enough in my explanation. OPS are not generic operations, but a particular set that should indeed swap two numbers. I also edited the previous message with a clarification changing OPS to OPS' in the lemma. The implication should now make more sense. Also, here is the full theorem statement:

def bfSwapTX: Op := >_[<_+_>_-]
def bfSwapXY: Op := >_[<_+_>_-]
def bfSwapYT: Op := <_<_[>_>_+_<_<_-]
def bfSwap: Op := (bfSwapTX)_(bfSwapXY)_(bfSwapYT)

theorem swap {x y: Nat}: (bfSwap, (State.mk [] 0 [x, y])) ⟹ State.mk [] 0 [y, x] := sorry

[Mario Carneiro]

from what I can tell the inductive hypotheses for the three loops are:

([<_+_>_-], (State.mk (a :: l) b r)) ⟹ State.mk (a+b :: l) 0 r -- loops bfSwapTX and bfSwapXY
([>_>_+_<_<_-], (State.mk l a (y :: b :: r))) ⟹ State.mk l 0 (y :: a+b :: r) -- bfSwapYT

[Mario Carneiro]

you prove the first one by induction on b generalizing a, and the second one by induction on a generalizing b

[Mario Carneiro]

and the rest is just forward simulation

[Stefan]

You are correct. Where I get stuck is on the successor step in the induction:

case succ
l r : List Nat
a k : Nat
t : (Op.brakPair (<_+_>_-), { before := a :: l, current := k, after := r } ) ⟹ { before := (a + k) :: l, current := 0, after := r }
⊢ (Op.brakPair (<_+_>_-), { before := a :: l, current := Nat.succ k, after := r }) ⟹  { before := (a + Nat.succ k) :: l, current := 0, after := r }

It's probably trivial, but I don't know how to progress with the proof from this step onwards

[Mario Carneiro]

you should apply brakPairTrue there

[Mario Carneiro]

you forgot to generalizing a there though

[Mario Carneiro]

because you need to apply the inductive hypothesis with a+1 in place of a

[Stefan]

Thank you very much for the input!! Could you guide to where I could see some examples using generalizing and/or some info on how to use it? This is new to me

[Mario Carneiro]

induction b generalizing a

[Stefan]

I got it, thank you very much for the help!

[Stefan]

I'm now trying to parse a string into an Op, but can't figure how to prove termination

Op is defined as follows:

inductive Op : Type where
  | nop        : Op
  | pInc       : Op
  | pDec       : Op
  | vInc       : Op
  | vDec       : Op
  | brakPair   : Op -> Op
  | seq        : Op -> Op -> Op
  | output     : Op
  | input      : Op

so far I've tried:

def fromString (s: String): Op :=
  parse (s.toUTF8.toList)
where
  parse (chrl: List UInt8): Op :=
    match chrl with
    | [] => nop
    | h :: t =>
      match h with
      | 62 => Op.seq Op.pInc   (parse t)        -- 62 >
      | 60 => Op.seq Op.pDec   (parse t)        -- 60 <
      | 43 => Op.seq Op.vInc   (parse t)        -- 43 +
      | 45 => Op.seq Op.vDec   (parse t)        -- 45 -
      | 46 => Op.seq Op.output (parse t)        -- 46 .
      | 59 => Op.seq Op.input  (parse t)        -- 59 ;
      | 91 =>                                   -- 91 [
        let head := t.takeWhile (λ x => x ≠ 93) -- 93 ]
        let tail := t.dropWhile (λ x => x ≠ 93) -- 93 ]
        let body := parse head
        let rest := parse tail
        Op.seq (Op.brakPair body) rest
      | _ => parse t -- anything else skip
    termination_by
      fromString s => s
      parse chrl => chrl

termination fails to be proven body and rest

[Joachim Breitner]

Can you, in prose, say why you think parse is terminating?

[Stefan]

Yes. With every recursive call the passed char list will be at least one character smaller in size. in the 91 case, len(head) + len(tail) = len(t), so again, the amount of chars processed will decrease. Execution stops when an empty list is reached.

[Joachim Breitner]

Ok, but that is a sizeable amount of arguing, and beyond what lean can do by default for you these days.

The first thing you need to do is to tell lean that you expect the length of the list to be decreasing (and no the size, which takes the “size” of the charaters into account):

      parse chrl => chrl.length

[Joachim Breitner]

Now the error message will be

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
h: UInt8
t: List UInt8
head: List UInt8 := List.takeWhile (fun x => decide (x ≠ 93)) t
⊢ List.length (List.takeWhile (fun x => !decide (x = 93)) t) < Nat.succ (List.length t)

[Stefan]

After trying that the error persists and I get the following message:

failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal
h : UInt8
t : List UInt8
head : List UInt8
⊢ List.length (List.takeWhile (fun x => !decide (x = 93)) t) < Nat.succ (List.length t)

If there is no other option, I would attempt prooving what's suggested, but don't understand what the exact syntax for beginning the poof should be. However, if you have other ideas to share, I would very much appreciate it

[Joachim Breitner]

Normally it should work to prove the relevant relations right in the code, e.g.

      | 91 =>                                   -- 91 [
        let head := t.takeWhile (λ x => x ≠ 93) -- 93 ]
        have h1 : head.length < t.length.succ := sorry
        let tail := t.dropWhile (λ x => x ≠ 93) -- 93 ]
        have h2 : tail.length < t.length.succ := sorry
        let body := parse head
        let rest := parse tail
        Op.seq (Op.brakPair body) rest

But in this case, there is some annoyance that (λ x => x ≠ 93) gets rewritten to (fun x => !decide (x = 93)) and and now assumption doesn’t work. You can work around it by writing

    decreasing_by first | decreasing_tactic | simp_wf; simp only [ne_eq, decide_not] at *; assumption

(IMHO this is a bug, the simp_wf in the default decreasing_tactic should only unfold wf stuff but otherwise leave the goal as it as far as possible).

[Stefan]

Thank you very much!

[Stefan]

I managed to finalize the proofs