bil.ott

indexvar index, m, n ::= {{ com subscripts}}
metavar id ::= {{ com a literal for variable}}
metavar num  ::= {{ com number literal }}
metavar string,str ::= {{ com quoted string literal }}



grammar


 insn :: insn_ ::=
   | { addr = w1 ; size = w2; code = bil }      :: S    :: insn

 bil,seq :: seq_ ::=
   | { s1 ; .. ; sn }                           :: S    :: many

 stmt,s :: stmt_ ::=
   | var := exp                                 ::      :: move
   {{ com -- assign $exp$ to $var$  }}
   | jmp e                                      ::      :: jump
   {{ com -- transfer control to a given address $e$ }}
   | cpuexn ( num )                             ::      :: cpuexn
   {{ com -- interrupt CPU with a given interrupt $num$ }}
   | special ( string )                         ::      :: special
   {{ com -- instruction with unknown semantics  }}
   | while ( exp ) seq                          ::      :: while
   {{ com -- eval $seq$ while $exp$ is true }}
   | if ( e ) seq                               :: S    :: ifthen
   {{ com -- eval $seq$ if $e$ is true }}
   | if ( e ) seq1 else seq2                    ::      :: if
   {{ com -- if $e$ is true then eval $seq_1$ else $seq_2$ }}


 exp,e :: exp_ ::=
   | ( exp )                                    :: S    :: paren
   | var                                        ::      :: var
   {{ com -- a variable }}
   | word                                       ::      :: int
   {{ com -- an immediate value }}
   | v [ w <- v' : sz ]                         ::      :: mem
   {{ com -- a memory value }}
   | e1 [ e2 , endian ] : nat                   ::      :: load
   {{ com -- load a value from address $e_2$ at storage $e_1$}}
   | e1 with [ e2 , endian ] : nat <- e3        ::      :: store
   {{ com -- update a storage $e_1$ with binding $e_2$ $\leftarrow$ $e_3$ }}
   | e1 bop e2                                  ::      :: binop
   {{ com -- perform binary operation on $e_1$ and $e_2$}}
   | uop e1                                     ::      :: unop
   {{ com -- perform an unary operation on $e_1$}}
   | cast : nat [ e ]                           ::      :: cast
   {{ com -- extract or extend bitvector $e$ }}
   | let var = e1 in e2                         ::      :: let
   {{ com -- bind $e_1$ to $var$ in expression $e_2$}}
   | unknown [ string ] : type                  ::      :: unk
   {{ com -- unknown or undefined value of a given $type$ }}
   | ite e1 e2 e3                      ::      :: ite
   {{ com -- evaluates to $e_2$ if $e_1$ is true else to $e_3$ }}
   | extract : nat1 : nat2 [ e ]                ::      :: ext
   {{ com -- extract or extend bitvector $e$}}
   | e1 @ e2                                    ::      :: concat
   {{ com -- concatenate two bitvector $e_1$ to $e_2$ }}
   | [ e1 / var ] e2                              :: M :: subst
   {{ com -- the (capture avoiding) substitution of $e_1$ for $var$ in $e_2$ }}

 var :: var_ ::=
   | id : type                                  :: S    :: var

 val,v :: val_ ::=
   | word                                      ::      :: imm
   | v [ w <- v' : sz ]                        ::      :: mem
   | unknown [ string ] : type                 ::      :: bot

 word,w :: word_ ::= {{coq sized_word}}
   | num : nat                                 :: M    :: word
   {{ coq (sized (natToWord [[nat]] [[num]])) }}
   | ( w )                                        :: S    :: paren
   {{ coq ([[w]])}}
   | 1 : nat                                   :: S    :: one
   | true                                       :: S    :: true
   {{ com -- sugar for 1:1 }}
   | false                                      :: S    :: false
   {{ com -- sugar for 0:1 }}
   | w1 .+ w2                                   :: S    :: plus
        {{ tex [[w1]] \stackrel{bv} + [[w2]] }}
        {{ com -- plus }}
   | w1 .- w2                                   :: S    :: minus
        {{ tex [[w1]] \stackrel{bv} - [[w2]] }}
        {{ com -- minus }}
   | w1 .* w2                                   :: S    :: times
        {{ tex [[w1]] \stackrel{bv} * [[w2]] }}
        {{ com -- times }}
   | w1 ./ w2                                   :: S    :: div
        {{ tex [[w1]] \stackrel{bv} / [[w2]] }}
        {{ com -- division }}
   | w1 ./$ w2                                   :: S    :: sdiv
        {{ tex [[w1]] \stackrel{sbv} / [[w2]] }}
        {{ com -- signed division }}
   | w1 .% w2                                   :: S    :: mod
        {{ tex [[w1]] \stackrel{bv} \% [[w2]] }}
        {{ com -- modulo }}
   | w1 .%$ w2                                   :: S    :: smod
        {{ tex [[w1]] \stackrel{sbv} \% [[w2]] }}
        {{ com -- signed modulo }}
   | w1 .<< w2                                   :: S    :: lsl
        {{ tex [[w1]] \stackrel{bv} \ll [[w2]] }}
        {{ com -- logical shift left }}
   | w1 .>> w2                                   :: S    :: lsr
        {{ tex [[w1]] \stackrel{bv} \gg [[w2]] }}
        {{ com -- logical shift right }}
   | w1 .~>> w2                                   :: S    :: asr
        {{ tex [[w1]] \stackrel{bv} \ggg [[w2]] }}
        {{ com -- arithmetic shift right }}
   | w1 .& w2                                   :: S    :: land
        {{ tex [[w1]] \stackrel{bv} \& [[w2]] }}
        {{ com -- bitwise and }}
   | w1 .| w2                                   :: S    :: lor
        {{ tex [[w1]] \stackrel{bv} | [[w2]] }}
        {{ com -- bitwise or }}
   | w1 .xor w2                                   :: S    :: xor
        {{ tex [[w1]] \stackrel{bv}{xor} [[w2]] }}
        {{ com -- bitwise xor }}
   | w1 .< w2                                   :: S    :: less
        {{ tex [[w1]] \stackrel{bv} < [[w2]] }}
        {{ com -- less than }}
   | w1 .<$ w2                                   :: S    :: signed_less
        {{ tex [[w1]] \stackrel{sbv} < [[w2]] }}
        {{ com -- signed less than }}
   | .- w                                       :: S    :: lneg
        {{ tex \stackrel{bv} - [[w]] }}
        {{ com -- integer negation }}
   | .~ w                                       :: S    :: lnot
        {{ tex \stackrel{bv}{\sim} [[w]] }}
        {{ com -- logical negation }}
   | w1 .@ w2                                   :: S    :: concat
        {{ tex [[w1]] \stackrel{bv} . [[w2]] }}
        {{ com -- concatenation }}
   | ext w ~ hi : sz1 ~ lo : sz2           :: S    :: extend_extract
        {{ tex [[ext]]\; [[w]] \sim [[hi]] : [[sz1]] \sim [[lo]] : [[sz2]] }}
        {{ com -- extract/extend }}
   | exts w ~ hi : sz1 ~ lo : sz2         :: S    :: extend_extract_signed
        {{ tex [[exts]]\; [[w]] \sim [[hi]] : [[sz1]] \sim [[lo]] : [[sz2]] }}
        {{ com -- signed extract/extend }}


 bop :: binop_ ::=
   | aop                                      ::      :: arith  {{ com -- arithmetic operators}}
   | lop                                      ::      :: logical  {{ com -- logical operators}}

 aop :: arithop_ ::=
   | +                                          ::      :: plus  {{ com -- plus}}
   | -                                          ::      :: minus {{ com -- minus}}
   | *                                          ::      :: times {{ com -- times}}
   | /                                          ::      :: divide {{ com -- divide}}
   | /$                                         ::      :: sdivide {{ com -- signed divide}}
        {{ tex \stackrel{signed} / }}
   | %                                          ::      :: mod {{ com -- modulo }}
   | %$                                         ::      :: smod {{ com -- signed modulo }}
        {{ tex \stackrel{signed} \% }}
   | &                                          ::      :: and {{ com -- bitwise and }}
   | |                                          ::      :: or  {{ com -- bitwise or }}
   | xor                                        ::      :: xor {{ com -- bitwise xor }}
   | '<<'                                       ::      :: lshift
        {{ com -- logical shift left }}
   | '>>'                                       ::      :: rshift
        {{ com -- logical shift right }}
   | '~>>'                                      ::      :: arshift
        {{ com -- arithmetic shift right}}

 lop :: logicop_ ::=
   | =                                          ::      :: eq  {{ com -- equality }}
   | <>                                         ::      :: neq {{ com -- non-equality }}
   | <                                          ::      :: lt  {{ com -- less than }}
   | '<='                                       ::      :: le
        {{ tex \leq }} {{ com -- less than or equal}}
   | '<$'                                       ::      :: slt {{ com -- signed less than}}
        {{ tex \stackrel{signed} < }}
   | '<=$'                                      ::      :: sle
        {{ tex \stackrel{signed} \leq }} {{ com -- signed less than or equal }}

 uop :: unop_ ::=
   | -                                          ::      :: neg {{ com -- unary negation}}
   | ~                                          ::      :: not {{ com -- bitwise complement}}

 nat,sz :: nat_ ::=
   | 0                                          :: M    :: zero
   | 1                                          :: M    :: one
   | 8                                          :: M    :: byte
   | nat1 + nat2                                :: M    :: nat_plus
   | nat1 - nat2                                :: M    :: nat_minus
   | ( nat )                                    :: M    :: nat_paren

 endian,ed :: endian_ ::=
   | el                                         ::      :: little {{ com -- little endian }}
   | be                                         ::      :: big    {{ com -- big endian }}

 cast :: cast_ ::=
   | low                                        ::      :: low {{ com -- extract lower bits }}
   | high                                       ::      :: high {{ com -- extract high bits}}
   | signed                                     ::      :: signed
   {{ com -- extend with sign bit}}
   | unsigned                                   ::      :: unsigned
   {{ com -- extend with zero}}

 widen_cast :: wcast_ ::=
   | signed                                     ::      :: signed
   | unsigned                                   ::      :: unsigned

 narrow_cast :: ncast_ ::=
   | low                                        ::      :: low
   | high                                       ::      :: high

 type,t :: type_ ::=
   | imm < sz >                                 ::      :: imm
   {{ com -- immediate of size $sz$}}
   | mem < sz1 , sz2 >                          ::      :: mem
   {{ com -- memory with address size $sz_1$ and element size $sz_2$}}

 delta {{ tex \Delta}} :: delta_ ::=
   | []                                         ::      :: nil  {{ com -- empty }}
   | delta [ var <- val ]                       ::      :: cons {{ com -- extend }}

 gamma {{ tex \Gamma }}, G {{ tex \Gamma }} :: gamma_ ::=
   | []                                         ::      :: nil  {{ com -- empty }}
   | gamma , var                                ::      :: cons {{ com -- extend }}
   | [ var ]                                    :: S    :: singleton {{ com -- singleton list }}
   | ( G )                                      :: S    :: parens
   | dom( delta )                               :: M    :: dom_delta
   {{ tex \mathsf{dom}([[delta]])}}
   {{ com -- domain of a runtime binding context}}

formula :: formula_ ::=
 | judgement                ::   :: judgement
 | ( formula )              :: M :: paren {{ coq ([[formula]]) }}
 | v1 <> v2                 :: M :: exp_neq {{ coq ([[v1]] <> [[v2]]) }}
 | var1 <> var2             :: M :: exp_var {{ coq ([[var1]] <> [[var2]]) }}
 | w1 .<> w2                 :: M :: word_neq
 {{ tex [[w1]] <> [[w2]] }}
 | nat1 > nat2              :: M :: nat_gt {{ coq ([[nat1]] > [[nat2]])}}
 | nat1 = nat2              :: M :: nat_eq {{ coq ([[nat1]] = [[nat2]])}}
 | nat1 >= nat2             :: M :: nat_ge {{ coq ([[nat1]] >= [[nat2]])}}
 | nat1 % sz = 0            :: M :: nat_mod_z {{ coq (exists n_, [[nat1]] = n_ * [[sz]]) }}
 | t1 = t2       :: M :: type_eq
 {{ coq ([[t1]] = [[t2]]) }}
 | e1 :=def e2              :: M :: defines
     {{ tex [[e1]] \stackrel{\text{def} }{:=} [[e2]] }}
 | ( var , val ) isin delta   :: M :: in_env
 | var notin dom ( delta )   :: M :: notin_env
   {{ tex [[var]] [[notin]] \mathsf{dom}([[delta]]) }}
 |  var isin gamma   :: M :: in_ctx
 | id notin dom ( gamma )   :: M :: notin_ctx
   {{ tex [[id]] [[notin]] \mathsf{dom}([[gamma]]) }}

terminals :: terminals_ ::=
  | ->				::   ::	rarrow					{{ tex \rightarrow }}
  | |-				::   :: vdash					{{ tex \vdash }}
  | ~				::   :: lneg  					{{ tex \neg }}
  | <-				::   :: larrow					{{ tex \leftarrow }}
  | |->				::   :: mapsto					{{ tex \mapsto }}
  | lambda			::   :: lambda					{{ tex \lambda }}
  | ~>				::   :: leadsto					{{ tex \leadsto }}
  | ~>*				::   :: mleadsto					{{ tex \leadsto^{*} }}
  | <>              ::   :: neq                     {{ tex \neq }}
  | >>              ::   :: lsr                     {{ tex \gg}}
  | ~>>             ::   :: asr                     {{ tex \ggg}}
  | <<              ::   :: lsl                     {{ tex \ll}}
  | isin        :: :: in {{ tex \in }}
  | notin     :: :: notin {{ tex \notin }}

subrules
  val <:: exp
  widen_cast <:: cast
  narrow_cast <:: cast

funs
  Compute ::=
fun
  type ( v ) :: t :: compute_type {{ com a function that computes the type of a value }}
by
  type(v[num1:nat <- v' : sz]) === mem<nat,sz>
  type(num:nat) === imm<nat>
  type(unknown[str]:t) === t

defns typing_type :: '' ::=
 defn t is ok :: :: type_wf :: twf_ by

 sz > 0
 -------------- :: imm
 imm<sz> is ok

 nat > 0
 sz > 0
 -------------- :: mem
 mem<nat,sz> is ok

defns typing_gamma :: '' ::=
 defn G is ok :: :: typ_gamma :: tg_ by

 --------- :: nil
 [] is ok

 id notin dom(G)
 t is ok
 G is ok
 --------------- :: cons
 (G, id:t) is ok

defns typing_exp :: '' ::=
 defn G |- exp '::' type :: :: type_exp :: t_ by

 id:t isin G
 G is ok
 ----------------- :: var
 G |- id:t :: t

 sz > 0
 G is ok
 ----------------- :: int
 G |- num:sz :: imm<sz>


 sz > 0
 nat > 0
 G |- v :: mem<nat,sz>
 G |- v' :: imm<sz>
 ---------------------------------------------------------- :: mem
 G |- v[num1:nat <- v' : sz] :: mem<nat,sz>


 sz' % sz = 0
 sz' > 0
 G |- e1 :: mem<nat,sz>
 G |- e2 :: imm<nat>
 -------------------------- :: load
 G |- e1 [e2, ed] : sz' :: imm<sz'>


 sz' % sz = 0
 sz' > 0
 G |- e1 :: mem<nat,sz>
 G |- e2 :: imm<nat>
 G |- e3 :: imm<sz'>
 --------------------------------------------- :: store
 G |- e1 with [e2, ed]:sz' <- e3 :: mem<nat,sz>


 G |- e1 :: imm<sz>
 G |- e2 :: imm<sz>
 --------------------------------- :: aop
 G |- e1 aop e2 :: imm<sz>

 G |- e1 :: imm<sz>
 G |- e2 :: imm<sz>
 --------------------------------- :: lop
 G |- e1 lop e2 :: imm<1>

 G |- e1 :: imm<sz>
 ---------------------------------- :: uop
 G |- uop e1 :: imm<sz>

 sz > 0
 sz >= nat
 G |- e :: imm<nat>
 ------------------------------------- :: cast_widen
 G |- widen_cast:sz[e] :: imm<sz>

 sz > 0
 nat >= sz
 G |- e :: imm<nat>
 ------------------------------------- :: cast_narrow
 G |- narrow_cast:sz[e] :: imm<sz>

 G |- e1  :: t
 G, id:t |- e2  :: t'
 ------------------------ :: let
 G |- let id:t = e1 in e2 :: t'

 t is ok
 G is ok
 ------------------------- :: unknown
 G |- unknown[str]:t :: t


 G |- e1 :: imm<1>
 G |- e2 :: t
 G |- e3 :: t
 -------------------------- :: ite
 G |- ite e1 e2 e3 :: t

 G |- e :: imm<sz>
 sz1 >= sz2
 ---------------------------------- :: extract
 G |- extract:sz1:sz2[e] :: imm<sz1-sz2+1>


 G |- e1 :: imm<sz1>
 G |- e2 :: imm<sz2>
 ---------------------------------- :: concat
 G |- e1 @ e2 :: imm<sz1+sz2>

defns typing_stmt :: '' ::=

 defn G |- bil is ok :: :: type_seq :: t_ by

 G |- stmt is ok
 ------------------------------ :: seq_one
 G |- {stmt} is ok

 G |- s1 is ok
 G |- {s2; ..; sn} is ok
 ------------------------------ :: seq_rec
 G |- {s1; s2; ..; sn} is ok


 defn G |- stmt is ok :: :: type_stmt :: t_ by


 G |- var :: t
 G |- exp :: t
 --------------------------- :: move
 G |- var := exp is ok


 G |- exp :: imm<nat>
 --------------------------- :: jmp
 G |- jmp exp is ok

 G is ok
 --------------------------- :: cpuexn
 G |- cpuexn(num) is ok

 G is ok
 ---------------------------- :: special
 G |- special(str) is ok


 G |- e :: imm<1>
 G |- seq is ok
 ---------------------------- :: while
 G |- while (e) seq is ok


 G |- e :: imm<1>
 G |- seq is ok
 ---------------------------- :: ifthen
 G |- if (e) seq is ok


 G |- e :: imm<1>
 G |- seq1 is ok
 G |- seq2 is ok
 ---------------------------- :: if
 G |- if (e) seq1 else seq2 is ok



defns program :: '' ::=


 defn delta , w , var ~> delta' , w' , var' :: :: step :: '' by

 delta,w,var |-> {addr=w1; size=w2; code=bil}
 delta, w1.+w2 |- bil ~> delta',w3,{}
 ---------------------------------------------------------- :: step
 delta,w,var  ~> delta',w3,var


 defn delta,w,var |-> insn :: :: decode :: '' by

 -------------------------------------------------- :: decode
 delta,w,var |-> insn


defns helpers :: '' ::=
 defn succ w1 = exp :: :: succ :: '' by

 -------------------------------- :: succ
 succ num:sz = num:sz .+ 1:sz


defns reduce_exp :: '' ::=

 defn delta |- exp ~> exp' :: :: exp :: '' by

 (var,v) isin delta
------------------ :: var_in
 delta |- var ~> v


 id:type notin dom(delta)
 -------------------------------------------- :: var_unknown
 delta |- id:type ~> unknown[str]:type

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% LOAD                                              %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

 delta |- e2 ~> e2'
 ------------------------------------- :: load_step_addr
 delta |- e1[e2,ed]:sz ~> e1[e2',ed]:sz


 delta |- e1 ~> e1'
 ------------------------------------- :: load_step_mem
 delta |- e1[v2,ed]:sz ~> e1'[v2,ed]:sz

 ------------------------------------------------------ :: load_byte
 delta |- v[w <- v':sz][w,ed']:sz ~> v'

 w1 <> w2
 ----------------------------------------------------------- :: load_byte_from_next
 delta |- v[w1 <- v':sz][w2,ed]:sz ~> v[w2,ed]:sz

 ---------------------------------------------------------- :: load_un_mem
 delta |- (unknown[str]:t)[v,ed]:sz ~> unknown[str]:imm<sz>

 ------------------------------------------------------------------------- :: load_un_addr
 delta |- (v[w1 <- v':sz])[unknown[str]:t,ed]:sz' ~> unknown[str]:imm<sz'>

 sz' > sz
 succ w = w'
 type(v) = mem<nat,sz>
 ------------------------------------------------------------- :: load_word_be
 delta |- v[w,be]:sz' ~> v[w,be]:sz @ (v[w', be]:(sz'-sz))

 sz' > sz
 succ w = w'
 type(v) = mem<nat,sz>
 -------------------------------------------------------- :: load_word_el
 delta |- v[w,el]:sz' ~> v[w',el]:(sz'-sz) @ (v[w,be]:sz)


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% STORE                                             %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


 delta |- e3 ~> e3'
 ------------------------------------------------------------------------- :: store_step_val
 delta |- e1 with [e2,ed]:sz <- e3 ~> e1 with [e2,ed] : sz <- e3'


 delta |- e2 ~> e2'
 ------------------------------------------------------------------------- :: store_step_addr
 delta |- e1 with [e2,ed]:sz <- v3 ~> e1 with [e2',ed] : sz <- v3


 delta |- e1 ~> e1'
 ------------------------------------------------------------------------- :: store_step_mem
 delta |- e1 with [v2,ed]:sz <- v3 ~> e1' with [v2,ed] : sz <- v3

 sz' > sz
 succ w = w'
 type(v) = mem<nat,sz>
 e1 :=def (v with [w,be]:sz <- high:sz[val])
 ---------------------------------------------------------------------------------- :: store_word_be
 delta |- v with [w,be]:sz' <- val ~> e1 with [w',be]:(sz'-sz) <- low:(sz'-sz)[val]

 sz' > sz
 succ w = w'
 type(v) = mem<nat,sz>
 e1 :=def (v with [w,el]:sz <- low:sz[val])
 -------------------------------------------------------------------------------- :: store_word_el
 delta |- v with [w,el]:sz' <- val ~> e1 with [w',el]:(sz'-sz) <- high:(sz'-sz)[val]

 type(v) = mem<nat,sz>
 --------------------------------------------------------- :: store_val
 delta |- v with [w,ed] : sz <- v' ~> v[w <- v' : sz]

 type(v) = t
 ----------------------------------------------------------------------- :: store_un_addr
 delta |- v with [unknown[str]:t',ed] : sz' <- v2 ~> unknown[str]:t

 delta |- e1 ~> e1'
 ------------------------------------------------ :: let_step
 delta |- let var = e1 in e2 ~> let var = e1' in e2


 ------------------------------------------------- :: let
 delta |- let var = v in e ~> [v/var]e


 delta |- e1 ~> e1'
 ------------------------------------------------------------------ :: ite_step_cond
 delta |- ite e1 v2 v3 ~> ite e1' v2 v3

 delta |- e2 ~> e2'
 ------------------------------------------------------------------ :: ite_step_then
 delta |- ite e1 e2 v3 ~> ite e1 e2' v3

 delta |- e3 ~> e3'
 ------------------------------------------------------------------ :: ite_step_else
 delta |- ite e1 e2 e3 ~> ite e1 e2 e3'

 ----------------------------------------------- :: ite_true
 delta |- ite true v2 v3 ~> v2


 ------------------------------------------------ :: ite_false
 delta |- ite false v2 v3 ~> v3

 type(v2) = t'
 ------------------------------------------------------------------ :: ite_unk
 delta |- ite unknown[str]:t v2 v3 ~> unknown[str]:t'

 delta |- e2 ~> e2'
 ------------------------------------------ :: bop_rhs
 delta |- v1 bop e2 ~> v1 bop e2'

 delta |- e1 ~> e1'
 ----------------------------------------- :: bop_lhs
 delta |- e1 bop e2 ~> e1' bop e2

 -------------------------------------------------------- :: aop_unk_rhs
 delta |- e aop unknown[str]:t ~> unknown[str]:t

 -------------------------------------------------------- :: aop_unk_lhs
 delta |- unknown[str]:t aop e ~> unknown[str]:t

 -------------------------------------------------------- :: lop_unk_rhs
 delta |- e lop unknown[str]:t ~> unknown[str]:imm<1>

 -------------------------------------------------------- :: lop_unk_lhs
 delta |- unknown[str]:t lop e ~> unknown[str]:imm<1>

 -------------------------------------- :: plus
 delta |- w1 + w2 ~> w1 .+ w2

 -------------------------------------- :: minus
 delta |- w1 - w2 ~> w1 .- w2


 ------------------------------------- :: times
 delta |- w1 * w2 ~> w1 .* w2


 ------------------------------------- :: div
 delta |- w1 / w2 ~> w1 ./ w2


 --------------------------------------- :: sdiv
 delta |- w1 /$ w2 ~> w1 ./$ w2


 ------------------------------------- :: mod
 delta |- w1 % w2 ~> w1 .% w2


 ---------------------------------------- :: smod
 delta |- w1 %$ w2 ~> w1 .%$ w2


 ----------------------------------------------- :: lsl
 delta |- w1 << w2 ~> w1 .<< w2

 ----------------------------------------------- :: lsr
 delta |- w1 >> w2 ~> w1 .>> w2

 ----------------------------------------------- :: asr
 delta |- w1 ~>> w2 ~> w1 .~>> w2


 ----------------------------------------------- :: land
 delta |- w1 & w2 ~> w1 .& w2

 ----------------------------------------------- :: lor
 delta |- w1 | w2 ~> w1 .| w2

 ----------------------------------------------- :: xor
 delta |- w1 xor w2 ~> w1 .xor w2

 ----------------------------------------------- :: eq_same
 delta |- w = w ~> true

 w1 .<> w2
 ----------------------------------------------- :: eq_diff
 delta |- w1 = w2 ~> false


 ----------------------------------------------- :: neq_same
 delta |- w <> w ~> false

 w1 .<> w2
 ----------------------------------------------- :: neq_diff
 delta |- w1 <> w2 ~> true

 ----------------------------------------------- :: less
 delta |- w1 < w2 ~> w1 .< w2



 ----------------------------------------------- :: less_eq
 delta |- w1 <= w2 ~> (w1 < w2) | (w1 = w2)



 ----------------------------------------------- :: signed_less
 delta |- w1 <$ w2 ~> w1 .<$ w2


 ----------------------------------------------------- :: signed_less_eq
 delta |- w1 <=$ w2 ~> (w1 = w2) & (w1 <$ w2)

 delta |- e ~> e'
 ---------------------------------------- :: uop
 delta |- uop e ~> uop e'

 ------------------------------------------------ :: uop_unk
 delta |- uop unknown[str] : t ~> unknown[str] : t

 ---------------------------------------- :: not
 delta |- ~ w ~> .~ w

 ---------------------------------------- :: neg
 delta |- - w ~> .- w

 delta |- e2 ~> e2'
 ---------------------------------------- :: concat_rhs
 delta |- e1 @ e2 ~> e1 @ e2'


 delta |- e1 ~> e1'
 ---------------------------------------- :: concat_lhs
 delta |- e1 @ v2 ~> e1' @ v2

 type(v2) = imm<sz2>
 ----------------------------------------------------------------- :: concat_lhs_un
 delta |- unknown[str]:imm<sz1> @ v2 ~> unknown[str]:imm<sz1 +sz2>

 type(v1) = imm<sz1>
 ---------------------------------------------------------------- :: concat_rhs_un
 delta |- v1 @ unknown[str]:imm<sz2> ~> unknown[str]:imm<sz1 +sz2>

 ---------------------------------------- :: concat
 delta |- w1 @ w2 ~> w1 .@ w2

 delta |- e ~> e'
 ------------------------------------------------- :: extract_reduce
 delta |- extract:sz1:sz2[e] ~> extract:sz1:sz2[e']


 ------------------------------------------------------------------------------ :: extract_un
 delta |- extract:sz1:sz2[unknown[str]:t] ~> unknown[str]:imm<(sz1 - sz2) + 1>

 ------------------------------------------------------ :: extract
 delta |- extract:sz1:sz2[w] ~> ext w ~hi:sz1 ~lo:sz2

 delta |- e ~> e'
 --------------------------------- :: cast_reduce
 delta |- cast:sz[e] ~> cast:sz[e']

 ------------------------------------------------------------ :: cast_unk
 delta |- cast:sz[unknown[str] : t] ~> unknown[str] : imm<sz>

 -------------------------------------------- :: cast_low
 delta |- low:sz[w] ~> ext w ~hi:(sz-1) ~lo:0


 ----------------------------------------------------------- :: cast_high
 delta |- high:sz[num:sz'] ~> ext num:sz' ~hi:(sz'-1) ~lo:(sz'-sz)


 -------------------------------------------- :: cast_signed
 delta |- signed:sz[w] ~> exts w ~hi:(sz-1) ~lo:0

 -------------------------------------------------- :: cast_unsigned
 delta |- unsigned:sz[w] ~> ext w ~hi:(sz-1) ~lo:0


defns reduce_stmt :: '' ::=

 defn delta , word |- stmt ~> delta' , word' :: :: stmt :: '' by


 delta |- e ~>* v
 ----------------------------------------- :: move
 delta,w |- var := e ~> delta[var <- v], w


 delta |- e ~>* w'
 ---------------------------------- :: jmp
 delta,w |- jmp e ~> delta, w'


 ------------------------------------ :: cpuexn
 delta,w |- cpuexn(num) ~> delta,w


 ------------------------------------ :: special
 delta,w |- special(str) ~> delta,w


 delta |- e ~>* true
 delta,word |- seq ~> delta',word',{}
 ------------------------------------- :: ifthen_true
 delta,word |- if (e) seq ~> delta', word'

 delta |- e ~>* true
 delta,word |- seq ~> delta',word',{}
 ------------------------------------- :: if_true
 delta,word |- if (e) seq else seq1 ~> delta', word'

 delta |- e ~>* false
 delta,word |- seq ~> delta',word',{}
 ------------------------------------- :: if_false
 delta,word |- if (e) seq1 else seq ~> delta', word'


 delta1 |- e ~>* true
 delta1,word1 |- seq ~> delta2,word2,{}
 delta2,word2 |- while (e) seq ~> delta3,word3
 --------------------------------------------- :: while
 delta1,word1 |- while (e) seq ~> delta3,word3

 delta |- e ~>* false
 ----------------------------------------- :: while_false
 delta,word |- while (e) seq ~> delta,word



 defn delta , word |- seq ~> delta' , word' , seq' :: :: seq :: '' by

 delta,word |- s1 ~> delta',word'
 ------------------------------------------------------------- :: seq_rec
 delta,word |- {s1; s2; ..; sn} ~> delta', word', {s2; ..; sn}

 delta,word |- s1 ~> delta',word'
 ------------------------------------------------------------- :: seq_last
 delta,word |- {s1; s2} ~> delta', word', {s2}

 delta,word |- s1 ~> delta',word'
 ------------------------------------------------------------- :: seq_one
 delta,word |- {s1} ~> delta', word', {}


 ------------------------------------------------------------- :: seq_nil
 delta,word |- {} ~> delta, word, {}
 
defns multistep_exp :: '' ::=

 defn delta |- exp ~>* exp' :: :: mexp :: '' by

 ---------------- :: refl
 delta |- e ~>*  e

 delta |- e1 ~> e2
 delta |- e2 ~>* e3
 ------------------ :: reduce
 delta |- e1 ~>* e3