zenon/formal-methods-fstar
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Add CALL definition

Browse Source
This commit is contained in:
Tobias Eidelpes 2021-06-03 10:30:02 +02:00
parent 4a588e982b
commit 7f9fa7758e
1 changed files with 20 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
Project2.fst
View File

@ -142,8 +142,17 @@ let step te cs =
Next (Exec((((gas-1, j, mem, stack'), (actor, input, code), gs))::ps)) Next (Exec((((gas-1, j, mem, stack'), (actor, input, code), gs))::ps))
| (RETURN, v::stack') -> Next (Ter (HaltState gs v (gas-1)) ps) | (RETURN, v::stack') -> Next (Ter (HaltState gs v (gas-1)) ps)
| (STOP, stack') -> Next (Ter (HaltState gs 0 (gas-1)) ps) | (STOP, stack') -> Next (Ter (HaltState gs 0 (gas-1)) ps)
| (TIMESTAMP, stack') -> magic () | (TIMESTAMP, stack') -> Next (Exec(((gas-1, pc+1, mem, te::stack'), (actor, input, code), gs)::ps))
| (CALL, to::v::inp::resaddr::stack') -> magic () | (CALL, to::v::inp::resaddr::stack') -> let (bal, _, _) = gs actor in
if bal < v then Next (Ter ExcState ps) else
if v < 0 then Next (Ter ExcState ps) else
let to_acc = (let (bal, stor, code) = gs to in (bal+v, stor, code)) in
let actor_acc = (let (bal, stor, code) = gs actor in (bal-v, stor, code)) in
let gs' = update (update gs to to_acc) actor actor_acc in
let mu' = (gas-1, 0, (fun x -> 0), []) in
let env' = (to, inp, (let (_, _, code) = (gs to) in code)) in
let old_ex_state = ((gas, pc, mem, to::v::inp::resaddr::stack'), (actor, input, code), gs) in
Next (Exec((mu', env', gs')::(old_ex_state::ps)))
| _ -> Next (Ter ExcState ps) | _ -> Next (Ter ExcState ps)
(* A simple wrapper for the step function that removes the execution outcome *) (* A simple wrapper for the step function that removes the execution outcome *)