[sledge sem] Add a more llair-like LLVM semantics

Summary:
The simple LLVM semantics steps one instruction at a time, but the
generated llair does whole blocks at a time, since many individual LLVM
instructions can become a single llair expression. We add a bigger-step
LLVM semantics that does whole blocks at a time (except that it also
stops at function calls, since those end blocks in llair). The steps in
this bigger-step semantics should be at the same granularity as the
llair steps, making it easier to verify the translation.

We add a notion of observation to the LLVM semantics (right now, just
global variable writes) and use that to define two top-level semantic
functions, which we prove to be equivalent.

Reviewed By: jberdine

Differential Revision: D17396016

fbshipit-source-id: ee632fb92

sledge/semantics/llvmScript.sml

@@ -9,6 +9,7 @@
  * are relevant for the LLVM -> LLAIR translation, especially exceptions. *)
 
 open HolKernel boolLib bossLib Parse;
+open llistTheory pathTheory;
 open settingsTheory memory_modelTheory;
 
 new_theory "llvm";
@@ -74,6 +75,7 @@ Datatype:
   | Br arg label label
   | Invoke reg ty arg (targ list) label label
   | Unreachable
+  | Exit
   (* Non-terminators *)
   | Sub reg bool bool ty arg arg
   | Extractvalue reg targ (const list)
@@ -131,6 +133,7 @@ Definition terminator_def:
   (terminator (Br _ _ _) ⇔ T) ∧
   (terminator (Invoke _ _ _ _ _ _) ⇔ T) ∧
   (terminator Unreachable ⇔ T) ∧
+  (terminator Exit ⇔ T) ∧
   (terminator _ ⇔ F)
 End
 
@@ -175,6 +178,15 @@ Datatype:
        heap : bool heap |>
 End
 
+(* Labels for the transitions to make externally observable behaviours apparent.
+ * For now, we'll consider this to be writes to global variables.
+ * *)
+Datatype:
+  obs =
+  | Tau
+  | W glob_var (word8 list)
+End
+
 (* ----- Things about types ----- *)
 
 (* Given a number n that fits into pointer_size number of bytes, create the
@@ -462,6 +474,11 @@ Definition inc_pc_def:
   inc_pc s = s with ip := (s.ip with i := s.ip.i + 1)
 End
 
+Inductive get_obs:
+  (flookup s.globals x = Some (n, w) ⇒ get_obs s w bytes (W x bytes)) ∧
+  ((∀n. (n, w) ∉ FRANGE s.globals) ⇒ get_obs s w bytes Tau)
+End
+
 (* NB, the semantics tracks the poison values, but not much thought has been put
  * into getting it exactly right, so we don't have much confidence that it is
  * exactly right. We also are currently ignoring the undefined value. *)
@@ -472,7 +489,7 @@ Inductive step_instr:
    eval s a = Some v
    ⇒
    step_instr prog s
-     (Ret (t, a))
+     (Ret (t, a)) Tau
      (update_result fr.result_var v
        <| ip := fr.ret;
           globals := s.globals;
@@ -498,19 +515,19 @@ Inductive step_instr:
    map (do_phi l s) phis = map Some updates
    ⇒
    step_instr prog s
-     (Br a l1 l2)
+     (Br a l1 l2) Tau
      (s with <| ip := <| f := s.ip.f; b := l; i := 0 |>;
                 locals := s.locals |++ updates |>)) ∧
 
   (* TODO *)
-  (step_instr prog s (Invoke r t a args l1 l2) s) ∧
+  (step_instr prog s (Invoke r t a args l1 l2) Tau s) ∧
 
   (eval s a1 = Some v1 ∧
    eval s a2 = Some v2 ∧
    do_sub nuw nsw v1 v2 t = Some v3
    ⇒
    step_instr prog s
-     (Sub r nuw nsw t a1 a2)
+     (Sub r nuw nsw t a1 a2) Tau
      (inc_pc (update_result r v3 s))) ∧
 
   (eval s a = Some v ∧
@@ -520,7 +537,7 @@ Inductive step_instr:
    extract_value v.value ns = Some result
    ⇒
    step_instr prog s
-     (Extractvalue r (t, a) const_indices)
+     (Extractvalue r (t, a) const_indices) Tau
      (inc_pc (update_result r <| poison := v.poison; value := result |> s))) ∧
 
   (eval s a1 = Some v1 ∧
@@ -531,7 +548,7 @@ Inductive step_instr:
    insert_value v1.value v2.value ns = Some result
    ⇒
    step_instr prog s
-     (Insertvalue r (t1, a1) (t2, a2) const_indices)
+     (Insertvalue r (t1, a1) (t2, a2) const_indices) Tau
      (inc_pc (update_result r
                 <| poison := (v1.poison ∨ v2.poison); value := result |> s))) ∧
 
@@ -543,7 +560,7 @@ Inductive step_instr:
    mk_ptr n2 = Some ptr
    ⇒
    step_instr prog s
-     (Alloca r t (t1, a1))
+     (Alloca r t (t1, a1)) Tau
      (inc_pc (update_result r <| poison := v.poison; value := ptr |>
                 (s with heap := new_h)))) ∧
 
@@ -553,20 +570,21 @@ Inductive step_instr:
    pbytes = get_bytes s.heap interval
    ⇒
    step_instr prog s
