Package machine-code-straightline: Hoare logic triple support for straightline code

Information

Files

• Package tarball machine-code-straightline-1.0.tgz
• Theory source file machine-code-straightline.thy (included in the package tarball)

Defined Type Operators

• HOL4
  • GraphLang
    • GraphLang.code
    • GraphLang.func
    • GraphLang.graph_function
    • GraphLang.inst
    • GraphLang.jump
    • GraphLang.next
    • GraphLang.next_node
    • GraphLang.node
    • GraphLang.variable

Defined Constants

• HOL4
  • straightline
    • straightline.arm_assert
    • straightline.DO_NOTHING
  • GraphLang
    • GraphLang.all_names
    • GraphLang.all_names_ignore
    • GraphLang.all_names_with_input
    • GraphLang.apply_update
    • GraphLang.arm_STACK_MEMORY
    • GraphLang.arm_STATE
    • GraphLang.arm_STATE_CPSR
    • GraphLang.arm_STATE_REGS
    • GraphLang.arm_assert_for
    • GraphLang.carry_out
    • GraphLang.check_jump
    • GraphLang.check_ret
    • GraphLang.code_CASE
    • GraphLang.code_size
    • GraphLang.count_leading_zero_bits
    • GraphLang.default_state
    • GraphLang.exec_graph
    • GraphLang.exec_graph_n
    • GraphLang.exec_graph_step
    • GraphLang.exec_next
    • GraphLang.exec_node
    • GraphLang.exec_node_return
    • GraphLang.find_func
    • GraphLang.find_func_tupled
    • GraphLang.find_inst
    • GraphLang.find_inst_tupled
    • GraphLang.fold
    • GraphLang.fs_locs
    • GraphLang.func_CASE
    • GraphLang.func_body_trans
    • GraphLang.func_name
    • GraphLang.func_ok
    • GraphLang.func_size
    • GraphLang.func_trans
    • GraphLang.funcs_ok
    • GraphLang.get_assert
    • GraphLang.get_jump
    • GraphLang.good_stack
    • GraphLang.good_stack_tail
    • GraphLang.good_stack_tail_tupled
    • GraphLang.graph
    • GraphLang.graph_function_CASE
    • GraphLang.graph_function_size
    • GraphLang.init_vars
    • GraphLang.inst_CASE
    • GraphLang.inst_loc
    • GraphLang.inst_size
    • GraphLang.inst_trans
    • GraphLang.jump_CASE
    • GraphLang.jump_ok
    • GraphLang.jump_size
    • GraphLang.list_func_trans
    • GraphLang.list_inst_trans
    • GraphLang.m0_STACK_MEMORY
    • GraphLang.m0_STATE
    • GraphLang.m0_STATE_PSR
    • GraphLang.m0_STATE_REGS
    • GraphLang.m0_assert_for
    • GraphLang.next_CASE
    • GraphLang.next_node_CASE
    • GraphLang.next_node_size
    • GraphLang.next_ok
    • GraphLang.next_size
    • GraphLang.next_trans
    • GraphLang.next_trans_tupled
    • GraphLang.next_trans_tupled_aux
    • GraphLang.node_CASE
    • GraphLang.node_size
    • GraphLang.odd_nums
    • GraphLang.ret_and_all_names
    • GraphLang.return_vars
    • GraphLang.save_vals
    • GraphLang.unspecified_pre
    • GraphLang.upd_ok
    • GraphLang.upd_stack
    • GraphLang.upd_vars
    • GraphLang.var_acc
    • GraphLang.var_bool
    • GraphLang.var_dom
    • GraphLang.var_mem
    • GraphLang.var_nat
    • GraphLang.var_upd
    • GraphLang.var_word32
    • GraphLang.var_word8
    • GraphLang.variable_CASE
    • GraphLang.variable_size
    • GraphLang.word32
    • GraphLang.word_add_with_carry
    • GraphLang.ARM
    • GraphLang.ASM
    • GraphLang.Basic
    • GraphLang.CALL
    • GraphLang.CALL_TAG
    • GraphLang.Call
    • GraphLang.Cond
    • GraphLang.Err
    • GraphLang.Func
    • GraphLang.GraphFunction
    • GraphLang.IF
    • GraphLang.IMPL_INST
    • GraphLang.Inst
    • GraphLang.Jump
    • GraphLang.LIST_IMPL_INST
    • GraphLang.LIST_IMPL_INST_tupled
    • GraphLang.LIST_SUBSET
    • GraphLang.M0
    • GraphLang.MemAcc32
    • GraphLang.MemAcc8
    • GraphLang.MemUpdate32
    • GraphLang.MemUpdate8
    • GraphLang.NextNode
    • GraphLang.READ32
    • GraphLang.READ8
    • GraphLang.Ret
    • GraphLang.Return
    • GraphLang.SKIP_TAG
    • GraphLang.ShiftLeft
    • GraphLang.ShiftRight
    • GraphLang.SignedShiftRight
    • GraphLang.Skip
    • GraphLang.VarBool
    • GraphLang.VarDom
    • GraphLang.VarMem
    • GraphLang.VarNat
    • GraphLang.VarNone
    • GraphLang.VarWord32
    • GraphLang.VarWord8
    • GraphLang.WRITE32
    • GraphLang.WRITE8

Theorems

⊦ GraphLang.unspecified_pre ⇔ ⊥

⊦ GraphLang.arm_STACK_MEMORY = arm_prog.arm_MEMORY

⊦ GraphLang.m0_STACK_MEMORY = m0_prog.m0_MEMORY

⊦ GraphLang.default_state = λx. GraphLang.VarNone

⊦ (λv₁. v₁) = id

⊦ GraphLang.apply_update [] s = s

⊦ (x ⇔ ⊤) ⇒ x

⊦ (⊤ ⇒ b) ⇒ b

⊦ ∀x. straightline.DO_NOTHING x = x

