State machine exercises

SoftwareFoundations2/StackMachine/Compile.lean

@@ -6,23 +6,26 @@ def AExp.compile : AExp → List Instruction
   | ANum n       => [ PUSH n ]
   | AId x        => [ LOAD x ]
   | AMult a1 a2  => a1.compile ++ a2.compile ++ [ MUL ]
-  | AMinus a1 a2 => sorry
-  | APlus a1 a2  => sorry
+  | AMinus a1 a2 => a1.compile ++ a2.compile ++ [ SUB ]
+  | APlus a1 a2  => a1.compile ++ a2.compile ++ [ ADD ]
 
 def BExp.compile : BExp → List Instruction
   | BTrue        => [ PUSH 1 ]
   | BFalse       => [ PUSH 0 ]
   | BEq a1 a2    => a1.compile ++ a2.compile ++ [ EQ ]
-  | BNeq a1 a2   => sorry
+  | BNeq a1 a2   => a1.compile ++ a2.compile ++ [ EQ, ISZERO ]
   | BLe a1 a2    => a1.compile ++ a2.compile ++ [ .LE ]
-  | BGt a1 a2    => sorry
-  | BNot b       => sorry
-  | BAnd b1 b2   => sorry
+  | BGt a1 a2    => a1.compile ++ a2.compile ++ [ .LE, ISZERO ]
+  | BNot b       => b.compile ++ [ISZERO]
+  | BAnd b1 b2   => b1.compile ++ b2.compile ++ [ MUL ]
 
 def Com.compileOffset (pcOffset : ℕ) : Com → List Instruction
-  | CSkip       => sorry
-  | CAsgn x a   => sorry
-  | CSeq c1 c2  => sorry
+  | CSkip       => [ NOP ]
+  | CAsgn x a   => a.compile ++ [ STORE x ]
+  | CSeq c1 c2  =>
+      let c1c := c1.compileOffset pcOffset
+      let c2c := c2.compileOffset (pcOffset + c1c.length)
+      c1c ++ c2c
   | CIf b c1 c2 =>
       -- See comment below for stack layout
       let bCode := b.compile
@@ -47,7 +50,7 @@ def Com.compileOffset (pcOffset : ℕ) : Com → List Instruction
 def Com.compile (com : Com) := com.compileOffset 0 ++ [.STOP]
 
 /-
-  Stack layout for a compiled `if b then l1 else l2`.
+  Code layout for a compiled `if b then l1 else l2`.
   First column: code section;
   Second column: offset within the code.
 
@@ -64,22 +67,19 @@ def Com.compile (com : Com) := com.compileOffset 0 ++ [.STOP]
       JUMP             pcOffset + bCode.length + l1.length + l2.length + 7
                        pcOffset + bCode.length + l1.length + l2.length + 8   { == pcJumpPost }
 
-  Stack layout for a compiled `while b do l od`:
+  Code layout for a compiled `while b do l od`:
 
       bCode            pcOffset                                              { == pcCheck }
       pcJumpTrue       pcOffset + bCode.length
       JUMPI            pcOffset + bCode.length + 1
-      pcJumpPost       pcOffset + bCode.length + 2      
+      pcJumpPost       pcOffset + bCode.length + 2
       JUMP             pcOffset + bCode.length + 3
       l                pcOffset + bCode.length + 4                           { == pcJumpTrue }
       pcCheck          pcOffset + bCode.length + l.length + 4
       JUMP             pcOffset + bCode.length + l.length + 5
                        pcOffset + bCode.length + l.length + 6                { == pcJumpPost }
 -/
 
-/-
-  Uncomment after filling all sorries:
-
 #eval aexp⟨{ (x * 2) - 1 + 30 }⟩.compile
 #eval aexp⟨{ x - (2 * y) }⟩.compile
 #eval ⟨{
@@ -136,4 +136,3 @@ def Com.compile (com : Com) := com.compileOffset 0 ++ [.STOP]
   pc    := 0,
   mem   := [ "x" ↦ 161 ],
 })
--/

SoftwareFoundations2/StackMachine/Lemmas.lean

@@ -15,42 +15,122 @@ attribute [local simp] fetchInstr
 attribute [local simp] stackPeek2
 attribute [local simp] stackPeek1
 