-     (Load r t (t1, a1))
+     (Load r t (t1, a1)) Tau
      (inc_pc (update_result r <| poison := (T ∈ set (map fst pbytes));
                                  value := fst (bytes_to_llvm_value t (map snd pbytes)) |>
                             s))) ∧
 
   (eval s a2 = Some <| poison := p2; value := FlatV (PtrV w) |> ∧
    eval s a1 = Some v1 ∧
-   interval = Interval freeable (w2n w) (w2n w + sizeof t) ∧
+   interval = Interval freeable (w2n w) (w2n w + sizeof t1) ∧
    is_allocated interval s.heap ∧
    bytes = llvm_value_to_bytes v1.value ∧
-   length bytes = sizeof t
+   length bytes = sizeof t1 ∧
+   get_obs s w bytes obs
    ⇒
    step_instr prog s
-     (Store (t1, a1) (t2, a2))
+     (Store (t1, a1) (t2, a2)) obs
      (inc_pc (s with heap := set_bytes p2 bytes (w2n w) s.heap))) ∧
 
   (map (eval s o snd) tindices = map Some (i1::indices) ∧
@@ -579,7 +597,7 @@ Inductive step_instr:
    mk_ptr (w2n w1 + sizeof t1 * i + off) = Some ptr
    ⇒
    step_instr prog s
-    (Gep r t ((PtrT t1), a1) tindices)
+    (Gep r t ((PtrT t1), a1) tindices) Tau
     (inc_pc (update_result r
                <| poison := (v1.poison ∨ i1.poison ∨ exists (λv. v.poison) indices);
                   value := ptr |>
@@ -590,7 +608,7 @@ Inductive step_instr:
    w64_cast w t = Some int_v
    ⇒
    step_instr prog s
-    (Ptrtoint r (t1, a1) t)
+    (Ptrtoint r (t1, a1) t) Tau
     (inc_pc (update_result r <| poison := v1.poison; value := int_v |> s))) ∧
 
   (eval s a1 = Some v1 ∧
@@ -598,7 +616,7 @@ Inductive step_instr:
    mk_ptr n = Some ptr
    ⇒
    step_instr prog s
-    (Inttoptr r (t1, a1) t)
+    (Inttoptr r (t1, a1) t) Tau
     (inc_pc (update_result r <| poison := v1.poison; value := ptr |> s))) ∧
 
   (eval s a1 = Some v1 ∧
@@ -606,14 +624,14 @@ Inductive step_instr:
    do_icmp c v1 v2 = Some v3
    ⇒
    step_instr prog s
-    (Icmp r c t a1 a2)
+    (Icmp r c t a1 a2) Tau
     (inc_pc (update_result r v3 s))) ∧
 
   (alookup prog fname = Some d ∧
    map (eval s o snd) targs = map Some vs
    ⇒
    step_instr prog s
-     (Call r t fname targs)
+     (Call r t fname targs) Tau
      <| ip := <| f := fname; b := None; i := 0 |>;
         locals := alist_to_fmap (zip (map snd d.params, vs));
         globals := s.globals;
@@ -622,33 +640,61 @@ Inductive step_instr:
              saved_locals := s.locals;
              result_var := r;
              stack_allocs := [] |> :: s.stack;
-        heap := s.heap |>) ∧
+        heap := s.heap |>)(* ∧
 
   (* TODO *)
-  (step_instr prog s (Cxa_allocate_exn r a) s) ∧
+  (step_instr prog s (Cxa_allocate_exn r a) Tau s) ∧
   (* TODO *)
-  (step_instr prog s (Cxa_throw a1 a2 a3) s) ∧
+  (step_instr prog s (Cxa_throw a1 a2 a3) Tau s) ∧
   (* TODO *)
-  (step_instr prog s (Cxa_begin_catch r a) s) ∧
+  (step_instr prog s (Cxa_begin_catch r a) Tau s) ∧
   (* TODO *)
-  (step_instr prog s (Cxa_end_catch) s) ∧
+  (step_instr prog s (Cxa_end_catch) Tau s) ∧
   (* TODO *)
-  (step_instr prog s (Cxa_get_exception_ptr r a) s)
+  (step_instr prog s (Cxa_get_exception_ptr r a) Tau s)
+  *)
 End
 
-Inductive next_instr:
-  alookup p s.ip.f = Some d ∧
-  alookup d.blocks s.ip.b = Some b ∧
-  s.ip.i < length b.body
-  ⇒
-  next_instr p s (el s.ip.i b.body)
+Inductive get_instr:
+  (∀prog ip.
+   alookup prog ip.f = Some d ∧
+   alookup d.blocks ip.b = Some b ∧
+   ip.i < length b.body
+   ⇒
+   get_instr prog ip (el ip.i b.body))
 End
 
 Inductive step:
-  next_instr p s i ∧
-  step_instr p s i s'
+  get_instr p s.ip i ∧
+  step_instr p s i l s'
   ⇒
-  step p s s'
+  step p s l s'
+End
+
+Datatype:
+  trace_type =
+  | Stuck
+  | Complete
+  | Partial
+End
+
+Definition get_observation_def:
+  get_observation prog last_s =
+    if get_instr prog last_s.ip Exit then
+      Complete
+    else if ∃s l. step prog last_s l s then
+      Partial
+    else
+      Stuck
+End
+
+(* The semantics of a program will be the finite traces of stores to global
+ * variables.
+ * *)
+Definition sem_def:
+  sem p s1 =
+    { (get_observation p (last path), filter (\x. x ≠ Tau) l)  | (path, l) |
+      toList (labels path) = Some l ∧ finite path ∧ okpath (step p) path ∧ first path = s1 }
 End
 
 (* ----- Invariants on state ----- *)

sledge/semantics/llvm_liveScript.sml

@@ -0,0 +1,176 @@
+(*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ *)
+
+(* Proofs about a shallowly embedded concept of live variables *)
+
+open HolKernel boolLib bossLib Parse;
+open pred_setTheory;
+open settingsTheory miscTheory llvmTheory llvm_propTheory;
+
+new_theory "llvm_live";
+
+numLib.prefer_num ();
+
+Definition inc_pc_def:
+  inc_pc ip = ip with i := ip.i + 1
+End
+
+(* The set of program counters the given instruction and starting point can
+ * immediately reach, withing a function *)
+Definition next_ips_def:
+  (next_ips (Ret _) ip = {}) ∧
+  (next_ips (Br _ l1 l2) ip =
+    { <| f := ip.f; b := Some l; i := 0 |> | l | l ∈ {l1; l2} }) ∧
+  (next_ips (Invoke _ _ _ _ l1 l2) ip =
+    { <| f := ip.f; b := Some l; i := 0 |> | l | l ∈ {l1; l2} }) ∧
+  (next_ips Unreachable ip = {}) ∧
+  (next_ips (Sub _ _ _ _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Extractvalue _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Insertvalue _ _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Alloca _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Load _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Store _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Gep _ _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Ptrtoint _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Inttoptr _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Icmp _ _ _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Call _ _ _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Cxa_allocate_exn _ _) ip = { inc_pc ip }) ∧
+  (* TODO: revisit throw when dealing with exceptions *)
+  (next_ips (Cxa_throw _ _ _) ip = {  }) ∧
+  (next_ips (Cxa_begin_catch _ _) ip = { inc_pc ip }) ∧
+  (next_ips (Cxa_end_catch) ip = { inc_pc ip }) ∧
+  (next_ips (Cxa_get_exception_ptr _ _) ip = { inc_pc ip })
+End
+
+(* The path is a list of program counters that represent a statically feasible
+ * path through a function *)
+Inductive good_path:
+  (∀prog. good_path prog []) ∧
+
+  (∀ip i.
+    get_instr prog ip i
+    ⇒
+    good_path prog [ip]) ∧
+
+  (∀prog path ip1 i1 ip2.
+    get_instr prog ip1 i1 ∧
+    ip2 ∈ next_ips i1 ip1 ∧
+    good_path prog (ip2::path)
+    ⇒
+    good_path prog (ip1::ip2::path))
+End
+
+Definition arg_to_regs_def:
+  (arg_to_regs (Constant _) = {}) ∧
+  (arg_to_regs (Variable r) = {r})
+End
+
+(* The registers that an instruction uses *)
+Definition uses_def:
+  (uses (Ret (_, a)) = arg_to_regs a) ∧
+  (uses (Br a _ _) = arg_to_regs a) ∧
+  (uses (Invoke _ _ a targs _ _) =
+    arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
+  (uses Unreachable = {}) ∧
+  (uses (Sub _ _ _ _ a1 a2) =
+    arg_to_regs a1 ∪ arg_to_regs a2) ∧
+  (uses (Extractvalue _ (_, a) _) = arg_to_regs a) ∧
+  (uses (Insertvalue _ (_, a1) (_, a2) _) =
+    arg_to_regs a1 ∪ arg_to_regs a2) ∧
+  (uses (Alloca _ _ (_, a)) = arg_to_regs a) ∧
+  (uses (Load _ _ (_, a)) = arg_to_regs a) ∧
+  (uses (Store (_, a1) (_, a2)) =
+    arg_to_regs a1 ∪ arg_to_regs a2) ∧
+  (uses (Gep _ _ (_, a) targs) =
+    arg_to_regs a ∪ BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
+  (uses (Ptrtoint _ (_, a) _) = arg_to_regs a) ∧
+  (uses (Inttoptr _ (_, a) _) = arg_to_regs a) ∧
+  (uses (Icmp _ _ _ a1 a2) =
+    arg_to_regs a1 ∪ arg_to_regs a2) ∧
+  (uses (Call _ _ _ targs) =
+    BIGUNION (set (map (arg_to_regs o snd) targs))) ∧
+  (uses (Cxa_allocate_exn _ a) = arg_to_regs a) ∧
+  (uses (Cxa_throw a1 a2 a3) =
+    arg_to_regs a1 ∪ arg_to_regs a2 ∪ arg_to_regs a3) ∧
+  (uses (Cxa_begin_catch _ a) = arg_to_regs a) ∧
+  (uses (Cxa_end_catch) = {  }) ∧
+  (uses (Cxa_get_exception_ptr _ a) = arg_to_regs a)
+End
+
+(* The registers that an instruction assigns *)
+Definition assigns_def:
+  (assigns (Invoke r _ _ _ _ _) = {r}) ∧
+  (assigns (Sub r _ _ _ _ _) = {r}) ∧
+  (assigns (Extractvalue r _ _) = {r}) ∧
+  (assigns (Insertvalue r _ _ _) = {r}) ∧
+  (assigns (Alloca r _ _) = {r}) ∧
+  (assigns (Load r _ _) = {r}) ∧
+  (assigns (Gep r _ _ _) = {r}) ∧
+  (assigns (Ptrtoint r _ _) = {r}) ∧
+  (assigns (Inttoptr r _ _) = {r}) ∧
+  (assigns (Icmp r _ _ _ _) = {r}) ∧
+  (assigns (Call r _ _ _) = {r}) ∧
+  (assigns (Cxa_allocate_exn r _) = {r}) ∧
+  (assigns (Cxa_begin_catch r _) = {r}) ∧
+  (assigns (Cxa_get_exception_ptr r _) = {r}) ∧
+  (assigns _ = {})
+End
+
+Definition live_def:
+  live prog ip ⇔
+    { r | ∃path instr.
+            good_path prog (ip::path) ∧
+            get_instr prog (last (ip::path)) instr ∧
+            r ∈ uses instr ∧
+            ∀ip2 instr2. ip2 ∈ set (front (ip::path)) ∧ get_instr prog ip2 instr2 ⇒ r ∉ assigns instr2 }
+End
+
+Theorem get_instr_live:
+  ∀prog ip instr.
+    get_instr prog ip instr
+    ⇒
+    uses instr ⊆ live prog ip
+Proof
+  rw [live_def, SUBSET_DEF] >>
+  qexists_tac `[]` >> rw [Once good_path_cases] >>
+  qexists_tac `instr` >> simp [] >> metis_tac [IN_DEF]
+QED
+
+Triviality set_rw:
+  !s P. (!x. x ∈ s ⇔ P x) ⇔ s = P
+Proof
+  rw [] >> eq_tac >> rw [IN_DEF] >> metis_tac []
+QED
+
+Theorem live_gen_kill:
+  ∀prog ip instr ip'.
+    get_instr prog ip instr
+    ⇒
+    live prog ip = BIGUNION {live prog ip' | ip' ∈ next_ips instr ip} DIFF assigns instr ∪ uses instr
+Proof
+  rw [live_def, EXTENSION] >> eq_tac >> rw []
+  >- (
+    Cases_on `path` >> fs []
+    >- metis_tac [get_instr_func] >>
+    rename1 `ip::ip2::path` >>
+    qpat_x_assum `good_path _ _` mp_tac >> simp [Once good_path_cases] >> rw [] >>
+    Cases_on `x ∈ uses instr` >> fs [] >> simp [set_rw, PULL_EXISTS] >>
+    qexists_tac `ip2` >> qexists_tac `path` >> qexists_tac `instr'` >> rw [] >>
+    metis_tac [get_instr_func])
+  >- (
+    fs [] >>
+    qexists_tac `ip'::path` >> qexists_tac `instr'` >> rw []
+    >- (simp [Once good_path_cases] >> metis_tac []) >>
+    metis_tac [get_instr_func])
+  >- (
+    qexists_tac `[]` >> qexists_tac `instr` >> rw [] >>
+    simp [Once good_path_cases] >>
+    metis_tac [])
+QED
+
+export_theory ();

sledge/semantics/llvm_propScript.sml

@@ -9,9 +9,9 @@
 
 open HolKernel boolLib bossLib Parse;
 open pairTheory listTheory rich_listTheory arithmeticTheory wordsTheory;
-open pred_setTheory finite_mapTheory;
+open pred_setTheory finite_mapTheory relationTheory llistTheory pathTheory;
 open logrootTheory numposrepTheory;
-open settingsTheory miscTheory llvmTheory memory_modelTheory;
+open settingsTheory miscTheory memory_modelTheory llvmTheory;
 
 new_theory "llvm_prop";
 
@@ -290,23 +290,30 @@ QED
 
 (* ----- Theorems about the step function ----- *)
 
+Theorem get_instr_func:
+  ∀p ip i1 i2. get_instr p ip i1 ∧ get_instr p ip i2 ⇒ i1 = i2
+Proof
+  rw [get_instr_cases] >>
+  metis_tac [optionTheory.SOME_11]
+QED
+
 Theorem inc_pc_invariant:
-  ∀p s i. prog_ok p ∧ next_instr p s i ∧ ¬terminator i ∧ state_invariant p s ⇒ state_invariant p (inc_pc s)
+  ∀p s i. prog_ok p ∧ get_instr p s.ip i ∧ ¬terminator i ∧ state_invariant p s ⇒ state_invariant p (inc_pc s)
 Proof
   rw [state_invariant_def, inc_pc_def, allocations_ok_def, globals_ok_def,
       stack_ok_def, frame_ok_def, heap_ok_def, EVERY_EL, ip_ok_def]
   >- (
     qexists_tac `dec` >> qexists_tac `block'` >> rw [] >>
-    fs [prog_ok_def, next_instr_cases] >> res_tac >> rw [] >>
+    fs [prog_ok_def, get_instr_cases] >> res_tac >> rw [] >>
     `s.ip.i ≠ length block'.body - 1` suffices_by decide_tac >>
     CCONTR_TAC >> fs [] >> rfs [LAST_EL, PRE_SUB1]) >>
   metis_tac []
 QED
 
-Theorem next_instr_update:
-  ∀p s i r v. next_instr p (update_result r v s) i <=> next_instr p s i
+Theorem get_instr_update:
+  ∀p s i r v. get_instr p (update_result r v s).ip i <=> get_instr p s.ip i
 Proof
-  rw [next_instr_cases, update_result_def]
+  rw [get_instr_cases, update_result_def]
 QED
 
 Theorem update_invariant:
@@ -341,8 +348,8 @@ Proof
 QED
 
 Theorem step_instr_invariant:
-  ∀i s2.
-    step_instr p s1 i s2 ⇒ prog_ok p ∧ next_instr p s1 i ∧ state_invariant p s1
+  ∀i l s2.
+    step_instr p s1 i l s2 ⇒ prog_ok p ∧ get_instr p s1.ip i ∧ state_invariant p s1
     ⇒
     state_invariant p s2
 Proof
@@ -391,37 +398,37 @@ Proof
     >- (fs [globals_ok_def] >> metis_tac [])
     >- (fs [stack_ok_def, frame_ok_def, EVERY_MEM] >> metis_tac []))
   >- (
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant]>>
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant]>>
     metis_tac [terminator_def])
   >- (
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant] >>
     metis_tac [terminator_def])
   >- (
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant] >>
     metis_tac [terminator_def])
   >- ( (* Allocation *)
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant]
     >- metis_tac [allocate_invariant]