⊦ ∀s. GraphLang.SKIP_TAG s ⇔ GraphLang.unspecified_pre

⊦ ∀a. ¬(GraphLang.Jump a = GraphLang.Return)

⊦ ∀f. GraphLang.func_body_trans f = snd (GraphLang.func_trans f)

⊦ ∀w.
    GraphLang.count_leading_zero_bits w =
    words.n2w (arm.CountLeadingZeroBits w)

⊦ ∀Gamma.
    GraphLang.exec_graph Gamma =
    relation.RTC (GraphLang.exec_graph_step Gamma)

⊦ ∀s is_tail_call. GraphLang.CALL_TAG s is_tail_call ⇔ ⊤

⊦ ∀fs.
    GraphLang.list_func_trans fs =
    GraphLang.graph (map GraphLang.func_trans fs)

⊦ ∀nn. GraphLang.Skip nn = GraphLang.Cond nn nn (λx. ⊤)

⊦ ∀nm f. GraphLang.var_acc nm f = f nm

⊦ ∀a mem. GraphLang.READ8 a mem = mem a

⊦ ∀a' a. ¬(GraphLang.ARM a = GraphLang.M0 a')

⊦ ¬(x = y) ⇔ ¬(y = x)

⊦ ∀m a. GraphLang.MemAcc8 m a = GraphLang.READ8 a m

⊦ ∀m a. GraphLang.MemAcc32 m a = GraphLang.READ32 a m

⊦ ∀jj. (∃c. jj = GraphLang.Jump c) ∨ jj = GraphLang.Return

⊦ ∀x x₁. GraphLang.find_func x x₁ = GraphLang.find_func_tupled (x, x₁)

⊦ ∀x x₁.
    GraphLang.good_stack_tail x x₁ ⇔
    GraphLang.good_stack_tail_tupled (x, x₁)

⊦ ∀w y. GraphLang.ShiftLeft w y = words.word_lsl w (words.w2n y)

⊦ ∀w y. GraphLang.ShiftRight w y = words.word_lsr w (words.w2n y)

⊦ ∀w y. GraphLang.SignedShiftRight w y = words.word_asr w (words.w2n y)

⊦ ∀Gamma n.
    GraphLang.exec_graph_n Gamma n =
    arithmetic.NRC (GraphLang.exec_graph_step Gamma) n

⊦ ∀x x₁. GraphLang.find_inst x x₁ = GraphLang.find_inst_tupled (x, x₁)

⊦ arm.Aligned (w, n) ⇒ arm.Align (w, n) = w

⊦ set_sep.STAR set_sep.emp p = p ∧ set_sep.STAR p set_sep.emp = p

⊦ ∀name entry l. GraphLang.func_name (GraphLang.Func name entry l) = name

⊦ GraphLang.list_func_trans fs =
  GraphLang.graph
    (map (λf. (GraphLang.func_name f, GraphLang.func_body_trans f)) fs)

⊦ ∀ff. ∃s c l. ff = GraphLang.Func s c l

⊦ ∀ii. ∃c f n. ii = GraphLang.Inst c f n

⊦ ∀a a'. GraphLang.NextNode a = GraphLang.NextNode a' ⇔ a = a'

⊦ ∀a a'. GraphLang.Jump a = GraphLang.Jump a' ⇔ a = a'

⊦ const x = (λy. x) ∧ suc = λn. n + 1

⊦ GraphLang.get_assert none = (λx. ⊤) ∧
  ∀a. GraphLang.get_assert (some a) = a

⊦ ∀loc v₀ v₁. GraphLang.inst_loc (GraphLang.Inst loc v₀ v₁) = words.w2n loc

⊦ (∀a. GraphLang.jump_size (GraphLang.Jump a) = 1) ∧
  GraphLang.jump_size GraphLang.Return = 0

⊦ ∀code fs.
    GraphLang.funcs_ok code fs ⇔
    all (GraphLang.func_ok code (GraphLang.fs_locs fs)) fs

⊦ address.ALIGNED w ⇒ ¬fcp.fcp_index w 0 ∧ ¬fcp.fcp_index w 1

⊦ words.n2w (arm.CountLeadingZeroBits w) =
  GraphLang.count_leading_zero_bits w ∧
  words.n2w (m0.CountLeadingZeroBits w) =
  GraphLang.count_leading_zero_bits w

⊦ ∀nm v f. GraphLang.var_upd nm v f = combin.UPDATE nm v f

⊦ ∀cc. (∃f. cc = GraphLang.ARM f) ∨ ∃f. cc = GraphLang.M0 f

⊦ ∀xs ys.
    GraphLang.LIST_SUBSET xs ys ⇔
    all (λx. bool.IN x (list.LIST_TO_SET ys)) xs

⊦ ∀P. (∀c. P (GraphLang.Jump c)) ∧ P GraphLang.Return ⇒ ∀jj. P jj

⊦ ∀a w mem. GraphLang.WRITE8 a w mem = combin.UPDATE a w mem

⊦ ∀m a w. GraphLang.MemUpdate8 m a w = GraphLang.WRITE8 a w m

⊦ ∀m a w. GraphLang.MemUpdate32 m a w = GraphLang.WRITE32 a w m

⊦ all (λn. s₁ n = s₂ n) GraphLang.all_names ⇒
  GraphLang.arm_STATE s₁ = GraphLang.arm_STATE s₂

⊦ all (λn. s₁ n = s₂ n) GraphLang.all_names ⇒
  GraphLang.m0_STATE s₁ = GraphLang.m0_STATE s₂

⊦ (∀p. GraphLang.jump_ok (GraphLang.Jump p) ⇔ even (words.w2n p)) ∧
  (GraphLang.jump_ok GraphLang.Return ⇔ ⊤)

⊦ (∀j.
     GraphLang.get_jump (GraphLang.Jump j) =
     GraphLang.NextNode (words.w2n j)) ∧
  GraphLang.get_jump GraphLang.Return = GraphLang.Ret