-set_option warn.sorry false in
 lemma isErrorLemma {err st'} : ¬ Reachable (.error err) st' := by
-  sorry
+  intros h
+  generalize eq : (Except.error err) = st at h
+  induction h with
+  | step h => cases eq
+  | trans s1 s2 ih1 ih2 =>
+    cases eq
+    simp only [imp_false, not_true_eq_false] at ih1
 
-set_option warn.sorry false in
 lemma isOOFLemma {st} : ¬ Reachable st (.error .OutOfFuel) := by
-  sorry
+  intros h
+  generalize eq : (Except.error ExecutionException.OutOfFuel) = st' at h
+  induction h with
+  | @step μ _ h =>
+    cases eq
+    simp [step, Bind.bind, Except.bind] at h
+    aesop
+  | trans s1 s2 ih1 ih2 =>
+    cases eq
+    simp only [imp_false, not_true_eq_false] at ih2
 
-set_option warn.sorry false in
 lemma isFinalStepLemma {μ st} (h : isFinal (.ok μ)) :
     step μ = st → isError st := by
-  sorry
+  rw [isFinal] at h
+  simp only [step, bind, Except.bind, fetchInstr, h, Nat.lt_irrefl, ↓reduceDIte]
+  intro h1
+  rw [←h1, isError]
+  trivial
 
-set_option warn.sorry false in
 lemma isFinalLemma {st st'} (h : isFinal st) :
     Reachable st st' → isError st' := by
-  sorry
+  intro h
+  induction h with
+  | @step μ st'' hx =>
+    exact isFinalStepLemma h hx
+  | @trans _ stx st'' s1 s2 ih1 ih2 =>
+    apply ih1 at h
+    cases st'' with
+    | ok => contradiction
+    | error e =>
+      have := @isErrorLemma e stx
+      contradiction
 
-set_option warn.sorry false in
 lemma executeFinal {μ st fuel} (h : isFinal (.ok μ)) :
     execute fuel μ = st → st = .ok μ := by
-  sorry
+  intro h1
+  rw [execute.eq_def] at h1
+  simp [h] at h1
+  symm
+  assumption
 
-set_option warn.sorry false in
 lemma executeExtend {μ μ' fuel} (h : step μ = .ok μ') :
     execute (fuel + 1) μ = execute fuel μ' := by
-  sorry
+  rw [execute]
+  by_cases hx : μ.pc < μ.code.length
+  · rw [h]
+    by_cases hf : isFinal (Except.ok μ)
+    · rw [isFinal] at hf
+      aesop
+    · simp [hf]
+  · simp [step, hx, Bind.bind, Except.bind] at h
 
-set_option warn.sorry false in
 lemma executeStepFinal {μ st} (h1 : isFinal st) (h2 : step μ = st) :
     execute 1 μ = st := by
-  sorry
+    rw [execute]
+    by_cases hx : μ.pc < μ.code.length
+    · have hf : ¬ isFinal (Except.ok μ) := by
+        rw [isFinal]
+        intro habs
+        rw [habs] at hx
+        exact Nat.lt_irrefl μ.code.length hx
+      rw [h2]
+      simp only [hf, ↓reduceIte]
+      cases st with
+      | ok μ' =>
+        simp only [execute, ite_eq_left_iff, reduceCtorEq, imp_false, Decidable.not_not]
+        exact h1
+      | error => contradiction
+    · simp only [step, bind, Except.bind, fetchInstr, hx, ↓reduceDIte] at h2
+      rw [←h2] at h1
+      contradiction
+
+lemma executeLemmaAux {n : Nat} {μ μ' : MachineState} (h : Reachable (.ok μ) (.ok μ'))
+  : ∃m, execute m μ = execute n μ' := by
+  generalize eq1 : Except.ok μ = st at h
+  generalize eq2 : Except.ok μ' = st' at h
+  induction h generalizing n μ μ' with
+  | step hs =>
+    cases eq1
+    cases eq2
+    use n + 1
+    exact executeExtend hs
+  | @trans _ _ sti _ _ ih1 ih2 =>
+    cases eq1
+    cases eq2
+    simp only [Except.ok.injEq, forall_eq_apply_imp_iff] at *
+    cases sti with
+    | error x =>
+      have := @isErrorLemma x (Except.ok μ')
+      contradiction
+    | ok μi =>
+      specialize @ih2 n μi rfl
+      obtain ⟨m2, hm2⟩ := ih2
+      specialize @ih1 m2 μ μi rfl rfl
+      obtain ⟨m1, hm1⟩ := ih1
+      rw [hm2] at hm1
+      use m1
 
-set_option warn.sorry false in
 /-- Hard exercise, you will likely need the lemmas above,
     and possibly additional intermediary results. -/
 lemma executeLemma {μ st} (h1 : Reachable (.ok μ) st) (h2 : isFinal st) :
     ∃ fuel : ℕ, execute fuel μ = st := by
-  sorry
+  cases st with
+  | error => contradiction
+  | ok μx =>
+    obtain ⟨m, hm⟩ := @executeLemmaAux 0 _ _ h1
+    use m
+    rw [hm, execute]
+    simp [h2]

SoftwareFoundations2/StackMachine/Semantics.lean

@@ -44,19 +44,29 @@ def step (μ : MachineState) : ExecutionState := do
       let ⟨n1, n2, s⟩ ← stackPeek2 μ
       .ok <| replaceStackAndIncrPC μ ((n2 + n1) :: s)
   | SUB      =>
-      sorry
+      let ⟨n1, n2, s⟩ ← stackPeek2 μ
+      .ok <| replaceStackAndIncrPC μ ((n2 - n1) :: s)
   | MUL      =>
-      sorry
+      let ⟨n1, n2, s⟩ ← stackPeek2 μ
+      .ok <| replaceStackAndIncrPC μ ((n2 * n1) :: s)
   | EQ       =>
       let ⟨n1, n2, s⟩ ← stackPeek2 μ
       if n2 == n1 then
         .ok <| replaceStackAndIncrPC μ (1 :: s)
       else
         .ok <| replaceStackAndIncrPC μ (0 :: s)
   | .LE       =>
-      sorry
+      let ⟨n1, n2, s⟩ ← stackPeek2 μ
+      if n2 ≤ n1 then
+        .ok <| replaceStackAndIncrPC μ (1 :: s)
+      else
+        .ok <| replaceStackAndIncrPC μ (0 :: s)
   | .ISZERO     =>
-      sorry
+      let ⟨n1, s⟩ ← stackPeek1 μ
+      if n1 == 0 then
+        .ok <| replaceStackAndIncrPC μ (1 :: s)
+      else
+        .ok <| replaceStackAndIncrPC μ (0 :: s)
   | JUMP =>
       let ⟨pc, s⟩ ← stackPeek1 μ
       .ok <| { μ with pc := pc, stack := s }