Verified Commit 6fb24ca1 authored by Julien's avatar Julien
Browse files

WIP! [OTT|Semantics] Adding protocol dependent operations

parent cb7e6689
Pipeline #155006545 failed with stage
in 10 minutes and 14 seconds
......@@ -33,7 +33,7 @@ Definition slice (nv1:num_val) (nv2:num_val) (s:string) := s. (* TODO *)
Definition pack (_:value) : string_val := EmptyString. (* TODO *)
Definition unpack (s:string_val) : value := (val_rval (rval_record nil)). (* TODO *)
(* Domain specific operations *)
Definition get_contract (a:add_val) : add_val := a. (* TODO *)
Definition get_address (a:add_val) : add_val := a. (* TODO *)
Definition get_implicit_account (a:add_val) : add_val := a. (* TODO *)
(* (* Domain specific operations *) *)
(* Definition get_contract (P:proto_env) (a:add_val) : add_val := a. (* TODO *) *)
(* Definition get_address (P:proto_env) (a:add_val) : add_val := a. (* TODO *) *)
(* Definition get_implicit_account (P:proto_env) (a:add_val) : add_val := a. (* TODO *) *)
......@@ -26,6 +26,7 @@ Fixpoint string_of_type (t:ty) : string :=
| ty_contract ty => "(contract "++(string_of_type ty)++")"
| ty_key => "key"
| ty_signature => "signature"
| ty_chain_id => "chain_id"
end
with string_of_rty (rt:rty) : string :=
match rt with
......@@ -188,11 +189,12 @@ Fixpoint string_of_rhs (r:rhs) : string :=
| rhs_amount => "amount"
| rhs_balance => "balance"
| rhs_self => "self"
| rhs_transfer_tokens x y z => "transfer_tokens " ++ x ++ " " ++ y ++ " " ++ z
| rhs_set_delegate x => "set_delegate " ++ x
| rhs_transfer_tokens x y z => "transfer_tokens " ++ string_of_arg x ++ " " ++ string_of_arg y ++ " " ++ string_of_arg z
| rhs_set_delegate x => "set_delegate " ++ string_of_arg x
| rhs_sender => "sender"
| rhs_source => "source"
| rhs_now => "now"
| rhs_chain_id => "chain_id"
end.
Fixpoint string_of_instruction (i:instruction) : string :=
......
......@@ -213,6 +213,7 @@ Section ty_ind.
P ty -> P (ty_contract ty).
Hypothesis Hkey : P ty_key.
Hypothesis Hsig : P ty_signature.
Hypothesis Hchain_id: P ty_chain_id.
Fixpoint ty_ind (t : ty) : (P t) :=
match t as t0 return (P t0) with
......@@ -253,6 +254,7 @@ Section ty_ind.
| ty_contract ty => Hcontract ty (ty_ind ty)
| ty_key => Hkey
| ty_signature => Hsig
| ty_chain_id => Hchain_id
end.
End ty_ind.
......@@ -299,7 +301,8 @@ Inductive type_without_var : ty -> Prop :=
type_without_var ty ->
type_without_var (ty_contract ty)
| key_without_var : type_without_var ty_key
| sig_without_var : type_without_var ty_signature.
| sig_without_var : type_without_var ty_signature
| chain_id_without_var : type_without_var ty_chain_id.
Open Scope string_scope.
......@@ -562,7 +565,7 @@ Fixpoint remove_tvar_from_rhs (r:rhs) (env:g) : M rhs :=
| rhs_map_update var l1 l2 => Return _ (rhs_map_update var l1 l2)
| rhs_amount| rhs_balance | rhs_check_signature _ _ _
| rhs_self | rhs_transfer_tokens _ _ _ | rhs_set_delegate _
| rhs_sender | rhs_source | rhs_now => Return _ r
| rhs_sender | rhs_source | rhs_now| rhs_chain_id => Return _ r
end.
Fixpoint remove_tvar_from_ins (ins:instruction) (env:g) : M instruction :=
......@@ -697,7 +700,7 @@ Fixpoint sort_fields_in_rhs (r:rhs) : rhs :=
| rhs_map_get _ _ | rhs_map_update _ _ _ => r
| rhs_amount | rhs_balance | rhs_check_signature _ _ _
| rhs_self | rhs_transfer_tokens _ _ _ | rhs_set_delegate _
| rhs_sender | rhs_source | rhs_now => r
| rhs_sender | rhs_source | rhs_now | rhs_chain_id => r
end.
Definition sort_fields_in_lhs (l:lhs) : lhs :=
......
......@@ -251,50 +251,50 @@ defns
Jeval :: 'eval_' ::=
defn
E |- rhs / val -> val' :: :: rhs :: rhs_ {{ Right-hand side evaluation}} by
P,E |- rhs / val -> val' :: :: rhs :: rhs_ {{ Right-hand side evaluation}} by
-------------------------------------------------------------- :: add
E |- x_1 + x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 + nv_2
P,E |- x_1 + x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 + nv_2
-------------------------------------------------------------- :: sub
E |- x_1 - x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 - nv_2
P,E |- x_1 - x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 - nv_2
-------------------------------------------------------------- :: mul
E |- x_1 * x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 * nv_2
P,E |- x_1 * x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 * nv_2
--------------------------------------------------------------------------------------------------------- :: ediv
E |- x_1 /mod x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> { quotient = nv_1 / nv_2 ; remainder = nv_1 % nv_2 }
P,E |- x_1 /mod x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> { quotient = nv_1 / nv_2 ; remainder = nv_1 % nv_2 }
-------------------------------------- :: not_nat
E |- ~ x_1 / { x_1 = nv_1 } -> ~ nv_1
P,E |- ~ x_1 / { x_1 = nv_1 } -> ~ nv_1
-------------------------------------------------------------- :: and_int_nat
E |- x_1 && x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 && nv_2
P,E |- x_1 && x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 && nv_2
-------------------------------------------------------------- :: or_nat_nat
E |- x_1 || x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 || nv_2
P,E |- x_1 || x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 || nv_2
-------------------------------------------------------------- :: xor_nat_nat
E |- x_1 ^ x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 ^ nv_2
P,E |- x_1 ^ x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 ^ nv_2
nv_2 <= 256
-------------------------------------------------------------- :: lsl_ok
E |- x_1 << x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 << nv_2
P,E |- x_1 << x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 << nv_2
nv_2 <= 256
-------------------------------------------------------------- :: lsr_ok
E |- x_1 >> x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 >> nv_2
P,E |- x_1 >> x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> nv_1 >> nv_2
-------------------------------------------------- :: abs
E |- abs x_1 / { x_1 = nv_1 } -> abs nv_1
P,E |- abs x_1 / { x_1 = nv_1 } -> abs nv_1
nv_1 >= 0
------------------------------------------------------------------------------ :: is_nat_some
E |- is_nat x_1 / { x_1 = nv_1 } -> (Some nv_1 : [ None : unit | Some : nat ])
P,E |- is_nat x_1 / { x_1 = nv_1 } -> (Some nv_1 : [ None : unit | Some : nat ])
nv_1 < 0
------------------------------------------------------------------------------ :: is_nat_none
E |- is_nat x_1 / { x_1 = nv_1 } -> (None {} : [ None : unit | Some : nat ])
P,E |- is_nat x_1 / { x_1 = nv_1 } -> (None {} : [ None : unit | Some : nat ])
-------------------------------------------------- :: int
E |- int x_1 / { x_1 = nv_1 } -> nv_1
P,E |- int x_1 / { x_1 = nv_1 } -> nv_1
......@@ -61,9 +61,17 @@ value, val :: 'val_' ::= {{com Value}}
g :: 'g_' ::= {{tex \Gamma}} {{com Typing context (for inlined definitions)}}
| . :: :: empty
p_dummy :: '_' ::= {{coq unit. Load Proto}}
P :: 'P_' ::= {{tex \Sigma}} {{com Execution context }} {{coq proto_env}} {{ phantom }}
E :: 'E_' ::= {{tex \Sigma}} {{com Semantic context (for global definitions)}}
| . :: :: empty
products :: 'products_' ::= {{com Products of types}}
| { ty_1 * ty'_1 ; .. ; ty_n * ty'_n } :: :: prod
formula :: 'formula_' ::=
| judgement :: :: judgement
| formula_1 .. formula_n :: :: dots
......@@ -296,47 +304,47 @@ defns
E |- { l_1 = x_1 ; .. ; l_n = x_n } /a { x_1 = val_1 ; .. ; x_n = val_n } -> { l_1 = val_1 ; .. ; l_n = val_n }
defn
E |- f / val -> val' :: :: f :: f_ {{com Function symbol evaluation}} by
P,E |- f / val -> val' :: :: f :: f_ {{com Function symbol evaluation}} by
defn
E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
P,E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
E |- arg /a val -> val'
---------------------------------------- :: arg
E |- arg / val -> val'
P,E |- arg / val -> val'
E |- arg /a val -> val'
E |- f / val' -> val''
P,E |- f / val' -> val''
---------------------------------- :: f
E |- f arg / val -> val''
P,E |- f arg / val -> val''
{ l = val } @ rval = rval'
----------------------------------------- :: projection
E |- var.l / rval' -> val
P,E |- var.l / rval' -> val
{ l_1 = val'_1 ; .. ; l_n = val'_n } @ rval = rval'
{ l_1 = val_1 ; .. ; l_n = val_n } @ rval = rval''
----------------------------------------------------------------------------------------------------------------- :: update
E |- { var with l_1 = var_1 ; .. ; l_n = var_n } / { var = rval' ; var_1 = val_1 ; .. ; var_n = val_n } -> rval''
P,E |- { var with l_1 = var_1 ; .. ; l_n = var_n } / { var = rval' ; var_1 = val_1 ; .. ; var_n = val_n } -> rval''
defn
E |- instruction / val -> val' :: :: instr :: instr_ {{com Instruction evaluation}} by
P,E |- instruction / val -> val' :: :: instr :: instr_ {{com Instruction evaluation}} by
E |- instruction / rval -> rval'
P,E |- instruction / rval -> rval'
rval @ rval'' = rval1
rval' @ rval'' = rval2
---------------------------------------------- :: frame
E |- instruction / rval1 -> rval2
P,E |- instruction / rval1 -> rval2
--------------------- :: noop
E |- noop / :val_rval: {} -> :val_rval: {}
P,E |- noop / :val_rval: {} -> :val_rval: {}
E |- I_1 / val -> val'
E |- I_2 / val' -> val''
P,E |- I_1 / val -> val'
P,E |- I_2 / val' -> val''
------------------------- :: seq
E |- I_1 ; I_2 / val -> val''
P,E |- I_1 ; I_2 / val -> val''
E |- rhs / val -> val'
P,E |- rhs / val -> val'
E |- lhs / val' -> val''
------------------------------------------------------ :: assign
E |- lhs = rhs / val -> val''
P,E |- lhs = rhs / val -> val''
......@@ -83,29 +83,29 @@ defns
Jeval :: 'eval_' ::=
defn
E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
P,E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
---------------------------------------------------------- :: not
E |- ~ x_1 / { x_1 = bool_val_1 } -> ~ bool_val_1
P,E |- ~ x_1 / { x_1 = bool_val_1 } -> ~ bool_val_1
-------------------------------------------------------------------------------------- :: and
E |- x_1 && x_2 / { x_1 = bool_val_1 ; x_2 = bool_val_2 } -> bool_val_1 && bool_val_2
P,E |- x_1 && x_2 / { x_1 = bool_val_1 ; x_2 = bool_val_2 } -> bool_val_1 && bool_val_2
-------------------------------------------------------------------------------------- :: or
E |- x_1 || x_2 / { x_1 = bool_val_1 ; x_2 = bool_val_2 } -> bool_val_1 || bool_val_2
P,E |- x_1 || x_2 / { x_1 = bool_val_1 ; x_2 = bool_val_2 } -> bool_val_1 || bool_val_2
----------------------------------------------------------------------------------- :: xor
E |- x_1 ^ x_2 / { x_1 = bool_val_1 ; x_2 = bool_val_2 } -> bool_val_1 ^ bool_val_2
P,E |- x_1 ^ x_2 / { x_1 = bool_val_1 ; x_2 = bool_val_2 } -> bool_val_1 ^ bool_val_2
defn
E |- instruction / val -> val' :: :: instr :: instr_ {{com Instruction evaluation}} by
P,E |- instruction / val -> val' :: :: instr :: instr_ {{com Instruction evaluation}} by
{ var' = (False :val_rval: {} : vty) } @ rval = rval'
--------------------------------------------------------- :: loop_end
E |- loop var do I done / rval' -> rval
P,E |- loop var do I done / rval' -> rval
{ var' = (True :val_rval: {} : vty) } @ rval = rval'
E |- I / rval -> rval1
E |- loop var do I done / rval1 -> rval2
P,E |- I / rval -> rval1
P,E |- loop var do I done / rval1 -> rval2
--------------------------------------------------------- :: loop_continue
E |- loop var do I done / rval' -> rval2
P,E |- loop var do I done / rval' -> rval2
......@@ -68,34 +68,34 @@ defns
Jeval :: 'eval_' ::=
defn
E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
P,E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
---------------------------------------------------------------- :: bytes_pack
E |- pack x / { x = val } -> pack val
P,E |- pack x / { x = val } -> pack val
g |- unpack bval : ty
----------------------------------------------------------- :: bytes_unpack_succ
E |- unpack ty x / { x = bval } -> (Some (unpack bval) : [ None : unit | Some : ty ])
P,E |- unpack ty x / { x = bval } -> (Some (unpack bval) : [ None : unit | Some : ty ])
~ (g |- unpack bval : ty)
----------------------------------------------------------- :: bytes_unpack_fail
E |- unpack ty x / { x = bval } -> (None {} : [ None : unit | Some : ty ])
P,E |- unpack ty x / { x = bval } -> (None {} : [ None : unit | Some : ty ])
------------------------------------------------------------------------------------ :: bytes_concat
E |- concat x_1 x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> bval_1 ++ bval_2
P,E |- concat x_1 x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> bval_1 ++ bval_2
---------------------------------------- :: bytes_size
E |- size x / { x = bval } -> size bval
P,E |- size x / { x = bval } -> size bval
nv_1 <= nv_2
nv_2 <= size bval
--------------------------------------------------------------------------------------------- :: bytes_slice_inbounds
E |- slice x x_1 x_2 / { x = bval ; x_1 = nv_1 ; x_2 = nv_2 } -> (Some (slice bval nv_1 nv_2) : [ None : unit | Some : bytes ])
P,E |- slice x x_1 x_2 / { x = bval ; x_1 = nv_1 ; x_2 = nv_2 } -> (Some (slice bval nv_1 nv_2) : [ None : unit | Some : bytes ])
nv_1 > nv_2
------------------------------------------------------------------------------------- :: bytes_slice_outofbounds1
E |- slice x x_1 x_2 / { x = bval ; x_1 = nv_1 ; x_2 = nv_2 } -> (None {} : [ None : unit | Some : bytes ])
P,E |- slice x x_1 x_2 / { x = bval ; x_1 = nv_1 ; x_2 = nv_2 } -> (None {} : [ None : unit | Some : bytes ])
nv_2 + nv_2 > size bval
------------------------------------------------------------------------------------- :: bytes_slice_outofbounds2
E |- slice x x_1 x_2 / { x = bval ; x_1 = nv_1 ; x_2 = nv_2 } -> (None {} : [ None : unit | Some : bytes ])
P,E |- slice x x_1 x_2 / { x = bval ; x_1 = nv_1 ; x_2 = nv_2 } -> (None {} : [ None : unit | Some : bytes ])
......@@ -193,128 +193,128 @@ defns
nv_1 == nv_2
------------------------------------------------------------------------- :: eq_num
E |- x_1 == x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
P,E |- x_1 == x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
nv_1 != nv_2
------------------------------------------------------------------------- :: eq_num_not
E |- x_1 == x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
P,E |- x_1 == x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
sval_1 == sval_2
--------------------------------------------------------------------- :: eq_str
E |- x_1 == x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
P,E |- x_1 == x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
sval_1 != sval_2
--------------------------------------------------------------------- :: eq_str_not
E |- x_1 == x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
P,E |- x_1 == x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
bval_1 == bval_2
--------------------------------------------------------------------- :: eq_bytes
E |- x_1 == x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
P,E |- x_1 == x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
bval_1 != bval_2
--------------------------------------------------------------------- :: eq_bytes_not
E |- x_1 == x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
P,E |- x_1 == x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
nv_1 != nv_2
------------------------------------------------------------------------- :: neq_num
E |- x_1 != x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
P,E |- x_1 != x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
nv_1 == nv_2
------------------------------------------------------------------------- :: neq_num_not
E |- x_1 != x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
P,E |- x_1 != x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
nv_1 < nv_2
--------------------------------------------------------------------- :: inf_num
E |- x_1 < x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
P,E |- x_1 < x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
nv_1 >= nv_2
--------------------------------------------------------------------- :: inf_num_not
E |- x_1 < x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
P,E |- x_1 < x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
sval_1 < sval_2
--------------------------------------------------------------------- :: inf_str
E |- x_1 < x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
P,E |- x_1 < x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
sval_1 >= sval_2
--------------------------------------------------------------------- :: inf_str_not
E |- x_1 < x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
P,E |- x_1 < x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
bval_1 < bval_2
--------------------------------------------------------------------- :: inf_bytes
E |- x_1 < x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
P,E |- x_1 < x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
bval_1 >= bval_2
--------------------------------------------------------------------- :: inf_bytes_not
E |- x_1 < x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
P,E |- x_1 < x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
nv_1 <= nv_2
--------------------------------------------------------------------- :: infeq_num
E |- x_1 <= x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
P,E |- x_1 <= x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
nv_1 > nv_2
--------------------------------------------------------------------- :: infeq_num_not
E |- x_1 <= x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
P,E |- x_1 <= x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
sval_1 <= sval_2
--------------------------------------------------------------------- :: infeq_str
E |- x_1 <= x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
P,E |- x_1 <= x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
sval_1 > sval_2
--------------------------------------------------------------------- :: infeq_str_not
E |- x_1 <= x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
P,E |- x_1 <= x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
bval_1 <= bval_2
--------------------------------------------------------------------- :: infeq_bytes
E |- x_1 <= x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
P,E |- x_1 <= x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
bval_1 > bval_2
--------------------------------------------------------------------- :: infeq_bytes_not
E |- x_1 <= x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
P,E |- x_1 <= x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
nv_1 > nv_2
--------------------------------------------------------------------- :: sup_num
E |- x_1 > x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
P,E |- x_1 > x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
nv_1 <= nv_2
--------------------------------------------------------------------- :: sup_num_not
E |- x_1 > x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
P,E |- x_1 > x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
sval_1 > sval_2
--------------------------------------------------------------------- :: sup_str
E |- x_1 > x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
P,E |- x_1 > x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
sval_1 <= sval_2
--------------------------------------------------------------------- :: sup_str_not
E |- x_1 > x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
P,E |- x_1 > x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
bval_1 > bval_2
--------------------------------------------------------------------- :: sup_bytes
E |- x_1 > x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
P,E |- x_1 > x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
bval_1 <= bval_2
--------------------------------------------------------------------- :: sup_bytes_not
E |- x_1 > x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
P,E |- x_1 > x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
nv_1 >= nv_2
--------------------------------------------------------------------- :: supeq_num
E |- x_1 >= x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
P,E |- x_1 >= x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> true
nv_1 < nv_2
--------------------------------------------------------------------- :: supeq_num_not
E |- x_1 >= x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
P,E |- x_1 >= x_2 / { x_1 = nv_1 ; x_2 = nv_2 } -> false
sval_1 >= sval_2
--------------------------------------------------------------------- :: supeq_str
E |- x_1 >= x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
P,E |- x_1 >= x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> true
sval_1 < sval_2
--------------------------------------------------------------------- :: supeq_str_not
E |- x_1 >= x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
P,E |- x_1 >= x_2 / { x_1 = sval_1 ; x_2 = sval_2 } -> false
bval_1 >= bval_2
--------------------------------------------------------------------- :: supeq_bytes
E |- x_1 >= x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
P,E |- x_1 >= x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> true
bval_1 < bval_2
--------------------------------------------------------------------- :: supeq_bytes_not
E |- x_1 >= x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
P,E |- x_1 >= x_2 / { x_1 = bval_1 ; x_2 = bval_2 } -> false
......@@ -18,7 +18,7 @@ defns
Jeval :: 'eval_' ::=
defn
E |- instruction / val -> val' :: :: instr :: instr_ {{com Instruction evaluation}} by
P,E |- instruction / val -> val' :: :: instr :: instr_ {{com Instruction evaluation}} by
------------------------------------------------ :: drop
E |- drop var / { var = val } -> :val_rval: {}
P,E |- drop var / { var = val } -> :val_rval: {}
......@@ -17,7 +17,7 @@ defns
Jeval :: 'eval_' ::=
defn
E |- f / val -> val' :: :: f :: f_ {{com Function symbol evaluation}} by
P,E |- f / val -> val' :: :: f :: f_ {{com Function symbol evaluation}} by
-------------------------------------------- :: dup
E |- dup / val -> { car = val; cdr = val }
P,E |- dup / val -> { car = val; cdr = val }
......@@ -95,57 +95,57 @@ defns
Jeval :: 'eval_' ::=
defn
E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
P,E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
----------------------------------------------------------------------------------------------------------- :: list
E |- [ var_1 ; .. ; var_n ] / { var_1 = val_1 ; .. ; var_n = val_n } -> ([ val_1 ; .. ; val_n ] : list ty)
P,E |- [ var_1 ; .. ; var_n ] / { var_1 = val_1 ; .. ; var_n = val_n } -> ([ val_1 ; .. ; val_n ] : list ty)
-------------------------------------------------------------------- :: list_cons
E |- x_1 :: x_2 / { x_1 = val_1 ; x_2 = lval_2 } -> val_1 :: lval_2
P,E |- x_1 :: x_2 / { x_1 = val_1 ; x_2 = lval_2 } -> val_1 :: lval_2
------------------------------------------ :: list_size
E |- size x / { x = lval } -> size lval
P,E |- size x / { x = lval } -> size lval
{ var = ([] : list ty) } @ rval = rval'
E |- rhs_1 / rval -> val
P,E |- rhs_1 / rval -> val
------------------------------------------------------------------------------------------- :: list_match_nil
E |- match var with [] -> rhs_1 | var_1 :: var_2 -> rhs_2 end / rval' -> val
P,E |- match var with [] -> rhs_1 | var_1 :: var_2 -> rhs_2 end / rval' -> val
{ var = val_1 :: tl } @ rval = rval'
{ var_1 = val1 ; var_2 = tl } @ rval = rval''
E |- rhs_2 / rval'' -> val
P,E |- rhs_2 / rval'' -> val
--------------------------------------------------------------------------------------------------- :: list_match_cons
E |- match var with [] -> rhs_1 | var_1 :: var_2 -> rhs_2 end / rval' -> val
P,E |- match var with [] -> rhs_1 | var_1 :: var_2 -> rhs_2 end / rval' -> val
------------------------------------------------------------------------------------------- :: list_map_nil
E |- map var in var' do rhs done / { var' = ([] : list ty) } -> ([] : list ty)
P,E |- map var in var' do rhs done / { var' = ([] : list ty) } -> ([] : list ty)
E |- rhs / { var = val } -> val'
E |- map var in var' do rhs done / { var' = tl } -> tl'
P,E |- rhs / { var = val } -> val'
P,E |- map var in var' do rhs done / { var' = tl } -> tl'
------------------------------------------------------------------------- :: list_map_cons
E |- map var in var' do rhs done / { var' = val :: tl } -> val' :: tl'
P,E |- map var in var' do rhs done / { var' = val :: tl } -> val' :: tl'
defn
E |- instruction / val -> val' :: :: instr :: instr_ {{com Instruction evaluation}} by
P,E |- instruction / val -> val' :: :: instr :: instr_ {{com Instruction evaluation}} by
{ var = ([] : list ty) } @ rval = rval'
E |- instruction_1 / rval -> val
P,E |- instruction_1 / rval -> val
------------------------------------------------------------------------------------------- :: list_match_nil
E |- match var with [] -> instruction_1 | var_1 :: var_2 -> I_2 end / rval' -> val
P,E |- match var with [] -> instruction_1 | var_1 :: var_2 -> I_2 end / rval' -> val
{ var_1 = val_1 :: tl } @ rval = rval'
{ var_1 = val_1 ; var_2 = tl } @ rval = rval''
E |- instruction_2 / rval'' -> val
P,E |- instruction_2 / rval'' -> val
----------------------------------------------------------------------------------------------- :: list_match_cons
E |- match var with [] -> instruction_1 | var_1 :: var_2 -> instruction_2 end / rval' -> val
P,E |- match var with [] -> instruction_1 | var_1 :: var_2 -> instruction_2 end / rval' -> val
{ var' = ([] : list ty) } @ rval = rval'
-------------------------------------------------------------------------------------------- :: list_for_nil
E |- for var in var' do instruction_1 done / rval' -> rval
P,E |- for var in var' do instruction_1 done / rval' -> rval
{ var = val } @ rval = rval'
E |- instruction_1 / rval' -> rval1
P,E |- instruction_1 / rval' -> rval1
{ var' = tl } @ rval1 = rval''
E |- for var in var' do instruction_1 done / rval'' -> rval2
P,E |- for var in var' do instruction_1 done / rval'' -> rval2
-------------------------------------------------------------------------------------------- :: list_for_cons
E |- for var in var' do instruction_1 done / { var' = val :: tl } -> rval2
P,E |- for var in var' do instruction_1 done / { var' = val :: tl } -> rval2
......@@ -97,60 +97,60 @@ defns
Jeval :: 'eval_' ::=
defn
E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
P,E |- rhs / val -> val' :: :: rhs :: rhs_ {{com Right-hand side evaluation}} by
------------------------------------------------------------------------------------------------------------------------------------- :: map
E |- {| var_1 |-> var'_1 ; .. ; var_n |-> var'_n |} / { var_1 = val_1 ; .. ; var_n = val_n ; var'_1 = val'_1 ; .. ; var'_n = val'_n } -> ({| val_1 |-> val'_1 ; .. ; val_n |-> val'_n |} : map ty ty')
P,E |- {| var_1 |-> var'_1 ; .. ; var_n |-> var'_n |} / { var_1 = val_1 ; .. ; var_n = val_n ; var'_1 = val'_1 ; .. ; var'_n = val'_n } -> ({| val_1 |-> val'_1 ; .. ; val_n |-> val'_n |} : map ty ty')
-------------------------------------------------------------------------------------- :: map_map_nil
E |- map var_1 |-> var_2 in var_3 do rhs done / { var_3 = ({||} : map ty ty') } -> ({||} : map ty ty')
P,E |- map var_1 |-> var_2 in var_3 do rhs done / { var_3 = ({||} : map ty ty') } -> ({||} : map ty ty')
E |- rhs / { var_1 = val_1; var_2 = val_2 } -> val'_2
E |- map var_1 |-> var_2 in var_3 do rhs done / { var_3 = mval } -> mval'
P,E |- rhs / { var_1 = val_1; var_2 = val_2 } -> val'_2
P,E |- map var_1 |-> var_2 in var_3 do rhs done / { var_3 = mval } -> mval'
---------------------------------------------------------------------------------------------------------------------- :: map_map_cons
E |- map var_1 |-> var_2 in var_3 do rhs done / { var_3 = {| val_1 |-> val_2 ; <mval> |} } -> {| val_1 |-> val'_2 ; <mval'> |}
P,E |- map var_1 |-> var_2 in var_3 do rhs done / { var_3 = {| val_1 |-> val_2 ; <mval> |} } -> {| val_1 |-> val'_2 ; <mval'> |}
------------------------------------------------------------------------------ :: map_get_nil
E |- var_1[var_2] / { var_1 = ({||} : map ty ty'); var_2 = val_2 } -> (None {} : [ None : unit | Some : ty ])
P,E |- var_1[var_2] / { var_1 = ({||} : map ty ty'); var_2 = val_2 } -> (None {} : [ None : unit | Some : ty ])
---------------------------------------------------------------------------- :: map_get_found
E |- var_1[var_2] / { var_1 = {| val_2 |-> val ; <mval> |} ; var_2 = val_2 } -> (Some val : [ None : unit | Some : ty ])
P,E |- var_1[var_2] / { var_1 = {| val_2 |-> val ; <mval> |} ; var_2 = val_2 } -> (Some val : [ None : unit | Some : ty ])
val_2 <> val'_2
E |- var_1[var_2] / { var_1 = mval ; var_2 = val_2 } -> val'
P,E |- var_1[var_2] / { var_1 = mval ; var_2 = val_2 } -> val'
---------------------------------------------------------------------------- :: map_get_next
E |- var_1[var_2] / { var_1 = {| val_2 |-> val ; <mval> |} ; var_2 = val_2 } -> val'
P,E |- var_1[var_2] / { var_1 = {| val_2 |-> val ; <mval> |} ; var_2 = val_2 } -> val'
-------------------------------------------------------------------------------------------------------------- :: map_update_nil_none
E |- {| var_1 with var_2 |-> var_3 |} / {var_1 = ({||} : map ty ty') ; var_2 = val_2 ; var_3 = (None {} : [ None : unit | Some : ty ]) } -> ({||} : map ty ty')
P,E |- {| var_1 with var_2 |-> var_3 |} / {var_1 = ({||} : map ty ty') ; var_2 = val_2 ; var_3 = (None {} : [ None : unit | Some : ty ]) } -> ({||} : map ty ty')
-------------------------------------------------------------------------------------------------------------------- :: map_update_nil_some
E |- {| var_1 with var_2 |-> var_3 |} / {var_1 = ({||} : map ty ty') ; var_2 = val_2 ; var_3 = (Some val3 : [ None : unit | Some : ty ]) } -> ({| val_2 |-> val_3 |} : map ty ty')
P,E |- {| var_1 with var_2 |-> var_3 |} / {var_1 = ({||} : map ty ty') ; var_2 = val_2 ; var_3 = (Some val3 : [ None : unit | Some : ty ]) } -> ({| val_2 |-> val_3 |} : map ty ty')
-------------------------------------------------------------------------------------------------------------- :: map_update_cons_none
E |- {| var_1 with var_2 |-> var_3 |} / {var_1 = {| val_2 |-> val'_3 ; <mval> |} ; var_2 = val_2 ; var_3 = (None {} : [ None : unit | Some : ty ]) } -> mval
P,E |- {| var_1 with var_2 |-> var_3 |} / {var_1 = {| val_2 |-> val'_3 ; <mval> |} ; var_2 = val_2 ; var_3 = (None {} : [ None : unit | Some : ty ]) } -> mval
-------------------------------------------------------------------------------------------------------------------- :: map_update_cons_some