⊦ ∀gg. ∃l l₀ f n. gg = GraphLang.GraphFunction l l₀ f n

⊦ ∀u.
    GraphLang.upd_ok u ⇔
    list.ALL_DISTINCT (map fst u) ∧
    GraphLang.LIST_SUBSET (map fst u) GraphLang.all_names

⊦ ∀nn.
    (∃n. nn = GraphLang.NextNode n) ∨ nn = GraphLang.Ret ∨
    nn = GraphLang.Err

⊦ set_sep.STAR (if b then x else y) q =
  if b then set_sep.STAR x q else set_sep.STAR y q

⊦ t₁ = t₂ ∧ u₁ = u₂ ⇒ (t₁, u₁) = (t₂, u₂)

⊦ ∀x x₁ x₂.
    GraphLang.LIST_IMPL_INST x x₁ x₂ ⇔
    GraphLang.LIST_IMPL_INST_tupled (x, x₁, x₂)

⊦ ∀x x₁ x₂.
    GraphLang.next_trans x x₁ x₂ = GraphLang.next_trans_tupled (x, x₁, x₂)

⊦ ∀P. (∀s c l. P (GraphLang.Func s c l)) ⇒ ∀ff. P ff

⊦ ∀P. (∀c f n. P (GraphLang.Inst c f n)) ⇒ ∀ii. P ii

⊦ ∀a₀ a₁ a₂.
    GraphLang.inst_size (GraphLang.Inst a₀ a₁ a₂) =
    1 + GraphLang.next_size a₂

⊦ ∀P. (∀f. P (GraphLang.ARM f)) ∧ (∀f. P (GraphLang.M0 f)) ⇒ ∀cc. P cc

⊦ (∀a. GraphLang.code_size (GraphLang.ARM a) = 1) ∧
  ∀a. GraphLang.code_size (GraphLang.M0 a) = 1

⊦ ∀xs n ys. list.DROP (length xs + n) (xs @ ys) = list.DROP n ys

⊦ ∀P.
    (∀n. P (GraphLang.NextNode n)) ∧ P GraphLang.Ret ∧ P GraphLang.Err ⇒
    ∀nn. P nn

⊦ ∀w₁ w₂ c.
    GraphLang.word_add_with_carry w₁ w₂ c =
    fst (words.add_with_carry (w₁, w₂, c))

⊦ ∀vars accs st.
    GraphLang.init_vars vars accs st =
    GraphLang.save_vals vars (map (λi. i st) accs) GraphLang.default_state

⊦ ∀a₀ a₁ a₂ f. GraphLang.func_CASE (GraphLang.Func a₀ a₁ a₂) f = f a₀ a₁ a₂

⊦ ∀inner outer inner_st.
    GraphLang.return_vars inner outer inner_st =
    GraphLang.save_vals outer
      (map (λv. GraphLang.var_acc v inner_st) inner)

⊦ ∀a₀ a₁ a₂ f. GraphLang.inst_CASE (GraphLang.Inst a₀ a₁ a₂) f = f a₀ a₁ a₂

⊦ ∀f₀ f₁.
    ∃fn. (∀a. fn (GraphLang.Jump a) = f₀ a) ∧ fn GraphLang.Return = f₁

⊦ ∀asm.
    prog.SPEC arm_prog.ARM_MODEL
      (set_sep.STAR (arm_prog.arm_PC p)
         (set_sep.cond (GraphLang.SKIP_TAG asm))) pred_set.EMPTY
      (arm_prog.arm_PC (words.word_add p (words.n2w (arithmetic.BIT2 1))))

⊦ ∀w₁ w₂ c.
    GraphLang.carry_out w₁ w₂ c ⇔
    fst (snd (words.add_with_carry (w₁, w₂, c)))

⊦ ∀f. ∃fn. ∀a₀ a₁ a₂. fn (GraphLang.Func a₀ a₁ a₂) = f a₀ a₁ a₂

⊦ ∀f. ∃fn. ∀a₀ a₁ a₂. fn (GraphLang.Inst a₀ a₁ a₂) = f a₀ a₁ a₂

⊦ GraphLang.IMPL_INST c locs (GraphLang.Inst n (const ⊤) next) ⇒
  ∀a. GraphLang.IMPL_INST c locs (GraphLang.Inst n a next)

⊦ ∀t l v₀ next.
    GraphLang.inst_trans t (GraphLang.Inst l v₀ next) =
    GraphLang.next_trans (words.w2n l) t next

⊦ ∀P. (∀l l₀ f n. P (GraphLang.GraphFunction l l₀ f n)) ⇒ ∀gg. P gg

⊦ ∀upds st.
    GraphLang.upd_vars upds st =
    GraphLang.save_vals (map fst upds)
      (map (pair.UNCURRY (λnm vf. vf st)) upds) st

⊦ ¬fcp.fcp_index w 0 ∧ ¬fcp.fcp_index w 1 ⇒
  (b ⇒ address.ALIGNED w ⇔ address.ALIGNED w)

⊦ GraphLang.func_ok code locs f ∧ all (GraphLang.func_ok code locs) fs ⇒
  all (GraphLang.func_ok code locs) (f :: fs)

⊦ ∀b₁ b₂ b₃ b₄.
    GraphLang.word32 b₁ b₂ b₃ b₄ =
    words.word_concat b₁ (words.word_concat b₂ (words.word_concat b₃ b₄))

⊦ (∀a. ¬(GraphLang.NextNode a = GraphLang.Ret)) ∧
  (∀a. ¬(GraphLang.NextNode a = GraphLang.Err)) ∧
  ¬(GraphLang.Ret = GraphLang.Err)

⊦ ∀fs stack.
    GraphLang.good_stack fs stack ⇔
    GraphLang.good_stack_tail fs stack ∧
    GraphLang.next_node_CASE (fst (head stack)) (λn. even n) ⊤ ⊥