-    >- (fs [next_instr_cases, allocate_cases] >> metis_tac [terminator_def]))
+    >- (fs [get_instr_cases, allocate_cases] >> metis_tac [terminator_def]))
   >- (
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
-    fs [next_instr_cases] >>
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant] >>
+    fs [get_instr_cases] >>
     metis_tac [terminator_def])
   >- ( (* Store *)
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant]
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant]
     >- (irule set_bytes_invariant >> rw [] >> metis_tac [])
-    >- (fs [next_instr_cases] >> metis_tac [terminator_def]))
+    >- (fs [get_instr_cases] >> metis_tac [terminator_def]))
   >- (
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant] >>
     metis_tac [terminator_def])
   >- (
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant] >>
     metis_tac [terminator_def])
   >- (
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant] >>
     metis_tac [terminator_def])
   >- (
-    irule inc_pc_invariant >> rw [next_instr_update, update_invariant] >>
+    irule inc_pc_invariant >> rw [get_instr_update, update_invariant] >>
     metis_tac [terminator_def])
   >- ( (* Call *)
     rw [state_invariant_def]
@@ -435,11 +442,35 @@ Proof
         last_x_assum drule >> disch_then drule >> rw [] >>
         CCONTR_TAC >> fs [] >> rfs [LAST_EL] >>
         Cases_on `length block'.body = s1.ip.i + 1` >> fs [PRE_SUB1] >>
-        fs [next_instr_cases] >>
+        fs [get_instr_cases] >>
         metis_tac [terminator_def])
       >- (fs [EVERY_MEM, frame_ok_def] >> metis_tac [])))
 QED
 