⊦ (∀a. GraphLang.next_node_size (GraphLang.NextNode a) = 1 + a) ∧
  GraphLang.next_node_size GraphLang.Ret = 0 ∧
  GraphLang.next_node_size GraphLang.Err = 0

⊦ ∀vars vals st.
    GraphLang.save_vals vars vals st =
    GraphLang.fold (pair.UNCURRY (λvar val. GraphLang.var_upd var val))
      (list.ZIP (vars, vals)) st

⊦ ∀a₀ a₁ a₂.
    GraphLang.func_size (GraphLang.Func a₀ a₁ a₂) =
    1 +
    (list.list_size string.char_size a₀ +
     list.list_size GraphLang.inst_size a₂)

⊦ ∀a₀ a₁ a₂ a₃ f.
    GraphLang.graph_function_CASE (GraphLang.GraphFunction a₀ a₁ a₂ a₃) f =
    f a₀ a₁ a₂ a₃

⊦ ∀f₀ f₁.
    ∃fn. (∀a. fn (GraphLang.ARM a) = f₀ a) ∧ ∀a. fn (GraphLang.M0 a) = f₁ a

⊦ ∀xs n. n ≤ length xs ⇒ ∃ys zs. xs = ys @ zs ∧ length ys = n

⊦ ∀nm st.
    GraphLang.var_bool nm st ⇔
    GraphLang.variable_CASE (GraphLang.var_acc nm st) ⊥ (λv₆. ⊥) (λv₇. ⊥)
      (λv₈. ⊥) (λv₉. ⊥) (λv₁₀. ⊥) (λq. q)

⊦ ∀nm st.
    GraphLang.var_nat nm st =
    GraphLang.variable_CASE (GraphLang.var_acc nm st) 0 (λn. n) (λv₇. 0)
      (λv₈. 0) (λv₉. 0) (λv₁₀. 0) (λv₁₁. 0)

⊦ ∀nm st.
    GraphLang.var_dom nm st =
    GraphLang.variable_CASE (GraphLang.var_acc nm st) pred_set.EMPTY
      (λv₆. pred_set.EMPTY) (λv₇. pred_set.EMPTY) (λv₈. pred_set.EMPTY)
      (λv₉. pred_set.EMPTY) (λd. d) (λv₁₁. pred_set.EMPTY)

⊦ ∀f.
    ∃fn.
      ∀a₀ a₁ a₂ a₃.
        fn (GraphLang.GraphFunction a₀ a₁ a₂ a₃) = f a₀ a₁ a₂ a₃

⊦ words.word_msb (words.n2w n) ⇔
  n div arithmetic.BIT2 0 ↑ 31 mod arithmetic.BIT2 0 = 1

⊦ ∀name entry l.
    GraphLang.func_trans (GraphLang.Func name entry l) =
    (name,
     GraphLang.GraphFunction GraphLang.ret_and_all_names
       GraphLang.all_names_with_input
       (GraphLang.graph (GraphLang.list_inst_trans 1 l)) (words.w2n entry))

⊦ ∀insts.
    GraphLang.LIST_IMPL_INST code names insts ⇒
    list.ALL_DISTINCT (map GraphLang.inst_loc insts) ∧
    even (words.w2n entry) ⇒
    GraphLang.func_ok code names (GraphLang.Func name entry insts)

⊦ ∀P. P [] ∧ (∀x y xs. P xs ⇒ P ((x, y) :: xs)) ⇒ ∀v. P v

⊦ prog.SPEC m (set_sep.STAR p (r x)) c q ⇒
  ∀pc. pc = x ⇒ prog.SPEC m (set_sep.STAR p (r pc)) c q

⊦ prog.SPEC m (set_sep.STAR pre (res w)) code q ⇒
  ∀p. p = w ⇒ prog.SPEC m (set_sep.STAR pre (res p)) code q

⊦ (∀a f v. GraphLang.jump_CASE (GraphLang.Jump a) f v = f a) ∧
  ∀f v. GraphLang.jump_CASE GraphLang.Return f v = v

⊦ ∀P.
    P [] ∧ (∀loc state name rest. P ((loc, state, name) :: rest)) ⇒ ∀z. P z

⊦ (c_post ⇒ prog.SPEC model (assert p) code (assert post)) ⇒
  triple.TRIPLE (assert, model) (pre, p) code (pre ∧ c_post, post)

⊦ t₁ = t₂ ∧ (y₁ = y₂ ⇒ u₁ = u₂) ⇒ y₁ = y₂ ⇒ (t₁, u₁) = (t₂, u₂)

⊦ (x₁ = x₂ ⇒ t₁ = t₂) ∧ u₁ = u₂ ⇒ x₁ = x₂ ⇒ (t₁, u₁) = (t₂, u₂)

⊦ ∀f₀ f₁ f₂.
    ∃fn.
      (∀a. fn (GraphLang.NextNode a) = f₀ a) ∧ fn GraphLang.Ret = f₁ ∧
      fn GraphLang.Err = f₂

⊦ GraphLang.graph [] = const none ∧
  ∀y xs x.
    GraphLang.graph ((x, y) :: xs) =
    combin.UPDATE x (some y) (GraphLang.graph xs)

⊦ (∀k. GraphLang.odd_nums k 0 = []) ∧
  ∀k n.
    GraphLang.odd_nums k (suc n) =
    k :: GraphLang.odd_nums (k + arithmetic.BIT2 0) n

⊦ const = (λx y. x) ∧
  (address.ALIGNED x ⇔ words.word_and x (words.n2w 3) = words.n2w 0) ∧
  list.REV xs [] = reverse xs

⊦ GraphLang.IMPL_INST code names (GraphLang.Inst i (const ⊤) next) ∧
  GraphLang.LIST_IMPL_INST code names xs ⇒
  GraphLang.LIST_IMPL_INST code names
    (GraphLang.Inst i (const ⊤) next :: xs)

⊦ ∀P.
    P [] ∧
    (∀name entry l xs. P xs ⇒ P (GraphLang.Func name entry l :: xs)) ⇒
    ∀fs. P fs

⊦ (∀a a'. GraphLang.ARM a = GraphLang.ARM a' ⇔ a = a') ∧
  ∀a a'. GraphLang.M0 a = GraphLang.M0 a' ⇔ a = a'

⊦ prog.SPEC arm_prog.ARM_MODEL
    (set_sep.STAR (set_sep.STAR (aPC p) (aR (words.n2w 0) r₀))
       (set_sep.cond GraphLang.unspecified_pre)) pred_set.EMPTY
    (set_sep.STAR (aR (words.n2w 0) bool.ARB)
       (aPC (words.word_add p (words.n2w (arithmetic.BIT2 1)))))

⊦ list.EL (length xs + n) (reverse xs @ ys) = list.EL n ys ∧
  list.EL (length xs) (reverse xs @ ys) = list.EL 0 ys

⊦ GraphLang.fs_locs [] = const none ∧
  ∀xs name l entry.
    GraphLang.fs_locs (GraphLang.Func name entry l :: xs) =
    combin.UPDATE name (some entry) (GraphLang.fs_locs xs)

⊦ (∀a f f₁. GraphLang.code_CASE (GraphLang.ARM a) f f₁ = f a) ∧
  ∀a f f₁. GraphLang.code_CASE (GraphLang.M0 a) f f₁ = f₁ a

⊦ ∀nm st.
    GraphLang.var_word8 nm st =
    GraphLang.variable_CASE (GraphLang.var_acc nm st) (words.n2w 0)
      (λv₆. words.n2w 0) (λw. w) (λv₈. words.n2w 0) (λv₉. words.n2w 0)
      (λv₁₀. words.n2w 0) (λv₁₁. words.n2w 0)

⊦ ∀nm st.
    GraphLang.var_word32 nm st =
    GraphLang.variable_CASE (GraphLang.var_acc nm st) (words.n2w 0)
      (λv₆. words.n2w 0) (λv₇. words.n2w 0) (λw. w) (λv₉. words.n2w 0)
      (λv₁₀. words.n2w 0) (λv₁₁. words.n2w 0)

⊦ ∀a₀ a₁ a₂ a₃.
    GraphLang.graph_function_size (GraphLang.GraphFunction a₀ a₁ a₂ a₃) =
    1 +
    (list.list_size (list.list_size string.char_size) a₀ +
     (list.list_size (list.list_size string.char_size) a₁ + a₃))

⊦ ∀n xs ys.
    list.EL (length xs) (xs @ ys) = list.EL 0 ys ∧
    list.EL (length xs + n) (xs @ ys) = list.EL n ys

⊦ ∀a x p c q.
    (a ⇒ prog.SPEC x p c q) ⇒
    ∀d. pred_set.SUBSET c d ⇒ a ⇒ prog.SPEC x p d q

⊦ GraphLang.IMPL_INST c locs
    (GraphLang.Inst n (const ⊤) (GraphLang.IF g next₁ next₂)) ⇒
  ∀a.
    (∀s. a s ⇒ g s) ⇒ GraphLang.IMPL_INST c locs (GraphLang.Inst n a next₁)

⊦ (∀s. GraphLang.apply_update [] s = s) ∧
  ∀y xs x s.
    GraphLang.apply_update ((x, y) :: xs) s =
    combin.UPDATE x (y s) (GraphLang.apply_update xs s)

⊦ prog.SPEC m (set_sep.STAR p (f x)) c (set_sep.STAR q (f x)) ⇔
  ∀v. v = x ⇒ prog.SPEC m (set_sep.STAR p (f v)) c (set_sep.STAR q (f v))

⊦ ∀a mem.
    GraphLang.READ32 a mem =
    GraphLang.word32 (mem (words.word_add a (words.n2w 3)))
      (mem (words.word_add a (words.n2w (arithmetic.BIT2 0))))
      (mem (words.word_add a (words.n2w 1))) (mem a)

⊦ (∀t. GraphLang.list_inst_trans t [] = []) ∧
  ∀t x xs.
    GraphLang.list_inst_trans t (x :: xs) =
    bool.LET (pair.UNCURRY (λt₁ ys. ys @ GraphLang.list_inst_trans t₁ xs))
      (GraphLang.inst_trans t x)

⊦ snd (snd (words.add_with_carry (x, y, c))) ⇔
  (words.word_msb x ⇔ words.word_msb y) ∧
  ¬(words.word_msb x ⇔
     words.word_msb
       (if c then words.word_sub x (words.word_1comp y)
        else words.word_add x y))

⊦ (∀f s. GraphLang.fold f [] s = s) ∧
  ∀f x xs s. GraphLang.fold f (x :: xs) s = GraphLang.fold f xs (f x s)

⊦ ∀nm st.
    GraphLang.var_mem nm st =
    GraphLang.variable_CASE (GraphLang.var_acc nm st) (λv₈. words.n2w 0)
      (λv₆ v₈. words.n2w 0) (λv₇ v₈. words.n2w 0) (λv₈ v₈. words.n2w 0)
      (λm. m) (λv₁₀ v₈. words.n2w 0) (λv₁₁ v₈. words.n2w 0)

⊦ ∀a₀ a₁ a₂ a0' a1' a2'.
    GraphLang.Func a₀ a₁ a₂ = GraphLang.Func a0' a1' a2' ⇔
    a₀ = a0' ∧ a₁ = a1' ∧ a₂ = a2'

⊦ ∀a₀ a₁ a₂ a0' a1' a2'.
    GraphLang.Inst a₀ a₁ a₂ = GraphLang.Inst a0' a1' a2' ⇔
    a₀ = a0' ∧ a₁ = a1' ∧ a₂ = a2'

⊦ GraphLang.IMPL_INST c locs
    (GraphLang.Inst n (const ⊤) (GraphLang.IF g next₁ next₂)) ⇒
  ∀a.
    (∀s. a s ⇒ ((¬) ∘ g) s) ⇒
    GraphLang.IMPL_INST c locs (GraphLang.Inst n a next₂)

⊦ ∀P.
    (∀s. P [] s) ∧ (∀x y xs s. P xs s ⇒ P ((x, y) :: xs) s) ⇒ ∀v v₁. P v v₁

⊦ (b₁ ⇒ prog.SPEC m p c₁ q₁) ∧ (b₂ ⇒ prog.SPEC m p c₂ q₂) ⇒ (¬b₁ ⇒ b₂) ⇒
  prog.SPEC m p (pred_set.UNION c₁ c₂) (if b₁ then q₁ else q₂)

⊦ (x₁ = x₂ ⇒ t₁ = t₂) ∧ (y₁ = y₂ ⇒ u₁ = u₂) ⇒ (x₁, y₁) = (x₂, y₂) ⇒
  (t₁, u₁) = (t₂, u₂)

⊦ GraphLang.funcs_ok (GraphLang.ARM code) fs ⇒
  ∀n s₁ s₂.
    GraphLang.good_stack fs s₁ ∧ GraphLang.good_stack fs s₂ ∧
    GraphLang.exec_graph_n (GraphLang.list_func_trans fs) n s₁ s₂ ⇒
    prog.SPEC arm_prog.ARM_MODEL (GraphLang.arm_assert_for s₁) code
      (GraphLang.arm_assert_for s₂)

⊦ GraphLang.funcs_ok (GraphLang.M0 code) fs ⇒
  ∀n s₁ s₂.
    GraphLang.good_stack fs s₁ ∧ GraphLang.good_stack fs s₂ ∧
    GraphLang.exec_graph_n (GraphLang.list_func_trans fs) n s₁ s₂ ⇒
    prog.SPEC m0_prog.M0_MODEL (GraphLang.m0_assert_for s₁) code
      (GraphLang.m0_assert_for s₂)

⊦ GraphLang.func_ok code locs f ⇒
  ∀c.
    pair.pair_CASE (code, c)
      (λv₂ v₃.
         GraphLang.code_CASE v₂
           (λc₁.
              GraphLang.code_CASE v₃ (λc₂. pred_set.SUBSET c₁ c₂)
                (λv₁₁. ⊥))
           (λc1'.
              GraphLang.code_CASE v₃ (λv₁₄. ⊥)
                (λc2'. pred_set.SUBSET c1' c2'))) ⇒
    GraphLang.func_ok c locs f

⊦ GraphLang.IMPL_INST code locs (GraphLang.Inst pc₁ assert₁ next₁) ∧
  GraphLang.IMPL_INST code locs (GraphLang.Inst pc₁ assert₂ next₂) ⇒
  ∀guard.
    GraphLang.IMPL_INST code locs
      (GraphLang.Inst pc₁ (λs. if guard s then assert₁ s else assert₂ s)
         (GraphLang.IF guard next₁ next₂))

⊦ ∀nn.
    (∃n l. nn = GraphLang.Basic n l) ∨
    (∃n n₀ f. nn = GraphLang.Cond n n₀ f) ∨
    ∃n s l l₀. nn = GraphLang.Call n s l l₀

⊦ GraphLang.IMPL_INST code locs (GraphLang.Inst pc₁ assert₁ next₁) ∧
  GraphLang.IMPL_INST code locs (GraphLang.Inst pc₁ assert₂ next₂) ⇒
  (∀s. assert₁ s ⇒ assert₂ s) ⇒
  ∀guard.
    GraphLang.IMPL_INST code locs
      (GraphLang.Inst pc₁ assert₁ (GraphLang.IF guard next₁ next₂))

⊦ (∀nn stf x xs.
     GraphLang.upd_stack nn stf (x :: xs) =
     (nn, stf (fst (snd x)), snd (snd x)) :: xs) ∧
  ∀nn stf. GraphLang.upd_stack nn stf [] = []

⊦ GraphLang.graph =
  relation.WFREC
    (select R'. wellFounded R' ∧ ∀y x xs. R' xs ((x, y) :: xs))
    (λgraph a.
       list.list_CASE a (id (const none))
         (λv xs.
            pair.pair_CASE v
              (λx y. id (combin.UPDATE x (some y) (graph xs)))))

⊦ (∀n. GraphLang.find_func n [] = none) ∧
  ∀xs name n insts entry.
    GraphLang.find_func n (GraphLang.Func name entry insts :: xs) =
    if n = name then some (GraphLang.Func name entry insts)
    else GraphLang.find_func n xs

⊦ (∀n. GraphLang.find_inst n [] = none) ∧
  ∀xs next n l asrt.
    GraphLang.find_inst n (GraphLang.Inst l asrt next :: xs) =
    if l = n then some (GraphLang.Inst l asrt next)
    else GraphLang.find_inst n xs

⊦ ∀P.
    (∀n l. P (GraphLang.Basic n l)) ∧
    (∀n n₀ f. P (GraphLang.Cond n n₀ f)) ∧
    (∀n s l l₀. P (GraphLang.Call n s l l₀)) ⇒ ∀nn. P nn

⊦ ∀M M' f.
    M = M' ∧
    (∀a₀ a₁ a₂. M' = GraphLang.Func a₀ a₁ a₂ ⇒ f a₀ a₁ a₂ = f' a₀ a₁ a₂) ⇒
    GraphLang.func_CASE M f = GraphLang.func_CASE M' f'

⊦ ∀M M' f.
    M = M' ∧
    (∀a₀ a₁ a₂. M' = GraphLang.Inst a₀ a₁ a₂ ⇒ f a₀ a₁ a₂ = f' a₀ a₁ a₂) ⇒
    GraphLang.inst_CASE M f = GraphLang.inst_CASE M' f'

⊦ ∀xs x n ys.
    list.LUPDATE x (length xs) (xs @ ys) = xs @ list.LUPDATE x 0 ys ∧
    list.LUPDATE x (length xs + n) (xs @ ys) = xs @ list.LUPDATE x n ys

⊦ ∀nn.
    (∃f n n₀. nn = GraphLang.IF f n n₀) ∨
    (∃o' l j. nn = GraphLang.ASM o' l j) ∨
    ∃o' l s j. nn = GraphLang.CALL o' l s j

⊦ ∀w.
    address.ALIGNED w ⇒
    arm.Align (w, arithmetic.BIT2 0) = w ∧
    arm.Align (w, arithmetic.BIT2 1) = w ∧
    m0.Align (w, arithmetic.BIT2 0) = w ∧
    m0.Align (w, arithmetic.BIT2 1) = w

⊦ GraphLang.var_word32 n (GraphLang.apply_update ((x, y) :: xs) s) =
  if n = x then
    GraphLang.variable_CASE (y s) (words.n2w 0) (λv₆. words.n2w 0)
      (λv₇. words.n2w 0) (λw. w) (λv₉. words.n2w 0) (λv₁₀. words.n2w 0)
      (λv₁₁. words.n2w 0)
  else GraphLang.var_word32 n (GraphLang.apply_update xs s)

⊦ ∀P.
    (∀n. P n []) ∧
    (∀n name entry insts xs.
       (¬(n = name) ⇒ P n xs) ⇒
       P n (GraphLang.Func name entry insts :: xs)) ⇒ ∀v v₁. P v v₁

⊦ ∀P.
    (∀n. P n []) ∧
    (∀n l asrt next xs.
       (¬(l = n) ⇒ P n xs) ⇒ P n (GraphLang.Inst l asrt next :: xs)) ⇒
    ∀v v₁. P v v₁

⊦ ∀a₀ a₁ a₂ a₃ a0' a1' a2' a3'.
    GraphLang.GraphFunction a₀ a₁ a₂ a₃ =
    GraphLang.GraphFunction a0' a1' a2' a3' ⇔
    a₀ = a0' ∧ a₁ = a1' ∧ a₂ = a2' ∧ a₃ = a3'

⊦ GraphLang.fs_locs =
  relation.WFREC
    (select R'.
       wellFounded R' ∧
       ∀l entry name xs. R' xs (GraphLang.Func name entry l :: xs))
    (λfs_locs a.
       list.list_CASE a (id (const none))
         (λv xs.
            GraphLang.func_CASE v
              (λname entry l.
                 id (combin.UPDATE name (some entry) (fs_locs xs)))))

⊦ bitstring.v2w
    (bitstring.field_insert 31 (arithmetic.BIT2 7)
       (bitstring.field 15 0 (bitstring.w2v w)) (bitstring.w2v v)) =
  words.bit_field_insert 31 (arithmetic.BIT2 7) w v

⊦ ∀M M' f v.
    M = M' ∧ (∀a. M' = GraphLang.Jump a ⇒ f a = f' a) ∧
    (M' = GraphLang.Return ⇒ v = v') ⇒
    GraphLang.jump_CASE M f v = GraphLang.jump_CASE M' f' v'

⊦ (∀a f v v₁.
     GraphLang.next_node_CASE (GraphLang.NextNode a) f v v₁ = f a) ∧
  (∀f v v₁. GraphLang.next_node_CASE GraphLang.Ret f v v₁ = v) ∧
  ∀f v v₁. GraphLang.next_node_CASE GraphLang.Err f v v₁ = v₁

⊦ ∀P.
    P GraphLang.VarNone ∧ (∀a. P (GraphLang.VarNat a)) ∧
    (∀a. P (GraphLang.VarWord8 a)) ∧ (∀a. P (GraphLang.VarWord32 a)) ∧
    (∀a. P (GraphLang.VarMem a)) ∧ (∀a. P (GraphLang.VarDom a)) ∧
    (∀a. P (GraphLang.VarBool a)) ⇒ ∀x. P x

⊦ ∀M M' f.
    M = M' ∧
    (∀a₀ a₁ a₂ a₃.
       M' = GraphLang.GraphFunction a₀ a₁ a₂ a₃ ⇒
       f a₀ a₁ a₂ a₃ = f' a₀ a₁ a₂ a₃) ⇒
    GraphLang.graph_function_CASE M f = GraphLang.graph_function_CASE M' f'

⊦ ∀P.
    (∀code names. P code names []) ∧
    (∀code names i assert next xs.
       P code names xs ⇒
       P code names (GraphLang.Inst i assert next :: xs)) ⇒
    ∀v v₁ v₂. P v v₁ v₂

⊦ (words.word_sub a
     (words.word_mul (words.n2w (l + n)) (words.n2w (arithmetic.BIT2 1))) =
   words.word_sub r₁₃
     (words.word_mul (words.n2w (arithmetic.BIT2 1)) (words.n2w l)) ⇒ b) ⇒
  address.ALIGNED a ∧ address.ALIGNED r₁₃ ∧
  n = words.w2n (words.word_sub a r₁₃) div arithmetic.BIT2 1 ⇒ b

⊦ ∀x.
    x = GraphLang.VarNone ∨ (∃n. x = GraphLang.VarNat n) ∨
    (∃c. x = GraphLang.VarWord8 c) ∨ (∃c. x = GraphLang.VarWord32 c) ∨
    (∃f. x = GraphLang.VarMem f) ∨ (∃f. x = GraphLang.VarDom f) ∨
    ∃b. x = GraphLang.VarBool b

⊦ ∀M M' f f₁.
    M = M' ∧ (∀a. M' = GraphLang.ARM a ⇒ f a = f' a) ∧
    (∀a. M' = GraphLang.M0 a ⇒ f₁ a = f1' a) ⇒
    GraphLang.code_CASE M f f₁ = GraphLang.code_CASE M' f' f1'

⊦ GraphLang.IMPL_INST c locs
    (GraphLang.Inst n b
       (GraphLang.IF g (GraphLang.ASM x u (GraphLang.Jump j)) next)) ⇔
  GraphLang.IMPL_INST c locs
    (GraphLang.Inst n (λs. b s ∧ g s)
       (GraphLang.ASM x u (GraphLang.Jump j))) ∧
  GraphLang.IMPL_INST c locs (GraphLang.Inst n (λs. b s ∧ ¬g s) next)

⊦ ∀P.
    (∀n n₀. P n ∧ P n₀ ⇒ ∀f. P (GraphLang.IF f n n₀)) ∧
    (∀o' l j. P (GraphLang.ASM o' l j)) ∧
    (∀o' l s j. P (GraphLang.CALL o' l s j)) ⇒ ∀n. P n

⊦ (address.ALIGNED (arm.Align (w, arithmetic.BIT2 0)) ⇔
   ¬fcp.fcp_index w 1) ∧
  (address.ALIGNED (arm.Align (w, arithmetic.BIT2 1)) ⇔ ⊤) ∧
  (address.ALIGNED (m0.Align (w, arithmetic.BIT2 0)) ⇔
   ¬fcp.fcp_index w 1) ∧
  (address.ALIGNED (m0.Align (w, arithmetic.BIT2 1)) ⇔ ⊤)

⊦ (∀k. GraphLang.odd_nums k 0 = []) ∧
  (∀k n.
     GraphLang.odd_nums k (bit1 n) =
     k ::
     GraphLang.odd_nums (k + arithmetic.BIT2 0)
       (arithmetic.- (bit1 n) 1)) ∧
  ∀k n.
    GraphLang.odd_nums k (arithmetic.BIT2 n) =
    k :: GraphLang.odd_nums (k + arithmetic.BIT2 0) (bit1 n)

⊦ (∀names code. GraphLang.LIST_IMPL_INST code names [] ⇔ ⊤) ∧
  ∀xs next names i code assert.
    GraphLang.LIST_IMPL_INST code names
      (GraphLang.Inst i assert next :: xs) ⇔
    GraphLang.IMPL_INST code names (GraphLang.Inst i assert next) ∧
    assert = const ⊤ ∧ GraphLang.LIST_IMPL_INST code names xs

⊦ GraphLang.IMPL_INST code locs
    (GraphLang.Inst pc assert
       (GraphLang.IF guard (GraphLang.ASM (some s₁) up₁ j₁)
          (GraphLang.ASM (some s₂) up₂ j₂))) ⇔
  GraphLang.IMPL_INST code locs
    (GraphLang.Inst pc assert
       (GraphLang.IF guard
          (GraphLang.ASM (some (λs. guard s ⇒ s₁ s)) up₁ j₁)
          (GraphLang.ASM (some (λs. ¬guard s ⇒ s₂ s)) up₂ j₂)))

⊦ ∀code names name entry l.
    GraphLang.func_ok code names (GraphLang.Func name entry l) ⇔
    list.ALL_DISTINCT (map GraphLang.inst_loc l) ∧ even (words.w2n entry) ∧
    ∀i assert next.
      bool.IN (GraphLang.Inst i assert next) (list.LIST_TO_SET l) ⇒
      GraphLang.IMPL_INST code names (GraphLang.Inst i assert next) ∧
      assert = const ⊤

⊦ GraphLang.IMPL_INST c locs
    (GraphLang.Inst n b
       (GraphLang.IF g (GraphLang.ASM pre u₁ (GraphLang.Jump w)) next)) ∧
  GraphLang.IMPL_INST c locs
    (GraphLang.Inst w g (GraphLang.ASM none [] (GraphLang.Jump j))) ⇒
  (∀s. g s ⇒ g (GraphLang.apply_update u₁ s)) ⇒
  GraphLang.IMPL_INST c locs
    (GraphLang.Inst n b
       (GraphLang.IF g (GraphLang.ASM pre u₁ (GraphLang.Jump j)) next))

⊦ ∀M M' f v v₁.
    M = M' ∧ (∀a. M' = GraphLang.NextNode a ⇒ f a = f' a) ∧
    (M' = GraphLang.Ret ⇒ v = v') ∧ (M' = GraphLang.Err ⇒ v₁ = v1') ⇒
    GraphLang.next_node_CASE M f v v₁ =
    GraphLang.next_node_CASE M' f' v' v1'

⊦ ∀f₀ f₁ f₂.
    ∃fn.
      (∀a₀ a₁. fn (GraphLang.Basic a₀ a₁) = f₀ a₀ a₁) ∧
      (∀a₀ a₁ a₂. fn (GraphLang.Cond a₀ a₁ a₂) = f₁ a₀ a₁ a₂) ∧
      ∀a₀ a₁ a₂ a₃. fn (GraphLang.Call a₀ a₁ a₂ a₃) = f₂ a₀ a₁ a₂ a₃

⊦ GraphLang.IMPL_INST c locs
    (GraphLang.Inst n b
       (GraphLang.IF g next (GraphLang.ASM pre u₁ (GraphLang.Jump w)))) ∧
  GraphLang.IMPL_INST c locs
    (GraphLang.Inst w ((¬) ∘ g)
       (GraphLang.ASM none [] (GraphLang.Jump j))) ⇒
  (∀s. g (GraphLang.apply_update u₁ s) ⇔ g s) ⇒
  GraphLang.IMPL_INST c locs
    (GraphLang.Inst n b
       (GraphLang.IF g next (GraphLang.ASM pre u₁ (GraphLang.Jump j))))