+Theorem exit_no_step:
+  !p s1. get_instr p s1.ip Exit ⇒ ¬?l s2. step p s1 l s2
+Proof
+  rw [step_cases, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
+  `i = Exit` by metis_tac [get_instr_func] >>
+  rw [step_instr_cases]
+QED
+
+Definition is_call_def:
+  (is_call (Call _ _ _ _) ⇔ T) ∧
+  (is_call _ ⇔ F)
+End
+
+Theorem step_same_block:
+  ∀p s1 l s2 i.
+    get_instr p s1.ip i ∧ step_instr p s1 i l s2 ∧ ¬terminator i ∧ ~is_call i⇒
+    s1.ip.f = s2.ip.f ∧
+    s1.ip.b = s2.ip.b ∧
+    s2.ip.i = s1.ip.i + 1
+Proof
+  rw [step_instr_cases] >>
+  fs [terminator_def, is_call_def, inc_pc_def, update_result_def]
+QED
+
 (* ----- Initial state is ok ----- *)
 
 Theorem init_invariant:
@@ -450,4 +481,390 @@ Proof
   >- rw [stack_ok_def]
 QED
 
+
+(* ----- A bigger-step semantics ----- *)
+Definition stuck_def:
+  stuck p s1 ⇔ ¬get_instr p s1.ip Exit ∧ ¬∃l s2. step p s1 l s2
+End
+
+Definition last_step_def:
+  last_step p s1 l s2 ⇔
+   ∃i.
+     step p s1 l s2 ∧ get_instr p s1.ip i ∧
+     (terminator i ∨ is_call i ∨ ¬∃l s3. step p s2 l s3)
+End
+
+(* Run all of the instructions up-to-and-including the next Call or terminator
+ * *)
+Inductive multi_step:
+
+  (∀p s1 s2 l.
+   last_step p s1 l s2
+   ⇒
+   multi_step p s1 [l] s2) ∧
+
+  (∀p s1 s2 s3 i l ls.
+   step p s1 l s2 ∧
+   get_instr p s1.ip i ∧
+   ¬(terminator i ∨ is_call i) ∧
+   multi_step p s2 ls s3
+   ⇒
+   multi_step p s1 (l::ls) s3)
+End
+
+Inductive observation_prefixes:
+  (∀l. observation_prefixes (Complete, l) (Complete, filter (\x. x ≠ Tau) l)) ∧
+  (∀l. observation_prefixes (Stuck, l) (Stuck, filter (\x. x ≠ Tau) l)) ∧
+  (∀l1 l2 x.
+    l2 ≼ l1 ∧ (l2 = l1 ⇒ x = Partial)
+    ⇒
+    observation_prefixes (x, l1) (Partial, filter (\x. x ≠ Tau) l2))
+End
+
+Definition multi_step_sem_def:
+  multi_step_sem p s1 =
+    { l1 | ∃path l2. l1 ∈ observation_prefixes (get_observation p (last path), flat l2) ∧
+           toList (labels path) = Some l2 ∧
+           finite path ∧ okpath (multi_step p) path ∧ first path = s1 }
+End
+
+Theorem multi_step_to_step_path:
+  ∀p s1 l s2.
+    multi_step p s1 l s2 ⇒
+      ∃path.
+        finite path ∧ okpath (step p) path ∧ first path = s1 ∧ last path = s2 ∧
+        toList (labels path) = Some l
+Proof
+  ho_match_mp_tac multi_step_ind >> conj_tac
+  >- (rw [] >> qexists_tac `pcons s1 l (stopped_at s2)` >> fs [toList_THM, last_step_def]) >>
+  rw [] >>
+  qexists_tac `pcons s1 l path` >> rw [toList_THM] >>
+  `LFINITE (labels path)` by metis_tac [finite_labels] >>
+  drule LFINITE_toList >> rw [] >> rw []
+QED
+
+Theorem expand_multi_step_path:
+  ∀path. okpath (multi_step prog) path ∧ finite path ⇒
+    !l. toList (labels path) = Some l ⇒
+    ∃path'.
+      toList (labels path') = Some (flat l) ∧ finite path' ∧
+      okpath (step prog) path' ∧ first path' = first path ∧ last path' = last path
+Proof
+  ho_match_mp_tac finite_okpath_ind >> rw []
+  >- (qexists_tac `stopped_at x` >> fs [toList_THM] >> rw []) >>
+  fs [toList_THM] >> rw [] >>
+  first_x_assum drule >> rw [] >>
+  drule multi_step_to_step_path >> rw [] >>
+  qexists_tac `plink path'' path'` >> rw [] >>
+  simp [toList_THM, labels_plink] >>
+  `LFINITE (LAPPEND (labels path'') (labels path'))` by metis_tac [LFINITE_APPEND, finite_labels] >>
+  drule LFINITE_toList >> rw [] >> drule toList_LAPPEND_APPEND >> rw []
+QED
+
+Theorem contract_step_path:
+  ∀path. okpath (step prog) path ∧ finite path ⇒
+    ∀l1 l s. last_step prog (last path) l s ∧
+      toList (labels path) = Some l1
+    ⇒
+    ∃path' l2.
+      toList (labels path') = Some l2 ∧
+      flat l2 = l1 ++ [l] ∧
+      finite path' ∧
+      okpath (multi_step prog) path' ∧ first path' = first path ∧ last path' = s
+Proof
+  ho_match_mp_tac finite_okpath_ind >> rw []
+  >- (
+    qexists_tac `pcons x [l] (stopped_at s)` >> fs [] >> simp [toList_THM] >>
+    simp [Once multi_step_cases] >>
+    fs [toList_THM]) >>
+  fs [toList_THM] >>
+  first_x_assum drule >> disch_then drule >> rw [] >>
+  Cases_on `last_step prog x r (first path)`
+  >- (
+    qexists_tac `pcons x [r] path'` >> simp [] >>
+    simp [Once multi_step_cases, toList_THM])
+  >- (
+    qpat_x_assum `okpath (multi_step _) _` mp_tac >>
+    simp [Once okpath_cases] >> rw [] >> fs [toList_THM] >> rw [] >> fs [] >>
+    qexists_tac `pcons x (r::r') p` >> fs [toList_THM] >> rw [Once multi_step_cases] >>
+    disj2_tac >> qexists_tac `first path` >> rw [] >> fs [last_step_def] >> rfs [] >>
+    fs [step_cases, get_instr_cases] >>
+    metis_tac [])
+QED
+
+Definition get_next_step_def:
+  get_next_step p s1 =
+    some (s2, l). step p s1 l s2 ∧ ¬last_step p s1 l s2
+End
+
+Triviality finite_plink_trivial:
+  ∀path. finite path ⇒ path = plink path (stopped_at (last path))
+Proof
+  ho_match_mp_tac finite_path_ind >> rw []
+QED
+
+Definition instrs_left_def:
+  instrs_left prog s =
+    case alookup prog s.ip.f of
+    | None => 0
+    | Some d =>
+      case alookup d.blocks s.ip.b of
+      | None => 0
+      | Some b => length b.body - s.ip.i
+End
+
+Theorem extend_step_path:
+  ∀path.
+    okpath (step p) path ∧ finite path
+    ⇒
+    (∀s. path = stopped_at s ⇒ ∃s' l. step p s l s') ⇒
+    ?path' l s n. finite path' ∧ okpath (step p) path' ∧ last_step p (last path') l s ∧
+      length path = Some (Suc n) ∧ n ∈ PL (pconcat path' l (stopped_at s)) ∧
+      path = take n (pconcat path' l (stopped_at s))
+Proof
+  rw [] >>
+  Cases_on `get_next_step p (last path) = None ∧ ∀s. path ≠ stopped_at s`
+  >- (
+    fs [get_next_step_def, optionTheory.some_def, FORALL_PROD, METIS_PROVE [] ``~x ∨ y ⇔ (x ⇒ y)``] >>
+    Cases_on `?l2 s2. step p (last path) l2 s2` >> fs []
+    >- (
+      first_x_assum drule >> rw [] >>
+      qexists_tac `path` >> qexists_tac `l2` >> qexists_tac `s2` >> rw [] >>
+      fs [finite_length] >>
+      qexists_tac `n - 1` >>
+      `n ≠ 0` by metis_tac [length_never_zero] >>
+      rw [PL_def] >>
+      `length (pconcat path l2 (stopped_at s2)) = Some (n + 1)`
+      by metis_tac [length_pconcat, alt_length_thm] >>
+      rw [take_pconcat]
+      >- metis_tac [take_all] >>
+      fs [PL_def] >> rfs [])
+    >- (
+      drule finite_path_end_cases >>
+      rw [] >> fs [] >> rfs [] >>
+      qexists_tac `p'` >> rw [] >>
+      qexists_tac `l` >> qexists_tac `s` >> rw [] >>
+      fs [finite_length] >>
+      qexists_tac `n` >> rw []
+      >- (
+        rw [last_step_def] >> fs [step_cases] >>
+        metis_tac []) >>
+      `length (plink p' (pcons (last p') l (stopped_at s))) = Some (n + Suc 1 - 1)`
+      by metis_tac [length_plink, alt_length_thm, optionTheory.OPTION_MAP_DEF] >>
+      rw []
+      >- (
+        rw [PL_def] >> fs [finite_length] >>
+        `length (pconcat p' l (stopped_at s)) = Some (n + 1)`
+        by metis_tac [length_pconcat, alt_length_thm] >>
+        fs [])
+      >- (
+        rw [take_pconcat]
+        >- (fs [PL_def, finite_length] >> rfs []) >>
+        metis_tac [finite_length, pconcat_to_plink_finite]))) >>
+  qexists_tac `plink path (unfold I (get_next_step p) (last path))` >> rw [] >>
+  qmatch_goalsub_abbrev_tac `finite path1` >>
+  `∃m. length path = Some (Suc m)`
+  by (fs [finite_length] >> Cases_on `n` >> fs [length_never_zero]) >>
+  simp [GSYM PULL_EXISTS] >>
+  conj_asm1_tac
+  >- (
+    simp [Abbr `path1`] >> irule unfold_finite >>
+    WF_REL_TAC `measure (instrs_left p)` >>
+    rpt gen_tac >>
+    simp [instrs_left_def, get_next_step_def, optionTheory.some_def, EXISTS_PROD] >>
+    qmatch_goalsub_abbrev_tac `@x. P x` >> rw [] >>
+    `?x. P x` by (fs [Abbr `P`, EXISTS_PROD] >> metis_tac []) >>
+    `P (@x. P x)` by metis_tac [SELECT_THM] >>
+    qunabbrev_tac `P` >> pop_assum mp_tac >> simp [] >>
+    simp [last_step_def] >> rw [] >>
+    pop_assum mp_tac >> simp [] >>
+    `?i. get_instr p s2.ip i` by metis_tac [get_instr_cases, step_cases] >>
+    disch_then (qspec_then `i` mp_tac) >> simp [] >>
+    pop_assum mp_tac >> pop_assum mp_tac >> simp [Once step_cases] >>
+    rw [] >>
+    `i' = i` by metis_tac [get_instr_func] >> rw [] >>
+    drule step_same_block >> disch_then drule >> simp [] >>
+    rw [] >> fs [step_cases, get_instr_cases]) >>
+ `last path = first path1`
+  by (
+    unabbrev_all_tac >> simp [Once unfold_thm] >>
+    CASE_TAC >> rw [] >> split_pair_case_tac >> rw []) >>
+  simp [last_plink] >>
+  conj_asm1_tac
+  >- (
+    unabbrev_all_tac >>
+    irule okpath_unfold >> rw [] >>
+    qexists_tac `\x.T` >> rw [get_next_step_def] >>
+    fs [optionTheory.some_def] >>
+    pairarg_tac >> fs [] >>
+    qmatch_assum_abbrev_tac `(@x. P x) = _` >>
+    `P (@x. P x)`
+    by (
+      simp [SELECT_THM] >>
+      unabbrev_all_tac >> fs [EXISTS_PROD] >>
+      metis_tac []) >>
+    rfs [] >>
+    unabbrev_all_tac >> fs []) >>
+  `?n. length path1 = Some n` by fs [finite_length] >>
+  `n ≠ 0` by metis_tac [length_never_zero] >>
+  `length (plink path path1) = Some (Suc m + n - 1)` by metis_tac [length_plink] >>
+  simp [take_pconcat, PL_def, finite_pconcat, length_plink] >>
+  `!l s. length (pconcat (plink path path1) l (stopped_at s)) = Some ((Suc m + n − 1) + 1)`
+  by metis_tac [length_pconcat, alt_length_thm] >>
+  rw [GSYM PULL_EXISTS]
+  >- (
+    unabbrev_all_tac >> drule unfold_last >>
+    qmatch_goalsub_abbrev_tac `last_step _ (last path1) _ _` >>
+    simp [get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
+    rw [METIS_PROVE [] ``~x ∨ y ⇔ (~y ⇒ ~x)``] >> CCONTR_TAC >>
+    Cases_on `1 ∈ PL path1`
+    >- (
+      fs [] >> pairarg_tac >> fs [] >> rw [] >>
+      qmatch_assum_abbrev_tac `(@x. P x) = _` >>
+      `P (@x. P x)`
+      by (
+        simp [SELECT_THM] >>
+        unabbrev_all_tac >> fs [EXISTS_PROD] >>
+        metis_tac []) >>
+      fs [Abbr `P`] >> pairarg_tac >> fs [] >> rw [] >>
+      fs [last_step_def] >> rfs  [] >>
+      `?i. get_instr p x.ip i` by (fs [step_cases] >> metis_tac []) >>
+      metis_tac []) >>
+    `n = 1` by (rfs [PL_def, finite_length] >> decide_tac) >> rw [] >>
+    qspec_then `path1` strip_assume_tac path_cases
+    >- (
+      unabbrev_all_tac >> fs [] >> rw [] >>
+      fs [Once unfold_thm] >>
+      Cases_on `get_next_step p (last path)` >> simp [] >> fs [] >> rw [] >>
+      fs [get_next_step_def, optionTheory.some_def, FORALL_PROD] >>
+      split_pair_case_tac >> fs []) >>
+    fs [alt_length_thm, length_never_zero])
+  >- (
+    rw [take_plink]
+    >-  (imp_res_tac take_all >> fs []) >>
+    metis_tac [finite_plink_trivial])
+QED
+
+Theorem find_path_prefix:
+  ∀path.
+     okpath (step p) path ∧ finite path
+    ⇒
+    !obs l1. toList (labels path) = Some l1 ∧
+    obs ∈ observation_prefixes (get_observation p (last path), l1)
+    ⇒
+    ∃n l2. n ∈ PL path ∧ toList (labels (take n path)) = Some l2 ∧
+      obs = (get_observation p (last (take n path)), filter (\x. x ≠ Tau) l2)
+Proof
+  ho_match_mp_tac finite_okpath_ind >> rw [toList_THM]
+  >- fs [observation_prefixes_cases, get_observation_def, IN_DEF] >>
+  `?s ls. obs = (s, ls)` by metis_tac [pairTheory.pair_CASES] >>
+  fs [] >>
+  `∃l. length path = Some l ∧ l ≠ 0` by metis_tac [finite_length, length_never_zero] >>
+  `take (l-1) path = path` by metis_tac [take_all] >>
+  Cases_on `s` >> fs []
+  >- (
+    qexists_tac `l` >> rw [toList_THM] >>
+    Cases_on `l` >> fs [toList_THM] >>
+    fs [observation_prefixes_cases, IN_DEF, PL_def])
+  >- (
+    qexists_tac `l` >> rw [toList_THM] >>
+    Cases_on `l` >> fs [toList_THM] >>
+    fs [observation_prefixes_cases, IN_DEF, PL_def]) >>
+  qpat_x_assum `(Partial, _) ∈ _` mp_tac >>
+  simp [observation_prefixes_cases, Once IN_DEF] >> rw [] >>
+  rename1 `short_l ≼ first_l::long_l` >>
+  Cases_on `short_l` >> fs []
+  >- (
+    qexists_tac `0` >> rw [toList_THM, get_observation_def] >>
+    metis_tac [exit_no_step]) >>
+  rename1 `short_l ≼ long_l` >>
+  rfs [] >>
+  `(Partial, filter (\x. x ≠ Tau) short_l) ∈ observation_prefixes (get_observation p (last path),long_l)`
+  by (simp [observation_prefixes_cases, IN_DEF] >> metis_tac []) >>
+  first_x_assum drule >> strip_tac >>
+  qexists_tac `Suc n` >> simp [toList_THM] >> rw [] >> rfs [last_take]
+QED
+
+Triviality is_prefix_lem:
+  ∀l1 l2 l3. l1 ≼ l2 ⇒ l1 ≼ l2 ++ l3
+Proof
+  Induct >> rw [] >> fs [] >>
+  Cases_on `l2` >> fs []
+QED
+
+Theorem big_sem_equiv:
+  !p s1. multi_step_sem p s1 = sem p s1
+Proof
+  rw [multi_step_sem_def, sem_def, EXTENSION] >> eq_tac >> rw []
+  >- (
+    drule expand_multi_step_path >> rw [] >>
+    rename [`toList (labels m_path) = Some m_l`, `toList (labels s_path) = Some (flat m_l)`] >>
+    `?n short_l.
+      n ∈ PL s_path ∧
+      toList (labels (take n s_path)) = Some short_l ∧
+      x = (get_observation p (last (take n s_path)), filter (\x. x ≠ Tau) short_l)`
+    by metis_tac [find_path_prefix] >>
+    qexists_tac `take n s_path` >> rw [])
+  >- (
+    Cases_on `¬∀s. path = stopped_at s ⇒ ∃s' l. step p s l s'`
+    >- (
+      fs [] >> rw [] >> fs [toList_THM] >> rw [] >>
+      qexists_tac `stopped_at s` >> rw [toList_THM] >>
+      rw [observation_prefixes_cases, IN_DEF, get_observation_def]) >>
+    drule extend_step_path >> disch_then drule >>
+    impl_tac >> rw []
+    >- metis_tac [] >>
+    rename1 `last_step _ (last s_ext_path) last_l last_s` >>
+    `?s_ext_l. toList (labels s_ext_path) = Some s_ext_l` by metis_tac [LFINITE_toList, finite_labels] >>
+    qabbrev_tac `orig_path = take n (pconcat s_ext_path last_l (stopped_at last_s))` >>
+    drule contract_step_path >> simp [] >> disch_then drule >> rw [] >>
+    rename [`toList (labels m_path) = Some m_l`,
+            `toList (labels s_ext_path) = Some s_ext_l`,
+            `first m_path = first s_ext_path`,
+            `okpath (multi_step _) m_path`] >>
+    qexists_tac `m_path` >> rw [] >>
+    TRY (rw [Abbr `orig_path`] >> NO_TAC) >>
+    rfs [last_take, take_pconcat] >>
+    Cases_on `length s_ext_path = Some n`
+    >- (
+      rfs [PL_def] >> fs [] >>
+      rw [observation_prefixes_cases, IN_DEF] >> rw [] >>
+      unabbrev_all_tac >> rw [last_pconcat] >> fs [] >>
+      drule toList_LAPPEND_APPEND >> rw [toList_THM] >>
+      Cases_on `get_observation p (last m_path)` >> simp [] >>
+      qexists_tac `s_ext_l ++ [last_l]` >> rw []) >>
+    fs [PL_def, finite_pconcat] >> rfs [] >>
+    `?m. length s_ext_path = Some m` by metis_tac [finite_length] >>
+    `length s_ext_path = Some m` by metis_tac [finite_length] >>
+    `length (pconcat s_ext_path last_l (stopped_at (last m_path))) = Some (m + 1)`
+    by metis_tac [length_pconcat, alt_length_thm] >>
+    fs [] >>
+    `n < m` by decide_tac >> fs [] >> rw [] >>
+    `n ∈ PL s_ext_path` by rw [PL_def] >>
+    Cases_on `get_observation p (last orig_path) = Partial`
+    >- (
+      rw [observation_prefixes_cases, IN_DEF] >> rw [] >>
+      unabbrev_all_tac >> fs [] >>
+      `LTAKE n (labels s_ext_path) = Some l` by metis_tac [LTAKE_labels] >>
+      fs [toList_some] >> rfs [] >>
+      Cases_on `m` >> fs [length_labels] >>
+      qexists_tac `l` >> rw [] >> rfs []
+      >- (
+        irule is_prefix_lem >>
+        `n ≤ length s_ext_l` by decide_tac >>
+        fs [ltake_fromList2] >>
+        rw [take_is_prefix])
+      >- (drule LTAKE_LENGTH >> rw [])) >>
+    `¬∃l s. step p (last orig_path) l s`
+    by (fs [get_observation_def] >> BasicProvers.EVERY_CASE_TAC >> fs [] >> metis_tac [exit_no_step]) >>
+    unabbrev_all_tac >> rfs [last_take] >>
+    fs [okpath_pointwise] >>
+    Cases_on `Suc n ∈ PL s_ext_path` >> rw []
+    >- (last_x_assum (qspec_then `n` mp_tac) >> rw []) >>
+    `n = m - 1` by (fs [PL_def] >> rfs []) >>
+    rw [] >>
+    `el (m - 1) s_ext_path = last s_ext_path` by metis_tac [take_all, last_take] >>
+    fs [last_step_def])
+QED
+
 export_theory ();

sledge/semantics/miscScript.sml

@@ -9,7 +9,7 @@
  * could be upstreamed to HOL, and should eventually. *)
 
 open HolKernel boolLib bossLib Parse;
-open listTheory rich_listTheory arithmeticTheory integerTheory;
+open listTheory rich_listTheory arithmeticTheory integerTheory llistTheory pathTheory;
 open integer_wordTheory wordsTheory;
 open finite_mapTheory open logrootTheory numposrepTheory;
 open settingsTheory;
@@ -163,7 +163,7 @@ Proof
 QED
 
 Theorem mod_n2l:
-  ∀d n. 0 < d ⇒ map (\x. x MOD d) (n2l d n) = n2l d n
+  ∀d n. 0 < d ⇒ map (λx. x MOD d) (n2l d n) = n2l d n
 Proof
   rw [] >> drule n2l_BOUND >> disch_then (qspec_then `n` mp_tac) >>
   qspec_tac (`n2l d n`, `l`) >>
@@ -192,7 +192,7 @@ Proof
     conj_tac
     >- (
       simp [int_mod, INT_ADD_ASSOC,
-            intLib.COOPER_PROVE ``!x y (z:int). x - (y + z - a) = x - y - z + a``] >>
+            intLib.COOPER_PROVE ``∀x y (z:int). x - (y + z - a) = x - y - z + a``] >>
       qexists_tac `-((i + s1) / s2)` >>
       intLib.COOPER_TAC) >>
     `&INT_MIN (:α) = s1` by (unabbrev_all_tac >> rw [INT_MIN_def]) >>
@@ -228,7 +228,7 @@ Proof
       fs [Abbr `s2`] >>
       `s1 = &INT_MIN (:'a)` by intLib.COOPER_TAC >> rw [] >>
       irule INT_LESS_MOD >> rw [] >>
-      fs [intLib.COOPER_PROVE ``!(x:int) y. ¬(x ≤ y) ⇔ y < x``] >> rw [] >>
+      fs [intLib.COOPER_PROVE ``∀(x:int) y. ¬(x ≤ y) ⇔ y < x``] >> rw [] >>
       full_simp_tac std_ss [GSYM INT_MUL] >>
       qpat_abbrev_tac `s = &INT_MIN (:α)`
       >- (
@@ -241,4 +241,345 @@ Proof
     simp [INT_MOD_PLUS])
 QED
 
+(* ----- Theorems about lazy lists ----- *)
+
+Theorem toList_some:
+  ∀ll l. toList ll = Some l ⇔ ll = fromList l
+Proof
+  Induct_on `l` >> rw [] >>
+  Cases_on `ll` >> rw [toList_THM] >>
+  metis_tac []
+QED
+
+
+(* ----- Theorems about labelled transition system paths ----- *)
+
+Theorem take_all:
+  ∀p n. length p = Some n ⇒ take (n - 1) p = p
+Proof
+  Induct_on `n` >> rw []
+  >- metis_tac [length_never_zero] >>
+  qspec_then `p` mp_tac path_cases >> rw [] >> fs [alt_length_thm] >>
+  first_x_assum drule >> rw [] >>
+  Cases_on `n` >> fs [length_never_zero]
+QED
+
+Theorem el_plink:
+  ∀n p1 p2.
+    n ∈ PL (plink p1 p2) ∧ last p1 = first p2 ⇒
+    el n (plink p1 p2) = (if n ∈ PL p1 then el n p1 else el (Suc n - THE (length p1)) p2)
+Proof
+  Induct_on `n` >> rw [first_plink] >>
+  qspec_then `p1` mp_tac path_cases >> rw [] >> fs [] >>
+  rw [alt_length_thm] >>
+  first_x_assum drule >> rw [] >>
+  Cases_on `length q` >> fs [PL_def, length_def]
+QED
+
+Theorem el_pcons:
+  ∀n x l p. el n (pcons x l p) = if n = 0 then x else el (n - 1) p
+Proof
+  Induct_on `n` >>
+  rw []
+QED
+
+Theorem first_pconcat[simp]:
+  ∀p1 l p2. first (pconcat p1 l p2) = first p1
+Proof
+  rw [] >> qspec_then `p1` mp_tac path_cases >> rw [] >> rw [pconcat_thm]
+QED
+
+Theorem el_pconcat:
+  ∀n p1 l p2.
+    n ∈ PL (pconcat p1 l p2) ⇒
+    el n (pconcat p1 l p2) = (if n ∈ PL p1 then el n p1 else el (n - THE (length p1)) p2)
+Proof
+  Induct_on `n` >> rw [] >>
+  qspec_then `p1` mp_tac path_cases >> rw [] >> fs [pconcat_thm] >>
+  rw [alt_length_thm] >>
+  first_x_assum drule >> rw [] >>
+  Cases_on `length q` >> fs [PL_def, length_def]
+QED
+
+Theorem labels_pconcat[simp]:
+  ∀p1 l p2. labels (pconcat p1 l p2) = LAPPEND (labels p1) (l:::labels p2)
+Proof
+  rw [pconcat_def, labels_LMAP, path_rep_bijections_thm, LMAP_APPEND]
+QED
+
+Theorem length_pconcat:
+  ∀p1 l p2 l1 l2.
+    length p1 = Some l1 ∧ length p2 = Some l2
+    ⇒
+    length (pconcat p1 l p2) = Some (l1 + l2)
+Proof
+  rw [pconcat_def, length_def, path_rep_bijections_thm, finite_def,
+      LFINITE_APPEND] >>
+  rw [] >>
+  `LFINITE (LAPPEND (snd (fromPath p1)) ((l,first p2):::snd (fromPath p2)))`
+  by rw [LFINITE_APPEND] >>
+  imp_res_tac LFINITE_toList >> rw [] >>
+  imp_res_tac toList_LAPPEND_APPEND >> fs [toList_THM]
+QED
+
+Theorem take_pconcat:
+  ∀n p1 l p2.
+    take n (pconcat p1 l p2) =
+      if n ∈ PL p1 then
+        take n p1
+      else
+        pconcat p1 l (take (n - THE (length p1)) p2)
+Proof
+  Induct_on `n` >> rw []
+  >- (
+    fs [PL_def] >>
+    qspec_then `p1` mp_tac path_cases >> rw [] >> rw [pconcat_thm] >>
+    fs [finite_def, alt_length_thm])
+  >- (
+    qspec_then `p1` mp_tac path_cases >> rw [] >> rw [pconcat_thm] >>
+    fs [PL_def])
+  >- (
+    qspec_then `p1` mp_tac path_cases >> rw [] >> rw [pconcat_thm] >>
+    fs [PL_def, alt_length_thm, finite_length])
+QED
+
+Theorem last_pconcat[simp]:
+  ∀p1. finite p1 ⇒ ∀l p2. last (pconcat p1 l p2) = last p2
+Proof
+  ho_match_mp_tac finite_path_ind >>
+  rw [pconcat_thm]
+QED
+
+Theorem length_labels:
+  ∀p n. length p = Some (Suc n) ⇔ LLENGTH (labels p) = Some n
+Proof
+  Induct_on `n` >> rw [] >>
+  qspec_then `p` mp_tac path_cases >> rw [] >> rw [alt_length_thm, length_never_zero]
+QED
+
+Theorem ltake_fromList2:
+  ∀n l. n ≤ length l ⇒ LTAKE n (fromList l) = Some (take n l)
+Proof
+  Induct_on `l` >> rw [] >>
+  Cases_on `n` >> fs []
+QED
+
+Theorem el_take:
+  ∀p m n. n ∈ PL p ∧ m ≤ n ⇒ el m (take n p) = el m p
+Proof
+  Induct_on `n` >> rw [] >> rw [el_pcons] >>
+  first_x_assum (qspecl_then [`tail p`, `m-1`] mp_tac) >>
+  impl_tac
+  >- (
+    fs [PL_def] >> rw [] >>
+    qspec_then `p` mp_tac path_cases >> rw [] >> fs [alt_length_thm] >>
+    fs [finite_length] >> fs []) >>
+  rw [] >>
+  Cases_on `m` >> rw []
+QED
+
+Theorem nth_label_pcons:
+  (∀n s l p. nth_label 0 (pcons s l p) = l) ∧
+  (∀n s l p. nth_label (Suc n) (pcons s l p) = nth_label n p)
+Proof
+  rw []
+QED
+
+Theorem okpath_pointwise_imp1:
+  ∀p. (∀n. Suc n ∈ PL p ⇒ r (el n p) (nth_label n p) (el (Suc n) p)) ⇒ okpath r p
+Proof
+  ho_match_mp_tac okpath_co_ind >> rw [] >>
+  qspec_then `p` mp_tac path_cases >> rw [] >> rw [first_thm] >>
+  fs [PL_def]
+  >- (first_x_assum (qspec_then `0` mp_tac) >> rw []) >>
+  rw [el_pcons]
+  >- (first_x_assum (qspec_then `1` mp_tac) >> rw [] >> fs [el_pcons, nth_label_compute])
+  >- (
+    first_x_assum (qspec_then `Suc n` mp_tac) >> rw [] >>
+    Cases_on `n` >> fs [])
+QED
+
+Theorem okpath_pointwise_imp2:
+  ∀p. okpath r p ∧ finite p ⇒ (∀n. Suc n ∈ PL p ⇒ r (el n p) (nth_label n p) (el (Suc n) p))
+Proof
+  ho_match_mp_tac finite_okpath_ind >> rw [] >>
+  Cases_on `n` >> fs []
+QED
+
+Theorem okpath_pointwise:
+  ∀r p. okpath r p ⇔ (∀n. Suc n ∈ PL p ⇒ r (el n p) (nth_label n p) (el (Suc n) p))
+Proof
+  rw [] >> eq_tac >> rw [okpath_pointwise_imp1] >>
+  `okpath r (take (Suc n) p)` by metis_tac [okpath_take] >>
+  `finite (take (Suc n) p)` by metis_tac [finite_take] >>
+  drule okpath_pointwise_imp2 >> simp [] >>
+  disch_then (qspec_then `n` mp_tac) >> simp [el_pcons] >>
+  Cases_on `n = 0` >> simp [] >>
+  `n ∈ PL (tail p)`
+  by (
+    fs [PL_def] >>
+    qspec_then `p` mp_tac path_cases >> rw [] >> rw [first_thm] >>
+    fs [alt_length_thm] >> fs [finite_length] >> fs []) >>
+  simp [el_take] >>
+  `el (n - 1) (tail p) = el n p` by (Cases_on `n` >> rw []) >>
+  simp [] >>
+  `∃m. n = Suc m` by intLib.COOPER_TAC >>
+  `Suc m ∈ PL (tail p)` by fs [PL_def] >>
+  ASM_REWRITE_TAC [nth_label_pcons] >>
+  simp [nth_label_take]
+QED
+
+Theorem length_plink:
+  ∀p1 p2 l1 l2.
+    length p1 = Some l1 ∧ length p2 = Some l2
+    ⇒
+    length (plink p1 p2) = Some (l1 + l2 - 1)
+Proof
+  Induct_on `l1` >> rw [] >> fs [length_never_zero] >>
+  qspec_then `p1` mp_tac path_cases >> rw [plink_def] >>
+  fs [alt_length_thm] >> res_tac >> fs [ADD1] >>
+  `l1 ≠ 0` by metis_tac [length_never_zero] >>
+  decide_tac
+QED
+
+Theorem take_plink:
+  ∀n p1 p2.
+    take n (plink p1 p2) =
+      if Suc n ∈ PL p1 then
+        take n p1
+      else
+        plink p1 (take ((Suc n) - THE (length p1)) p2)
+Proof
+  Induct_on `n` >> rw []
+  >- (
+    fs [PL_def] >>
+    qspec_then `p1` mp_tac path_cases >> rw [] >>
+    fs [finite_def, alt_length_thm])
+  >- (
+    fs [PL_def] >>
+    qspec_then `p1` mp_tac path_cases >> rw []>> rw [plink_def] >>
+    fs [finite_length, alt_length_thm] >> rfs [] >>
+    Cases_on `n` >> fs [length_never_zero])
+  >- (
+    qspec_then `p1` mp_tac path_cases >> rw []>> rw [plink_def] >>
+    fs [PL_def])
+  >- (
+    qspec_then `p1` mp_tac path_cases >> rw []>> rw [plink_def] >>
+    fs [PL_def])
+  >- (
+    qspec_then `p1` mp_tac path_cases >> rw [] >> rw [] >>
+    fs [PL_def, alt_length_thm])
+  >- (
+    qspec_then `p1` mp_tac path_cases >> rw [] >> fs [alt_length_thm] >>
+    `finite q` by fs [PL_def] >>
+    fs [finite_length])
+QED
+
+Theorem unfold_last_lem:
+  ∀path. finite path ⇒
+    ∀proj f s. path = unfold proj f s ⇒
+    ∃y. proj y = last path ∧ f y = None ∧ (1 ∈ PL path ⇒ ∃x l. f x = Some (y, l))
+Proof
+  ho_match_mp_tac finite_path_ind >> rw []
+  >- (
+    fs [Once unfold_thm] >> Cases_on `f s` >> fs []
+    >- metis_tac [] >>
+    split_pair_case_tac >> fs []) >>
+  pop_assum mp_tac >> simp [Once unfold_thm] >> Cases_on `f s` >> simp [] >>
+  split_pair_case_tac >> rw [] >>
+  first_x_assum (qspecl_then [`proj`, `f`, `s'`] mp_tac) >> simp [] >>
+  Cases_on `1 ∈ PL (unfold proj f s')` >> rw [] >>
+  fs [PL_def] >>
+  fs [Once unfold_thm] >>
+  Cases_on `f s'` >> fs [alt_length_thm] >> rw [] >-
+  metis_tac [] >>
+  split_pair_case_tac >> fs [] >> rw [] >> fs [alt_length_thm, finite_length] >>
+  rfs [] >>
+   `n = 0 ∨ n = 1` by decide_tac >> fs [length_never_zero]
+QED
+
+Theorem unfold_last:
+  ∀proj f s.
+    finite (unfold proj f s)
+    ⇒
+    ∃y. proj y = last (unfold proj f s) ∧ f y = None ∧
+    (1 ∈ PL (unfold proj f s) ⇒ ∃x l. f x = Some (y, l))
+Proof
+  metis_tac [unfold_last_lem]
+QED
+
+Theorem pconcat_to_plink_finite:
+  ∀p1. finite p1 ⇒ ∀l p2. pconcat p1 l p2 = plink p1 (pcons (last p1) l p2)
+Proof
+  ho_match_mp_tac finite_path_ind >> rw [pconcat_thm]
+QED
+
+Definition opt_funpow_def:
+  (opt_funpow f 0 x = Some x) ∧
+  (opt_funpow f (Suc n) x = option_join (option_map f (opt_funpow f n x)))
+End
+
+Theorem opt_funpow_alt:
+  ∀n f s.
+    opt_funpow f (Suc n) s = option_join (option_map (opt_funpow f n) (f s))
+Proof
+  Induct_on `n` >> rw [] >> Cases_on `f s` >> rw [] >>
+  `1 = Suc 0` by decide_tac >>
+  ASM_REWRITE_TAC [] >>
+  rw [opt_funpow_def] >>
+  fs [opt_funpow_def]
+QED
+
+Theorem unfold_finite_funpow_lem:
+  ∀f proj s x.
+    opt_funpow (option_map fst ∘ f) m s = Some x ∧ f x = None
+    ⇒
+    finite (unfold proj f s)
+Proof
+  Induct_on `m` >> rw [opt_funpow_def] >>
+  simp [Once unfold_thm] >>
+  CASE_TAC >> fs [] >> split_pair_case_tac >> fs [] >> rw [] >>
+  Cases_on `opt_funpow (option_map fst ∘ f) m s` >> rw [] >>
+  fs [optionTheory.OPTION_MAP_DEF] >>
+  first_x_assum irule >> qexists_tac `x` >> rw [] >>
+  `opt_funpow (option_map fst ∘ f) (Suc m) s = Some (fst z)` by fs [opt_funpow_def] >>
+  rfs [opt_funpow_alt]
+QED
+
+Theorem unfold_finite_funpow:
+  ∀f proj s m.
+    opt_funpow (option_map fst ∘ f) m s = None
+    ⇒
+    finite (unfold proj f s)
+Proof
+  rw [] >> irule unfold_finite_funpow_lem >>
+  Induct_on `m` >> rw [] >> fs [opt_funpow_def] >>
+  Cases_on `opt_funpow (option_map fst ∘ f) m s` >> fs [] >>
+  metis_tac []
+QED
+
+Theorem unfold_finite:
+  ∀proj f s.
+    (∃R. WF R ∧ ∀n s2 l s3. opt_funpow (option_map fst o f) n s = Some s2 ∧ f s2 = Some (s3, l) ⇒ R s3 s2)
+    ⇒
+    finite (unfold proj f s)
+Proof
+  rw [] >> drule relationTheory.WF_INDUCTION_THM >>
+  disch_then (qspecl_then [`λx. ∀n. opt_funpow (option_map fst o f) n s = Some x ⇒
+                                    ∃m. opt_funpow (option_map fst o f) m x = None`,
+                           `s`] mp_tac) >>
+  simp [] >>
+  impl_tac
+  >- (
+    rw [] >>
+    first_x_assum drule >> Cases_on `f x` >> simp []
+    >- (qexists_tac `Suc n` >> simp [opt_funpow_alt]) >>
+    PairCases_on `x'` >> rw [] >>
+    first_x_assum drule >> rw [] >>
+    first_x_assum (qspec_then `Suc n` mp_tac) >> simp [opt_funpow_def] >>
+    rw [] >>
+    qexists_tac `Suc m` >> rw [opt_funpow_alt]) >>
+  metis_tac [unfold_finite_funpow, opt_funpow_def]
+QED
+
 export_theory ();

sledge/semantics/settingsScript.sml

@@ -55,5 +55,6 @@ overload_on ("map2", ``list$MAP2``);
 overload_on ("foldl", ``FOLDL``);
 overload_on ("foldr", ``FOLDR``);
 overload_on ("option_rel", ``OPTREL``);
+overload_on ("front", ``FRONT``);
 
 export_theory ();