diff --git a/ConfigParser.hs b/ConfigParser.hs index c93157e..acc1016 100644 --- a/ConfigParser.hs +++ b/ConfigParser.hs @@ -14,19 +14,24 @@ jsonFile :: FilePath jsonFile = "config-sample.json" data DistributionConfig = - Config [ProcessConfig] [String] + Config [ProcessConfig] [String] [ConstantConfig] deriving (Show, Generic) data ProcessConfig = PConfig String [H.Action] deriving (Show, Generic) +data ConstantConfig = + Constant String H.Value + deriving (Show, Generic) + instance FromJSON DistributionConfig where parseJSON = withObject "DistribuitionConfig" $ \obj -> do ps <- obj .: "processes" vs <- obj .: "shared_variables" - return (Config ps vs) + cs <- obj .: "constants" + return (Config ps vs cs) instance FromJSON ProcessConfig where parseJSON = @@ -37,6 +42,15 @@ instance FromJSON ProcessConfig where Left e -> fail ("Invalid action in:" ++ show as ++ ". Error: " ++ show e) Right cs -> return (PConfig i cs) +instance FromJSON ConstantConfig where + parseJSON = + withObject "ConstantConfig" $ \obj -> do + n <- obj .: "name" + v <- obj .: "value" + case parseValue v of + Left e -> fail ("Invalid value in:" ++ show v ++ ". Error: " ++ show e) + Right val -> return (Constant n val) + parseConfig :: FilePath -> IO (Either String DistributionConfig) parseConfig file = do content <- B.readFile file @@ -45,4 +59,4 @@ parseConfig file = do -- main = parseJson jsonFile >>= print processNames :: DistributionConfig -> [String] -processNames (Config ps _) = map (\(PConfig n _) -> n) ps +processNames (Config ps _ _) = map (\(PConfig n _) -> n) ps diff --git a/Elixir.hs b/Elixir.hs index 9d34177..23a5300 100644 --- a/Elixir.hs +++ b/Elixir.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE TupleSections #-} module Elixir where import Data.List @@ -9,14 +10,14 @@ import Helpers import Snippets generate :: Spec -> DistributionConfig -> [(String, ElixirCode)] -generate (Spec m i n ds) (Config ps shared) = +generate (Spec m i n ds) (Config ps shared consts) = let defs = filter (not . (specialDef i n)) ds cs = findConstants ds vs = findVariables ds header = moduleHeader (moduleName m) m shared False -- defNext = findIdentifier n ds base = baseSpec header cs vs defs - in (moduleName m, base):map (generateForProcess m n vs defs) ps + in (moduleName m, base):map (generateForProcess m n vs cs defs) ps generateStarter :: Spec -> (String, ElixirCode) generateStarter (Spec m i _ ds) = @@ -27,12 +28,12 @@ generateStarter (Spec m i _ ds) = in (moduleName m, starterTask (moduleName m) state) generateForProcess :: - Module -> String -> [Variable] -> [Definition] -> ProcessConfig -> (String, ElixirCode) -generateForProcess m n vs defs (PConfig p as) = + Module -> String -> [Variable] -> [Constant] -> [Definition] -> ProcessConfig -> (String, ElixirCode) +generateForProcess m n vs cs defs (PConfig p as) = let name = moduleName m ++ "_" ++ p header = moduleHeader name m [] True defNext = ActionDefinition n [] [] (ActionOr as) - in (name, spec header [] vs [] defNext) + in (name, spec header cs vs [] defNext) -- filterDefs :: [Call] -> [Definition] -> [Definition] @@ -88,11 +89,16 @@ definition g (ValueDefinition i ps v) = declaration i ps ++ ident (value g v) ++ -- Comment translation, not specified definition _ (Comment s) = "# " ++ cleanTrailing s +definitionName (ActionDefinition i _ _ _) = i +definitionName (ValueDefinition i _ _) = i + +localDefinition g (ValueDefinition i ps v) = snake i ++ " = fn(variables" ++ intercalate "" (map ("," ++) ps) ++ ") -> " ++ value g v ++ "end" + {-- \vdash_d --} actionsAndConditions :: Context -> Action -> ([ElixirCode], [ElixirCode]) -- (CALL) actionsAndConditions g (ActionCall i ps) = - ([call (i ++ "Condition") ("variables" : map (value g) ps)], [call i ("variables" : map (value g) ps)]) + ([call g (i ++ "Condition") ("variables" : map (value g) ps)], [call g i ("variables" : map (value g) ps)]) -- (AND) actionsAndConditions g (ActionAnd as) = let (ics, ias) = unzipAndFold (map (actionsAndConditions g) as) @@ -125,6 +131,9 @@ actionsAndConditions g (ActionIf p t e) = else cFold ce) a = ifExpr cp (aFold at) (aFold ae) in ([c], [a]) +actionsAndConditions g (ActionLet ds a) = let (cs, as) = actionsAndConditions (g ++ map ((,"local") . definitionName) ds) a + defs = unwords (map (localDefinition g) ds) + in (defs:cs, defs:as) -- (COND) actionsAndConditions g (Condition p) = ([value g p], []) -- [new] (EXT) @@ -137,7 +146,7 @@ actionsAndConditions g (Exists i v a) = actionsAndConditions g (ForAll i v a) = let ig = (i, "param") : g (ics, ias) = actionsAndConditions ig a - c = "Enum.all?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ " end\n)" + c = "Enum.all?(" ++ value ig v ++ ", fn (" ++ i ++ ") ->" ++ cFold ics ++ " end)" in ([c], ias) -- (TRA) actionsAndConditions g a = ([], [action g a]) @@ -179,7 +188,7 @@ value g (Lt v1 v2) = value g v1 ++ " < " ++ value g v2 value g (Gte v1 v2) = value g v1 ++ " >= " ++ value g v2 value g (Lte v1 v2) = value g v1 ++ " <= " ++ value g v2 -- [new] (PRED-CALL) -value g (ConditionCall i ps) = call i ("variables" : map (value g) ps) +value g (ConditionCall i ps) = call g i ("variables" : map (value g) ps) -- (PRED-IN) value g (RecordBelonging v1 v2) = "Enum.member?(" ++ value g v2 ++ ", " ++ value g v1 ++ ")" -- [new] (PRED-NOTIN) @@ -209,6 +218,7 @@ value g (Filtered i v p) = value g (Cardinality s) = "Enum.count(" ++ value g s ++ ")" value g (SetIn v s) = "MapSet.member?(" ++ value g s ++ ", " ++ value g v ++ ")" value g (SetMinus s1 s2) = "MapSet.difference(" ++ value g s1 ++ ", " ++ value g s2 ++ ")" +value g (SetTimes s1 s2) = "(for x <- " ++ value g s1 ++ ", y <- " ++ value g s2 ++ ", do: {x, y})" -- (REC-LIT) and (REC-EX), aggregated to ensure ordering value g (Record rs) = let (literals, generations) = partition isLiteral rs @@ -219,7 +229,7 @@ value g (Record rs) = else m ++ " |> Enum.into(" ++ l ++ ")" -- (REC-EXCEPT) value g (Except i es) = - intercalate "\n" (map (\(k, v) -> "Map.put(" ++ reference g i ++ ", " ++ value g k ++ ", " ++ value g v ++ ")") es) + intercalate "|>" (reference g i:map (\(k, v) -> "Map.put(" ++ value g k ++ ", " ++ value g v ++ ")") es) value g (FunGen i s v) = "Map.new(" ++ value g s ++ ", fn(" ++ i ++ ") -> {" ++ i ++ ", " ++ value ((i, "param") : g) v ++ "} end)" -- [new] (CASE) value g (Case ms) = "cond do\n" ++ intercalate "\n" (map (caseMatch g) ms) ++ "\nend\n" diff --git a/Head.hs b/Head.hs index 40f41b7..2a43139 100644 --- a/Head.hs +++ b/Head.hs @@ -60,6 +60,7 @@ data Action | ActionOr [Action] | ActionCall Identifier [Value] | ActionIf Value Action Action + | ActionLet [Definition] Action | Exists Identifier Value Action | ForAll Identifier Value Action deriving (Show, Eq) @@ -91,6 +92,7 @@ data Value | Union Value Value | Filtered Identifier Value Value | Cardinality Value + | Fold Value Value Value | Record [(Key, Value)] | RecordSet [(Key, Value)] | Except Identifier [(Value, Value)] diff --git a/Helpers.hs b/Helpers.hs index 59e83bd..37ffc3e 100644 --- a/Helpers.hs +++ b/Helpers.hs @@ -29,8 +29,9 @@ sharedVariablesDeclaration shared = moduleContext (Module m _) = [(m, "module")] -- (CALL) helpers -call i [] = snake i -call i ps = snake i ++ "(" ++ intercalate ", " ps ++ ")" +call g i [] = snake i +call g i ps = let divider = if (i, "local") `elem` g then "." else "" + in snake i ++ divider ++ "(" ++ intercalate ", " ps ++ ")" -- (IF) helpers ifExpr c t e = "(if " ++ c ++ ", do: " ++ t ++ ", else: " ++ e ++ ")" @@ -58,18 +59,20 @@ enclose s = "(" ++ s ++ ")" cFold :: [ElixirCode] -> ElixirCode cFold [] = "true" cFold [c] = c -cFold cs = "Enum.all?([" ++ intercalate ", " cs ++ "])" +cFold cs = let (preassignments, conditions) = partition preassignment cs + in intercalate "" (map (++ "\n") preassignments) ++ "Enum.all?([" ++ intercalate ", " conditions ++ "])" aFold :: [ElixirCode] -> ElixirCode aFold [] = "%{}" aFold as = - let (otherActions, actions) = partition preassignment as + let (preassignments, as') = partition preassignment as + (postAssignments, actions) = partition postassignment as' kvs = intercalate ",\n" (map keyValue actions) initialVariables = case actions of [] -> [] _ -> ["%{\n" ++ ident kvs ++ "\n}"] - in mapMerge (initialVariables ++ otherActions) + in intercalate "" (map (++ "\n") preassignments) ++ mapMerge (initialVariables ++ postAssignments) orFold :: [ElixirCode] -> ElixirCode orFold [] = "true" @@ -86,11 +89,12 @@ keyValue a = drop 3 (dropEnd 2 a) mapMerge [m] = m mapMerge (m:ms) = "Map.merge(\n " ++ m ++ ",\n" ++ ident (mapMerge ms) ++ ")\n" -preassignment as = +preassignment as = any (isPrefixOf " = ") (tails as) +postassignment as = (head as) == '(' || take 2 as == "if" || dropWhile (/= ':') as == [] || take 4 as == "Enum" || take 3 as == "Map" || take 4 as == "List" -interpolate (Lit (Str i)) = "#{inspect " ++ i ++ "}" +interpolate (Lit (Str i)) = i interpolate (Ref i) = "#{inspect " ++ i ++ "}" interpolate i = show i diff --git a/JSONParser.hs b/JSONParser.hs index b19d785..0fe164a 100644 --- a/JSONParser.hs +++ b/JSONParser.hs @@ -71,6 +71,7 @@ instance FromJSON Declaration where case filename :: String of "Functions" -> return Ignored "SequencesExt" -> return Ignored + "Apalache" -> return Ignored _ -> do k <- obj .: "kind" n <- obj .: "name" @@ -110,7 +111,8 @@ instance FromJSON Expression where -- TODO: Parse this from config or something actionNames :: [String] -actionNames = ["SendMsg", "Deactivate", "Environment", "System", "PassToken", "InitiateProbe", "Next"] +-- actionNames = ["SendMsg", "Deactivate", "Environment", "System", "PassToken", "InitiateProbe", "Next"] +actionNames = ["SubmitTransfer", "CommitTransfer", "SubmitTransferFrom", "CommitTransferFrom", "SubmitApprove", "CommitApprove", "Next"] notIgnored Ignored = False notIgnored _ = True @@ -202,6 +204,12 @@ convertValue (OperEx o as) = "SET_FILTER" -> case as of [a1, a2, a3] -> liftA3 H.Filtered (identifier a1) (convertValue a2) (convertValue a3) + "SET_UNION2" -> + case as of + [a1, a2] -> liftA2 H.Union (convertValue a1) (convertValue a2) + "Apalache!ApaFoldSet" -> + case as of + [a1, a2, a3] -> liftA3 H.Fold (convertValue a1) (convertValue a2) (convertValue a3) "INT_RANGE" -> case as of [a1, a2] -> liftA2 H.Range (convertValue a1) (convertValue a2) @@ -287,7 +295,7 @@ convertAction (OperEx o as) = [a1, a2, a3] -> liftA3 H.ForAll (identifier a1) (convertValue a2) (convertExpression a3) "UNCHANGED" -> case as of - [a] -> liftA H.Unchanged (manyIdentifiers a) + [a] -> fmap H.Unchanged (manyIdentifiers a) "AND" -> case as of es -> fmap H.ActionAnd (mapM convertExpression es) @@ -300,15 +308,19 @@ convertAction (OperEx o as) = "OPER_APP" -> case as of (e:es) -> liftA2 H.ActionCall (identifier e) (mapM convertValue es) + "IF_THEN_ELSE" -> + case as of + [a1, a2, a3] -> liftA3 H.ActionIf (convertValue a1) (convertAction a2) (convertAction a3) op -> Left ("Unknown action operator " ++ op ++ " with args " ++ show as) in left (\s -> s ++ "\nwhen converting " ++ show (OperEx o as)) r +convertAction (LetInEx ds b) = liftA2 H.ActionLet (mapM convertDefinitions ds) (convertAction b) convertExpression :: Expression -> Either String H.Action -convertExpression (OperEx o as) = - if isPredicate (OperEx o as) - then convertValue (OperEx o as) >>= \x -> Right (H.Condition x) - else convertAction (OperEx o as) convertExpression (ValEx v) = convertValue (ValEx v) >>= \cv -> Right (H.Condition cv) +convertExpression e = + if isPredicate e + then convertValue e >>= \x -> Right (H.Condition x) + else convertAction e actionOperators :: [String] actionOperators = ["PRIME", "UNCHANGED"] @@ -321,8 +333,12 @@ isPredicate (OperEx o as) = all isPredicate as && if o == "OPER_APP" then case identifier (head as) of {Right i -> i `notElem` actionNames} else o `notElem` actionOperators +isPredicate (LetInEx ds b) = all definitionIsPredicate ds && isPredicate b isPredicate _ = True +definitionIsPredicate (Declaration k n ps (Just body)) = isPredicate body +definitionIsPredicate _ = True + isTemporal :: Expression -> Bool isTemporal (OperEx o as) = o `elem` temporalOperators || any isTemporal as isTemporal _ = False diff --git a/elixir/lib/generated_code/er_c20.ex b/elixir/lib/generated_code/er_c20.ex new file mode 100644 index 0000000..be8fdd4 --- /dev/null +++ b/elixir/lib/generated_code/er_c20.ex @@ -0,0 +1,165 @@ +defmodule ERC20 do + def shared_variables do + [ + :pendingTransactions, + :lastTx, + :nextTxId, + ] + end + require Oracle + @amounts [0, 100, 500] + def amounts, do: @amounts + + + @addr ["alice_OF_ADDR", "bob_OF_ADDR"] + def addr, do: @addr + + + def submit_transfer_condition(variables, _sender, _toAddr, _value) do + new_tx = fn(variables) -> %{ "id" => variables[:next_tx_id], "tag" => "transfer", "fail" => false, "sender" => _sender, "toAddr" => _toAddr, "value" => _value }end + Enum.all?([true]) + end + + def submit_transfer(variables, _sender, _toAddr, _value) do + new_tx = fn(variables) -> %{ "id" => variables[:next_tx_id], "tag" => "transfer", "fail" => false, "sender" => _sender, "toAddr" => _toAddr, "value" => _value }end + %{ + pending_transactions: MapSet.put(variables[:pending_transactions], new_tx.(variables)), + last_tx: %{ "id" => 0, "tag" => "None", "fail" => false }, + next_tx_id: variables[:next_tx_id] + 1, + balance_of: variables[:balance_of], + allowance: variables[:allowance] + } + end + + + def commit_transfer_condition(variables, _tx) do + fail = fn(variables) -> _tx["value"] < 0 or _tx["value"] > variables[:balance_of][_tx["sender"]] or _tx["sender"] == _tx["toAddr"]end + Enum.all?([_tx["tag"] == "transfer", (if fail.(variables), do: false, else: true)]) + end + + def commit_transfer(variables, _tx) do + fail = fn(variables) -> _tx["value"] < 0 or _tx["value"] > variables[:balance_of][_tx["sender"]] or _tx["sender"] == _tx["toAddr"]end + Map.merge( + %{ + pending_transactions: MapSet.difference(variables[:pending_transactions], MapSet.new([_tx])), + last_tx: _tx|>Map.put("fail", fail.(variables)) + }, + (if fail.(variables), do: %{ + balance_of: variables[:balance_of], + allowance: variables[:allowance], + next_tx_id: variables[:next_tx_id] + }, else: %{ + balance_of: variables[:balance_of]|>Map.put(_tx["sender"], (variables[:balance_of][_tx["sender"]]) - (_tx["value"]))|>Map.put(_tx["toAddr"], (variables[:balance_of][_tx["toAddr"]]) + (_tx["value"])), + allowance: variables[:allowance], + next_tx_id: variables[:next_tx_id] + })) + end + + + def submit_transfer_from_condition(variables, _sender, _fromAddr, _toAddr, _value) do + new_tx = fn(variables) -> %{ "id" => variables[:next_tx_id], "tag" => "transferFrom", "fail" => false, "sender" => _sender, "fromAddr" => _fromAddr, "toAddr" => _toAddr, "value" => _value }end + Enum.all?([true]) + end + + def submit_transfer_from(variables, _sender, _fromAddr, _toAddr, _value) do + new_tx = fn(variables) -> %{ "id" => variables[:next_tx_id], "tag" => "transferFrom", "fail" => false, "sender" => _sender, "fromAddr" => _fromAddr, "toAddr" => _toAddr, "value" => _value }end + %{ + pending_transactions: MapSet.put(variables[:pending_transactions], new_tx.(variables)), + last_tx: %{ "id" => 0, "tag" => "None", "fail" => false }, + next_tx_id: variables[:next_tx_id] + 1, + balance_of: variables[:balance_of], + allowance: variables[:allowance] + } + end + + + def commit_transfer_from_condition(variables, _tx) do + fail = fn(variables) -> _tx["value"] < 0 or _tx["value"] > variables[:balance_of][_tx["fromAddr"]] or _tx["value"] > variables[:allowance][{_tx["fromAddr"], _tx["sender"]}] or _tx["fromAddr"] == _tx["toAddr"]end + Enum.all?([_tx["tag"] == "transferFrom", (if fail.(variables), do: false, else: true)]) + end + + def commit_transfer_from(variables, _tx) do + fail = fn(variables) -> _tx["value"] < 0 or _tx["value"] > variables[:balance_of][_tx["fromAddr"]] or _tx["value"] > variables[:allowance][{_tx["fromAddr"], _tx["sender"]}] or _tx["fromAddr"] == _tx["toAddr"]end + Map.merge( + %{ + pending_transactions: MapSet.difference(variables[:pending_transactions], MapSet.new([_tx])), + last_tx: _tx|>Map.put("fail", fail.(variables)) + }, + (if fail.(variables), do: %{ + balance_of: variables[:balance_of], + allowance: variables[:allowance], + next_tx_id: variables[:next_tx_id] + }, else: %{ + balance_of: variables[:balance_of]|>Map.put(_tx["fromAddr"], (variables[:balance_of][_tx["fromAddr"]]) - (_tx["value"]))|>Map.put(_tx["toAddr"], (variables[:balance_of][_tx["toAddr"]]) + (_tx["value"])), + allowance: variables[:allowance]|>Map.put({_tx["fromAddr"], _tx["sender"]}, (variables[:allowance][{_tx["fromAddr"], _tx["sender"]}]) - (_tx["value"])), + next_tx_id: variables[:next_tx_id] + })) + end + + + def submit_approve_condition(variables, _sender, _spender, _value) do + new_tx = fn(variables) -> %{ "id" => variables[:next_tx_id], "tag" => "approve", "fail" => false, "sender" => _sender, "spender" => _spender, "value" => _value }end + Enum.all?([true]) + end + + def submit_approve(variables, _sender, _spender, _value) do + new_tx = fn(variables) -> %{ "id" => variables[:next_tx_id], "tag" => "approve", "fail" => false, "sender" => _sender, "spender" => _spender, "value" => _value }end + %{ + pending_transactions: MapSet.put(variables[:pending_transactions], new_tx.(variables)), + last_tx: %{ "id" => 0, "tag" => "None", "fail" => false }, + next_tx_id: variables[:next_tx_id] + 1, + balance_of: variables[:balance_of], + allowance: variables[:allowance] + } + end + + + def commit_approve_condition(variables, _tx) do + fail = fn(variables) -> _tx["value"] < 0 or _tx["sender"] == _tx["spender"]end + Enum.all?([_tx["tag"] == "approve", (if fail.(variables), do: false, else: true)]) + end + + def commit_approve(variables, _tx) do + fail = fn(variables) -> _tx["value"] < 0 or _tx["sender"] == _tx["spender"]end + Map.merge( + %{ + pending_transactions: MapSet.difference(variables[:pending_transactions], MapSet.new([_tx])), + balance_of: variables[:balance_of], + next_tx_id: variables[:next_tx_id], + last_tx: _tx|>Map.put("fail", fail.(variables)) + }, + (if fail.(variables), do: %{ + allowance: variables[:allowance] + }, else: %{ + allowance: variables[:allowance]|>Map.put({_tx["sender"], _tx["spender"]}, _tx["value"]) + })) + end + + + + def decide_action(oracle, variables, actions, step) do + different_states = Enum.uniq_by(actions, fn(action) -> action[:state] end) + + cond do + Enum.count(different_states) == 1 -> + Enum.at(actions, 0)[:state] + true -> + send oracle, {:choose, self(), actions} + + receive do + {:ok, n} -> Enum.at(actions, n)[:state] + {:cancel} -> variables + {:stop} -> exit(0) + end + end + end + + def wait_lock(oracle) do + send(oracle, {:lock, self()}) + receive do + {:lock_acquired, state} -> IO.puts("Lock acquired"); {map, _} = Map.split(state, shared_variables); map + {:already_locked, _} -> IO.puts("Lock refused"); Process.sleep(1000); wait_lock(oracle) + end + end +end + diff --git a/elixir/lib/generated_code/er_c20_alice.ex b/elixir/lib/generated_code/er_c20_alice.ex new file mode 100644 index 0000000..69daaf4 --- /dev/null +++ b/elixir/lib/generated_code/er_c20_alice.ex @@ -0,0 +1,60 @@ +defmodule ERC20_alice do + require Oracle + + import ERC20 + @amounts "" + def amounts, do: @amounts + + + @addr "" + def addr, do: @addr + + + + def next(variables) do + Enum.filter( + List.flatten([ + Enum.map(@addr, fn (toAddr) -> [ + Enum.map(@amounts, fn (value) -> [ + %{ action: "SubmitTransfer(alice_OF_ADDR, #{inspect toAddr}, #{inspect value})", condition: submit_transfer_condition(variables, "alice_OF_ADDR", toAddr, value), state: submit_transfer(variables, "alice_OF_ADDR", toAddr, value) } + ] end + ) + ] end + ), + Enum.map(@addr, fn (fromAddr) -> [ + Enum.map(@addr, fn (toAddr) -> [ + Enum.map(@amounts, fn (value) -> [ + %{ action: "SubmitTransferFrom(alice_OF_ADDR, #{inspect fromAddr}, #{inspect toAddr}, #{inspect value})", condition: submit_transfer_from_condition(variables, "alice_OF_ADDR", fromAddr, toAddr, value), state: submit_transfer_from(variables, "alice_OF_ADDR", fromAddr, toAddr, value) } + ] end + ) + ] end + ) + ] end + ), + Enum.map(@addr, fn (spender) -> [ + Enum.map(@amounts, fn (value) -> [ + %{ action: "SubmitApprove(alice_OF_ADDR, #{inspect spender}, #{inspect value})", condition: submit_approve_condition(variables, "alice_OF_ADDR", spender, value), state: submit_approve(variables, "alice_OF_ADDR", spender, value) } + ] end + ) + ] end + ) + ]), + fn(action) -> action[:condition] end + ) + end + + def main(oracle, private_variables, step) do + shared_state = wait_lock(oracle) + variables = Map.merge(private_variables, shared_state) + + IO.puts(inspect(variables)) + actions = next(variables) + + next_variables = decide_action(oracle, variables, actions, step) + send(oracle, {:notify, step, variables, next_variables}) + Process.sleep(2000) + + main(oracle, next_variables, step + 1) + end +end + diff --git a/elixir/lib/generated_code/er_c20_blockchain.ex b/elixir/lib/generated_code/er_c20_blockchain.ex new file mode 100644 index 0000000..3b3288b --- /dev/null +++ b/elixir/lib/generated_code/er_c20_blockchain.ex @@ -0,0 +1,48 @@ +defmodule ERC20_blockchain do + require Oracle + + import ERC20 + @amounts "" + def amounts, do: @amounts + + + @addr "" + def addr, do: @addr + + + + def next(variables) do + Enum.filter( + List.flatten([ + Enum.map(variables[:pending_transactions], fn (tx) -> [ + %{ action: "CommitTransfer(#{inspect tx})", condition: commit_transfer_condition(variables, tx), state: commit_transfer(variables, tx) } + ] end + ), + Enum.map(variables[:pending_transactions], fn (tx) -> [ + %{ action: "CommitTransferFrom(#{inspect tx})", condition: commit_transfer_from_condition(variables, tx), state: commit_transfer_from(variables, tx) } + ] end + ), + Enum.map(variables[:pending_transactions], fn (tx) -> [ + %{ action: "CommitApprove(#{inspect tx})", condition: commit_approve_condition(variables, tx), state: commit_approve(variables, tx) } + ] end + ) + ]), + fn(action) -> action[:condition] end + ) + end + + def main(oracle, private_variables, step) do + shared_state = wait_lock(oracle) + variables = Map.merge(private_variables, shared_state) + + IO.puts(inspect(variables)) + actions = next(variables) + + next_variables = decide_action(oracle, variables, actions, step) + send(oracle, {:notify, step, variables, next_variables}) + Process.sleep(2000) + + main(oracle, next_variables, step + 1) + end +end + diff --git a/elixir/lib/generated_code/er_c20_bob.ex b/elixir/lib/generated_code/er_c20_bob.ex new file mode 100644 index 0000000..69fe444 --- /dev/null +++ b/elixir/lib/generated_code/er_c20_bob.ex @@ -0,0 +1,60 @@ +defmodule ERC20_bob do + require Oracle + + import ERC20 + @amounts "" + def amounts, do: @amounts + + + @addr "" + def addr, do: @addr + + + + def next(variables) do + Enum.filter( + List.flatten([ + Enum.map(@addr, fn (toAddr) -> [ + Enum.map(@amounts, fn (value) -> [ + %{ action: "SubmitTransfer(bob_OF_ADDR, #{inspect toAddr}, #{inspect value})", condition: submit_transfer_condition(variables, "bob_OF_ADDR", toAddr, value), state: submit_transfer(variables, "bob_OF_ADDR", toAddr, value) } + ] end + ) + ] end + ), + Enum.map(@addr, fn (fromAddr) -> [ + Enum.map(@addr, fn (toAddr) -> [ + Enum.map(@amounts, fn (value) -> [ + %{ action: "SubmitTransferFrom(bob_OF_ADDR, #{inspect fromAddr}, #{inspect toAddr}, #{inspect value})", condition: submit_transfer_from_condition(variables, "bob_OF_ADDR", fromAddr, toAddr, value), state: submit_transfer_from(variables, "bob_OF_ADDR", fromAddr, toAddr, value) } + ] end + ) + ] end + ) + ] end + ), + Enum.map(@addr, fn (spender) -> [ + Enum.map(@amounts, fn (value) -> [ + %{ action: "SubmitApprove(bob_OF_ADDR, #{inspect spender}, #{inspect value})", condition: submit_approve_condition(variables, "bob_OF_ADDR", spender, value), state: submit_approve(variables, "bob_OF_ADDR", spender, value) } + ] end + ) + ] end + ) + ]), + fn(action) -> action[:condition] end + ) + end + + def main(oracle, private_variables, step) do + shared_state = wait_lock(oracle) + variables = Map.merge(private_variables, shared_state) + + IO.puts(inspect(variables)) + actions = next(variables) + + next_variables = decide_action(oracle, variables, actions, step) + send(oracle, {:notify, step, variables, next_variables}) + Process.sleep(2000) + + main(oracle, next_variables, step + 1) + end +end + diff --git a/elixir/lib/mix/tasks/er_c20_starter.ex b/elixir/lib/mix/tasks/er_c20_starter.ex new file mode 100644 index 0000000..2983cee --- /dev/null +++ b/elixir/lib/mix/tasks/er_c20_starter.ex @@ -0,0 +1,28 @@ +defmodule Mix.Tasks.ErC20Starter do + @moduledoc "Printed when the user requests `mix help echo`" + @shortdoc "Echoes arguments" + use Mix.Task + import ERC20 + + @impl Mix.Task + def run(_) do + variables = %{} + initial_state = %{ + balance_of: Map.new(ERC20.addr, fn(a) -> {a, 100} end), + allowance: Map.new((for x <- ERC20.addr, y <- ERC20.addr, do: {x, y}), fn(pair) -> {pair, 0} end), + pending_transactions: MapSet.new([]), + next_tx_id: 0, + last_tx: %{ "id" => 0, "tag" => "None", "fail" => false } +} + + oracle = spawn(RandomOracle, :start, [initial_state, 0, nil]) + :global.register_name("oracle", oracle) + + ref = Process.monitor(oracle) + + receive do + {:DOWN, ^ref, _, _, _} -> + IO.puts("Oracle is down") + end + end +end diff --git a/tla_specifications/ERC20/ERC20.json b/tla_specifications/ERC20/ERC20.json new file mode 100644 index 0000000..5ca6c1c --- /dev/null +++ b/tla_specifications/ERC20/ERC20.json @@ -0,0 +1,9438 @@ +{ + "name": "ApalacheIR", + "version": "1.0", + "description": "https://apalache.informal.systems/docs/adr/005adr-json.html", + "modules": [ + { + "kind": "TlaModule", + "name": "ERC20", + "declarations": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 50, + "column": 5 + }, + "to": { + "line": 50, + "column": 11 + } + }, + "type": "Untyped", + "kind": "TlaConstDecl", + "name": "AMOUNTS" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 46, + "column": 5 + }, + "to": { + "line": 46, + "column": 8 + } + }, + "type": "Untyped", + "kind": "TlaConstDecl", + "name": "ADDR" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 62, + "column": 5 + }, + "to": { + "line": 62, + "column": 13 + } + }, + "type": "Untyped", + "kind": "TlaVarDecl", + "name": "allowance" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 77, + "column": 5 + }, + "to": { + "line": 77, + "column": 10 + } + }, + "type": "Untyped", + "kind": "TlaVarDecl", + "name": "lastTx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 56, + "column": 5 + }, + "to": { + "line": 56, + "column": 13 + } + }, + "type": "Untyped", + "kind": "TlaVarDecl", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 80, + "column": 5 + }, + "to": { + "line": 80, + "column": 12 + } + }, + "type": "Untyped", + "kind": "TlaVarDecl", + "name": "nextTxId" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 73, + "column": 5 + }, + "to": { + "line": 73, + "column": 23 + } + }, + "type": "Untyped", + "kind": "TlaVarDecl", + "name": "pendingTransactions" + }, + { + "source": { + "filename": "Apalache", + "from": { + "line": 100, + "column": 1 + }, + "to": { + "line": 102, + "column": 61 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "FunAsSeq", + "formalParams": [ + { + "kind": "OperParam", + "name": "__fn", + "arity": 0 + }, + { + "kind": "OperParam", + "name": "__len", + "arity": 0 + }, + { + "kind": "OperParam", + "name": "__capacity", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "Apalache", + "from": { + "line": 101, + "column": 5 + }, + "to": { + "line": 102, + "column": 61 + } + }, + "type": "Untyped", + "kind": "LetInEx", + "body": { + "source": { + "filename": "Apalache", + "from": { + "line": 102, + "column": 5 + }, + "to": { + "line": 102, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "Sequences!SubSeq", + "args": [ + { + "source": { + "filename": "Apalache", + "from": { + "line": 102, + "column": 12 + }, + "to": { + "line": 102, + "column": 50 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "Apalache!MkSeq", + "args": [ + { + "source": { + "filename": "Apalache", + "from": { + "line": 102, + "column": 18 + }, + "to": { + "line": 102, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "__capacity" + }, + { + "source": { + "filename": "Apalache", + "from": { + "line": 102, + "column": 30 + }, + "to": { + "line": 102, + "column": 49 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "__FunAsSeq_elem_ctor" + } + ] + }, + { + "source": { + "filename": "Apalache", + "from": { + "line": 102, + "column": 53 + }, + "to": { + "line": 102, + "column": 53 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 1 + } + }, + { + "source": { + "filename": "Apalache", + "from": { + "line": 102, + "column": 56 + }, + "to": { + "line": 102, + "column": 60 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "__len" + } + ] + }, + "decls": [ + { + "source": { + "filename": "Apalache", + "from": { + "line": 101, + "column": 9 + }, + "to": { + "line": 101, + "column": 46 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "__FunAsSeq_elem_ctor", + "formalParams": [ + { + "kind": "OperParam", + "name": "__i", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "Apalache", + "from": { + "line": 101, + "column": 38 + }, + "to": { + "line": 101, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "Apalache", + "from": { + "line": 101, + "column": 38 + }, + "to": { + "line": 101, + "column": 41 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "__fn" + }, + { + "source": { + "filename": "Apalache", + "from": { + "line": 101, + "column": 43 + }, + "to": { + "line": 101, + "column": 45 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "__i" + } + ] + } + } + ] + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 83, + "column": 1 + }, + "to": { + "line": 90, + "column": 60 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Init", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 84, + "column": 5 + }, + "to": { + "line": 90, + "column": 60 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 84, + "column": 8 + }, + "to": { + "line": 84, + "column": 39 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 84, + "column": 8 + }, + "to": { + "line": 84, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 84, + "column": 20 + }, + "to": { + "line": 84, + "column": 39 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_CTOR", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 84, + "column": 36 + }, + "to": { + "line": 84, + "column": 38 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 100 + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 84, + "column": 20 + }, + "to": { + "line": 84, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "a" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 84, + "column": 27 + }, + "to": { + "line": 84, + "column": 30 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 86, + "column": 8 + }, + "to": { + "line": 86, + "column": 50 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 86, + "column": 8 + }, + "to": { + "line": 86, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 86, + "column": 20 + }, + "to": { + "line": 86, + "column": 50 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_CTOR", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 86, + "column": 48 + }, + "to": { + "line": 86, + "column": 48 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 86, + "column": 20 + }, + "to": { + "line": 86, + "column": 50 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pair" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 86, + "column": 31 + }, + "to": { + "line": 86, + "column": 42 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_TIMES", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 86, + "column": 31 + }, + "to": { + "line": 86, + "column": 34 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 86, + "column": 39 + }, + "to": { + "line": 86, + "column": 42 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 88, + "column": 8 + }, + "to": { + "line": 88, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 88, + "column": 8 + }, + "to": { + "line": 88, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 88, + "column": 30 + }, + "to": { + "line": 88, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 89, + "column": 8 + }, + "to": { + "line": 89, + "column": 19 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 89, + "column": 8 + }, + "to": { + "line": 89, + "column": 15 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 89, + "column": 19 + }, + "to": { + "line": 89, + "column": 19 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 90, + "column": 8 + }, + "to": { + "line": 90, + "column": 60 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 90, + "column": 8 + }, + "to": { + "line": 90, + "column": 13 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "lastTx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 90, + "column": 17 + }, + "to": { + "line": 90, + "column": 60 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "RECORD", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 90, + "column": 19 + }, + "to": { + "line": 90, + "column": 20 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "id" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 90, + "column": 26 + }, + "to": { + "line": 90, + "column": 26 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 90, + "column": 29 + }, + "to": { + "line": 90, + "column": 31 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 90, + "column": 37 + }, + "to": { + "line": 90, + "column": 42 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "None" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 90, + "column": 45 + }, + "to": { + "line": 90, + "column": 48 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 90, + "column": 54 + }, + "to": { + "line": 90, + "column": 58 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": false + } + } + ] + } + ] + } + ] + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 102, + "column": 1 + }, + "to": { + "line": 109, + "column": 41 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "SubmitTransfer", + "formalParams": [ + { + "kind": "OperParam", + "name": "_sender", + "arity": 0 + }, + { + "kind": "OperParam", + "name": "_toAddr", + "arity": 0 + }, + { + "kind": "OperParam", + "name": "_value", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 103, + "column": 5 + }, + "to": { + "line": 109, + "column": 41 + } + }, + "type": "Untyped", + "kind": "LetInEx", + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 106, + "column": 5 + }, + "to": { + "line": 109, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 106, + "column": 8 + }, + "to": { + "line": 106, + "column": 66 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 106, + "column": 8 + }, + "to": { + "line": 106, + "column": 27 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 106, + "column": 8 + }, + "to": { + "line": 106, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 106, + "column": 31 + }, + "to": { + "line": 106, + "column": 66 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_UNION2", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 106, + "column": 31 + }, + "to": { + "line": 106, + "column": 49 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 106, + "column": 58 + }, + "to": { + "line": 106, + "column": 66 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 106, + "column": 60 + }, + "to": { + "line": 106, + "column": 64 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 106, + "column": 60 + }, + "to": { + "line": 106, + "column": 64 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "newTx" + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 8 + }, + "to": { + "line": 107, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 8 + }, + "to": { + "line": 107, + "column": 14 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 8 + }, + "to": { + "line": 107, + "column": 13 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "lastTx" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 18 + }, + "to": { + "line": 107, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "RECORD", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 20 + }, + "to": { + "line": 107, + "column": 21 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "id" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 27 + }, + "to": { + "line": 107, + "column": 27 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 30 + }, + "to": { + "line": 107, + "column": 32 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 38 + }, + "to": { + "line": 107, + "column": 43 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "None" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 46 + }, + "to": { + "line": 107, + "column": 49 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 107, + "column": 55 + }, + "to": { + "line": 107, + "column": 59 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": false + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 108, + "column": 8 + }, + "to": { + "line": 108, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 108, + "column": 8 + }, + "to": { + "line": 108, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 108, + "column": 8 + }, + "to": { + "line": 108, + "column": 15 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 108, + "column": 20 + }, + "to": { + "line": 108, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PLUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 108, + "column": 20 + }, + "to": { + "line": 108, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 108, + "column": 31 + }, + "to": { + "line": 108, + "column": 31 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 1 + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 109, + "column": 8 + }, + "to": { + "line": 109, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 109, + "column": 18 + }, + "to": { + "line": 109, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 109, + "column": 20 + }, + "to": { + "line": 109, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 109, + "column": 31 + }, + "to": { + "line": 109, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + } + ] + } + ] + } + ] + }, + "decls": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 103, + "column": 9 + }, + "to": { + "line": 104, + "column": 77 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "newTx", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 103, + "column": 18 + }, + "to": { + "line": 104, + "column": 77 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "RECORD", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 103, + "column": 20 + }, + "to": { + "line": 103, + "column": 21 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "id" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 103, + "column": 27 + }, + "to": { + "line": 103, + "column": 34 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 103, + "column": 37 + }, + "to": { + "line": 103, + "column": 39 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 103, + "column": 45 + }, + "to": { + "line": 103, + "column": 54 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "transfer" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 103, + "column": 57 + }, + "to": { + "line": 103, + "column": 60 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 103, + "column": 66 + }, + "to": { + "line": 103, + "column": 70 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": false + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 104, + "column": 20 + }, + "to": { + "line": 104, + "column": 25 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 104, + "column": 31 + }, + "to": { + "line": 104, + "column": 37 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_sender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 104, + "column": 40 + }, + "to": { + "line": 104, + "column": 45 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "toAddr" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 104, + "column": 51 + }, + "to": { + "line": 104, + "column": 57 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_toAddr" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 104, + "column": 60 + }, + "to": { + "line": 104, + "column": 64 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 104, + "column": 70 + }, + "to": { + "line": 104, + "column": 75 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_value" + } + ] + } + } + ] + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 114, + "column": 1 + }, + "to": { + "line": 131, + "column": 48 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "CommitTransfer", + "formalParams": [ + { + "kind": "OperParam", + "name": "_tx", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 115, + "column": 5 + }, + "to": { + "line": 131, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 115, + "column": 8 + }, + "to": { + "line": 115, + "column": 27 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 115, + "column": 8 + }, + "to": { + "line": 115, + "column": 14 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 115, + "column": 8 + }, + "to": { + "line": 115, + "column": 10 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 115, + "column": 12 + }, + "to": { + "line": 115, + "column": 14 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 115, + "column": 18 + }, + "to": { + "line": 115, + "column": 27 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "transfer" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 116, + "column": 8 + }, + "to": { + "line": 116, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 116, + "column": 8 + }, + "to": { + "line": 116, + "column": 27 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 116, + "column": 8 + }, + "to": { + "line": 116, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 116, + "column": 31 + }, + "to": { + "line": 116, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_MINUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 116, + "column": 31 + }, + "to": { + "line": 116, + "column": 49 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 116, + "column": 53 + }, + "to": { + "line": 116, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 116, + "column": 55 + }, + "to": { + "line": 116, + "column": 57 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 117, + "column": 9 + }, + "to": { + "line": 131, + "column": 48 + } + }, + "type": "Untyped", + "kind": "LetInEx", + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 9 + }, + "to": { + "line": 131, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 12 + }, + "to": { + "line": 122, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 12 + }, + "to": { + "line": 122, + "column": 18 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 12 + }, + "to": { + "line": 122, + "column": 17 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "lastTx" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 22 + }, + "to": { + "line": 122, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 24 + }, + "to": { + "line": 122, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 35 + }, + "to": { + "line": 122, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 37 + }, + "to": { + "line": 122, + "column": 40 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 44 + }, + "to": { + "line": 122, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 122, + "column": 44 + }, + "to": { + "line": 122, + "column": 47 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "fail" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 123, + "column": 12 + }, + "to": { + "line": 131, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "IF_THEN_ELSE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 123, + "column": 15 + }, + "to": { + "line": 123, + "column": 18 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 123, + "column": 15 + }, + "to": { + "line": 123, + "column": 18 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "fail" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 124, + "column": 16 + }, + "to": { + "line": 124, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 124, + "column": 26 + }, + "to": { + "line": 124, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 124, + "column": 28 + }, + "to": { + "line": 124, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 124, + "column": 39 + }, + "to": { + "line": 124, + "column": 47 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 124, + "column": 50 + }, + "to": { + "line": 124, + "column": 57 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 127, + "column": 13 + }, + "to": { + "line": 131, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 127, + "column": 16 + }, + "to": { + "line": 130, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 127, + "column": 16 + }, + "to": { + "line": 127, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 127, + "column": 16 + }, + "to": { + "line": 127, + "column": 24 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 127, + "column": 29 + }, + "to": { + "line": 130, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 18 + }, + "to": { + "line": 128, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 35 + }, + "to": { + "line": 128, + "column": 63 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 37 + }, + "to": { + "line": 128, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 37 + }, + "to": { + "line": 128, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 41 + }, + "to": { + "line": 128, + "column": 46 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 51 + }, + "to": { + "line": 128, + "column": 63 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "MINUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 35 + }, + "to": { + "line": 128, + "column": 63 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 18 + }, + "to": { + "line": 128, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 37 + }, + "to": { + "line": 128, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 37 + }, + "to": { + "line": 128, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 41 + }, + "to": { + "line": 128, + "column": 46 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 55 + }, + "to": { + "line": 128, + "column": 63 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 55 + }, + "to": { + "line": 128, + "column": 57 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 59 + }, + "to": { + "line": 128, + "column": 63 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 35 + }, + "to": { + "line": 129, + "column": 63 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 37 + }, + "to": { + "line": 129, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 37 + }, + "to": { + "line": 129, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 41 + }, + "to": { + "line": 129, + "column": 46 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "toAddr" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 51 + }, + "to": { + "line": 129, + "column": 63 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PLUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 35 + }, + "to": { + "line": 129, + "column": 63 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 128, + "column": 18 + }, + "to": { + "line": 128, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 37 + }, + "to": { + "line": 129, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 37 + }, + "to": { + "line": 129, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 41 + }, + "to": { + "line": 129, + "column": 46 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "toAddr" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 55 + }, + "to": { + "line": 129, + "column": 63 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 55 + }, + "to": { + "line": 129, + "column": 57 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 129, + "column": 59 + }, + "to": { + "line": 129, + "column": 63 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 131, + "column": 16 + }, + "to": { + "line": 131, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 131, + "column": 26 + }, + "to": { + "line": 131, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 131, + "column": 28 + }, + "to": { + "line": 131, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 131, + "column": 39 + }, + "to": { + "line": 131, + "column": 46 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + } + ] + } + ] + } + ] + } + ] + } + ] + }, + "decls": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 117, + "column": 13 + }, + "to": { + "line": 120, + "column": 36 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "fail", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 118, + "column": 11 + }, + "to": { + "line": 120, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 118, + "column": 14 + }, + "to": { + "line": 118, + "column": 26 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 118, + "column": 14 + }, + "to": { + "line": 118, + "column": 22 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 118, + "column": 14 + }, + "to": { + "line": 118, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 118, + "column": 18 + }, + "to": { + "line": 118, + "column": 22 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 118, + "column": 26 + }, + "to": { + "line": 118, + "column": 26 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 119, + "column": 14 + }, + "to": { + "line": 119, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 119, + "column": 14 + }, + "to": { + "line": 119, + "column": 22 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 119, + "column": 14 + }, + "to": { + "line": 119, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 119, + "column": 18 + }, + "to": { + "line": 119, + "column": 22 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 119, + "column": 26 + }, + "to": { + "line": 119, + "column": 46 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 119, + "column": 26 + }, + "to": { + "line": 119, + "column": 34 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 119, + "column": 36 + }, + "to": { + "line": 119, + "column": 45 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 119, + "column": 36 + }, + "to": { + "line": 119, + "column": 38 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 119, + "column": 40 + }, + "to": { + "line": 119, + "column": 45 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 120, + "column": 14 + }, + "to": { + "line": 120, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 120, + "column": 14 + }, + "to": { + "line": 120, + "column": 23 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 120, + "column": 14 + }, + "to": { + "line": 120, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 120, + "column": 18 + }, + "to": { + "line": 120, + "column": 23 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 120, + "column": 27 + }, + "to": { + "line": 120, + "column": 36 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 120, + "column": 27 + }, + "to": { + "line": 120, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 120, + "column": 31 + }, + "to": { + "line": 120, + "column": 36 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "toAddr" + } + } + ] + } + ] + } + ] + } + } + ] + } + ] + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 146, + "column": 1 + }, + "to": { + "line": 156, + "column": 41 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "SubmitTransferFrom", + "formalParams": [ + { + "kind": "OperParam", + "name": "_sender", + "arity": 0 + }, + { + "kind": "OperParam", + "name": "_fromAddr", + "arity": 0 + }, + { + "kind": "OperParam", + "name": "_toAddr", + "arity": 0 + }, + { + "kind": "OperParam", + "name": "_value", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 147, + "column": 5 + }, + "to": { + "line": 156, + "column": 41 + } + }, + "type": "Untyped", + "kind": "LetInEx", + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 153, + "column": 5 + }, + "to": { + "line": 156, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 153, + "column": 8 + }, + "to": { + "line": 153, + "column": 66 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 153, + "column": 8 + }, + "to": { + "line": 153, + "column": 27 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 153, + "column": 8 + }, + "to": { + "line": 153, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 153, + "column": 31 + }, + "to": { + "line": 153, + "column": 66 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_UNION2", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 153, + "column": 31 + }, + "to": { + "line": 153, + "column": 49 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 153, + "column": 58 + }, + "to": { + "line": 153, + "column": 66 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 153, + "column": 60 + }, + "to": { + "line": 153, + "column": 64 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 153, + "column": 60 + }, + "to": { + "line": 153, + "column": 64 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "newTx" + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 8 + }, + "to": { + "line": 154, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 8 + }, + "to": { + "line": 154, + "column": 14 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 8 + }, + "to": { + "line": 154, + "column": 13 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "lastTx" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 18 + }, + "to": { + "line": 154, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "RECORD", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 20 + }, + "to": { + "line": 154, + "column": 21 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "id" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 27 + }, + "to": { + "line": 154, + "column": 27 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 30 + }, + "to": { + "line": 154, + "column": 32 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 38 + }, + "to": { + "line": 154, + "column": 43 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "None" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 46 + }, + "to": { + "line": 154, + "column": 49 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 154, + "column": 55 + }, + "to": { + "line": 154, + "column": 59 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": false + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 155, + "column": 8 + }, + "to": { + "line": 155, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 155, + "column": 8 + }, + "to": { + "line": 155, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 155, + "column": 8 + }, + "to": { + "line": 155, + "column": 15 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 155, + "column": 20 + }, + "to": { + "line": 155, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PLUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 155, + "column": 20 + }, + "to": { + "line": 155, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 155, + "column": 31 + }, + "to": { + "line": 155, + "column": 31 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 1 + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 156, + "column": 8 + }, + "to": { + "line": 156, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 156, + "column": 18 + }, + "to": { + "line": 156, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 156, + "column": 20 + }, + "to": { + "line": 156, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 156, + "column": 31 + }, + "to": { + "line": 156, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + } + ] + } + ] + } + ] + }, + "decls": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 147, + "column": 9 + }, + "to": { + "line": 151, + "column": 9 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "newTx", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 147, + "column": 18 + }, + "to": { + "line": 151, + "column": 9 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "RECORD", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 148, + "column": 13 + }, + "to": { + "line": 148, + "column": 14 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "id" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 148, + "column": 20 + }, + "to": { + "line": 148, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 149, + "column": 13 + }, + "to": { + "line": 149, + "column": 15 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 149, + "column": 21 + }, + "to": { + "line": 149, + "column": 34 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "transferFrom" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 149, + "column": 37 + }, + "to": { + "line": 149, + "column": 40 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 149, + "column": 46 + }, + "to": { + "line": 149, + "column": 50 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": false + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 149, + "column": 53 + }, + "to": { + "line": 149, + "column": 58 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 149, + "column": 64 + }, + "to": { + "line": 149, + "column": 70 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_sender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 150, + "column": 13 + }, + "to": { + "line": 150, + "column": 20 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fromAddr" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 150, + "column": 26 + }, + "to": { + "line": 150, + "column": 34 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_fromAddr" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 150, + "column": 37 + }, + "to": { + "line": 150, + "column": 42 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "toAddr" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 150, + "column": 48 + }, + "to": { + "line": 150, + "column": 54 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_toAddr" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 150, + "column": 57 + }, + "to": { + "line": 150, + "column": 61 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 150, + "column": 67 + }, + "to": { + "line": 150, + "column": 72 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_value" + } + ] + } + } + ] + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 161, + "column": 1 + }, + "to": { + "line": 183, + "column": 33 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "CommitTransferFrom", + "formalParams": [ + { + "kind": "OperParam", + "name": "_tx", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 162, + "column": 5 + }, + "to": { + "line": 183, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 162, + "column": 8 + }, + "to": { + "line": 162, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 162, + "column": 8 + }, + "to": { + "line": 162, + "column": 14 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 162, + "column": 8 + }, + "to": { + "line": 162, + "column": 10 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 162, + "column": 12 + }, + "to": { + "line": 162, + "column": 14 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 162, + "column": 18 + }, + "to": { + "line": 162, + "column": 31 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "transferFrom" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 163, + "column": 8 + }, + "to": { + "line": 163, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 163, + "column": 8 + }, + "to": { + "line": 163, + "column": 27 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 163, + "column": 8 + }, + "to": { + "line": 163, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 163, + "column": 31 + }, + "to": { + "line": 163, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_MINUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 163, + "column": 31 + }, + "to": { + "line": 163, + "column": 49 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 163, + "column": 53 + }, + "to": { + "line": 163, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 163, + "column": 55 + }, + "to": { + "line": 163, + "column": 57 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 164, + "column": 9 + }, + "to": { + "line": 183, + "column": 33 + } + }, + "type": "Untyped", + "kind": "LetInEx", + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 9 + }, + "to": { + "line": 183, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 12 + }, + "to": { + "line": 170, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 12 + }, + "to": { + "line": 170, + "column": 18 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 12 + }, + "to": { + "line": 170, + "column": 17 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "lastTx" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 22 + }, + "to": { + "line": 170, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 24 + }, + "to": { + "line": 170, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 35 + }, + "to": { + "line": 170, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 37 + }, + "to": { + "line": 170, + "column": 40 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 44 + }, + "to": { + "line": 170, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 170, + "column": 44 + }, + "to": { + "line": 170, + "column": 47 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "fail" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 171, + "column": 13 + }, + "to": { + "line": 183, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "IF_THEN_ELSE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 171, + "column": 16 + }, + "to": { + "line": 171, + "column": 19 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 171, + "column": 16 + }, + "to": { + "line": 171, + "column": 19 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "fail" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 172, + "column": 18 + }, + "to": { + "line": 172, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 172, + "column": 28 + }, + "to": { + "line": 172, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 172, + "column": 30 + }, + "to": { + "line": 172, + "column": 38 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 172, + "column": 41 + }, + "to": { + "line": 172, + "column": 49 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 172, + "column": 52 + }, + "to": { + "line": 172, + "column": 59 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 175, + "column": 13 + }, + "to": { + "line": 183, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 175, + "column": 16 + }, + "to": { + "line": 178, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 175, + "column": 16 + }, + "to": { + "line": 175, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 175, + "column": 16 + }, + "to": { + "line": 175, + "column": 24 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 175, + "column": 29 + }, + "to": { + "line": 178, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 175, + "column": 31 + }, + "to": { + "line": 175, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 19 + }, + "to": { + "line": 176, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 21 + }, + "to": { + "line": 176, + "column": 32 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 21 + }, + "to": { + "line": 176, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 25 + }, + "to": { + "line": 176, + "column": 32 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fromAddr" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 37 + }, + "to": { + "line": 176, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "MINUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 19 + }, + "to": { + "line": 176, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 175, + "column": 31 + }, + "to": { + "line": 175, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 21 + }, + "to": { + "line": 176, + "column": 32 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 21 + }, + "to": { + "line": 176, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 25 + }, + "to": { + "line": 176, + "column": 32 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fromAddr" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 41 + }, + "to": { + "line": 176, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 41 + }, + "to": { + "line": 176, + "column": 43 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 176, + "column": 45 + }, + "to": { + "line": 176, + "column": 49 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 19 + }, + "to": { + "line": 177, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 21 + }, + "to": { + "line": 177, + "column": 30 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 21 + }, + "to": { + "line": 177, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 25 + }, + "to": { + "line": 177, + "column": 30 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "toAddr" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 35 + }, + "to": { + "line": 177, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PLUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 19 + }, + "to": { + "line": 177, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 175, + "column": 31 + }, + "to": { + "line": 175, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 21 + }, + "to": { + "line": 177, + "column": 30 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 21 + }, + "to": { + "line": 177, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 25 + }, + "to": { + "line": 177, + "column": 30 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "toAddr" + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 39 + }, + "to": { + "line": 177, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 39 + }, + "to": { + "line": 177, + "column": 41 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 177, + "column": 43 + }, + "to": { + "line": 177, + "column": 47 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 180, + "column": 16 + }, + "to": { + "line": 182, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 180, + "column": 16 + }, + "to": { + "line": 180, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 180, + "column": 16 + }, + "to": { + "line": 180, + "column": 24 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 180, + "column": 29 + }, + "to": { + "line": 182, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 180, + "column": 31 + }, + "to": { + "line": 180, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 19 + }, + "to": { + "line": 181, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 20 + }, + "to": { + "line": 181, + "column": 45 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 21 + }, + "to": { + "line": 181, + "column": 32 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 21 + }, + "to": { + "line": 181, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 25 + }, + "to": { + "line": 181, + "column": 32 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fromAddr" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 35 + }, + "to": { + "line": 181, + "column": 44 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 35 + }, + "to": { + "line": 181, + "column": 37 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 39 + }, + "to": { + "line": 181, + "column": 44 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 49 + }, + "to": { + "line": 181, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "MINUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 19 + }, + "to": { + "line": 181, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 180, + "column": 31 + }, + "to": { + "line": 180, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 20 + }, + "to": { + "line": 181, + "column": 45 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 21 + }, + "to": { + "line": 181, + "column": 32 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 21 + }, + "to": { + "line": 181, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 25 + }, + "to": { + "line": 181, + "column": 32 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fromAddr" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 35 + }, + "to": { + "line": 181, + "column": 44 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 35 + }, + "to": { + "line": 181, + "column": 37 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 39 + }, + "to": { + "line": 181, + "column": 44 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 53 + }, + "to": { + "line": 181, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 53 + }, + "to": { + "line": 181, + "column": 55 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 181, + "column": 57 + }, + "to": { + "line": 181, + "column": 61 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 183, + "column": 16 + }, + "to": { + "line": 183, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 183, + "column": 26 + }, + "to": { + "line": 183, + "column": 33 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + } + ] + } + ] + } + ] + } + ] + }, + "decls": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 164, + "column": 13 + }, + "to": { + "line": 168, + "column": 38 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "fail", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 165, + "column": 11 + }, + "to": { + "line": 168, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 165, + "column": 14 + }, + "to": { + "line": 165, + "column": 26 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 165, + "column": 14 + }, + "to": { + "line": 165, + "column": 22 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 165, + "column": 14 + }, + "to": { + "line": 165, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 165, + "column": 18 + }, + "to": { + "line": 165, + "column": 22 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 165, + "column": 26 + }, + "to": { + "line": 165, + "column": 26 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 166, + "column": 14 + }, + "to": { + "line": 166, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 166, + "column": 14 + }, + "to": { + "line": 166, + "column": 22 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 166, + "column": 14 + }, + "to": { + "line": 166, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 166, + "column": 18 + }, + "to": { + "line": 166, + "column": 22 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 166, + "column": 26 + }, + "to": { + "line": 166, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 166, + "column": 26 + }, + "to": { + "line": 166, + "column": 34 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 166, + "column": 36 + }, + "to": { + "line": 166, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 166, + "column": 36 + }, + "to": { + "line": 166, + "column": 38 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 166, + "column": 40 + }, + "to": { + "line": 166, + "column": 47 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fromAddr" + } + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 14 + }, + "to": { + "line": 167, + "column": 60 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "GT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 14 + }, + "to": { + "line": 167, + "column": 22 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 14 + }, + "to": { + "line": 167, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 18 + }, + "to": { + "line": 167, + "column": 22 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 26 + }, + "to": { + "line": 167, + "column": 60 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 26 + }, + "to": { + "line": 167, + "column": 34 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 26 + }, + "to": { + "line": 167, + "column": 60 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 36 + }, + "to": { + "line": 167, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 36 + }, + "to": { + "line": 167, + "column": 38 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 40 + }, + "to": { + "line": 167, + "column": 47 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fromAddr" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 50 + }, + "to": { + "line": 167, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 50 + }, + "to": { + "line": 167, + "column": 52 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 167, + "column": 54 + }, + "to": { + "line": 167, + "column": 59 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 168, + "column": 14 + }, + "to": { + "line": 168, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 168, + "column": 14 + }, + "to": { + "line": 168, + "column": 25 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 168, + "column": 14 + }, + "to": { + "line": 168, + "column": 16 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 168, + "column": 18 + }, + "to": { + "line": 168, + "column": 25 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fromAddr" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 168, + "column": 29 + }, + "to": { + "line": 168, + "column": 38 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 168, + "column": 29 + }, + "to": { + "line": 168, + "column": 31 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 168, + "column": 33 + }, + "to": { + "line": 168, + "column": 38 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "toAddr" + } + } + ] + } + ] + } + ] + } + } + ] + } + ] + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 190, + "column": 1 + }, + "to": { + "line": 200, + "column": 41 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "SubmitApprove", + "formalParams": [ + { + "kind": "OperParam", + "name": "_sender", + "arity": 0 + }, + { + "kind": "OperParam", + "name": "_spender", + "arity": 0 + }, + { + "kind": "OperParam", + "name": "_value", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 191, + "column": 5 + }, + "to": { + "line": 200, + "column": 41 + } + }, + "type": "Untyped", + "kind": "LetInEx", + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 197, + "column": 5 + }, + "to": { + "line": 200, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 197, + "column": 8 + }, + "to": { + "line": 197, + "column": 66 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 197, + "column": 8 + }, + "to": { + "line": 197, + "column": 27 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 197, + "column": 8 + }, + "to": { + "line": 197, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 197, + "column": 31 + }, + "to": { + "line": 197, + "column": 66 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_UNION2", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 197, + "column": 31 + }, + "to": { + "line": 197, + "column": 49 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 197, + "column": 58 + }, + "to": { + "line": 197, + "column": 66 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 197, + "column": 60 + }, + "to": { + "line": 197, + "column": 64 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 197, + "column": 60 + }, + "to": { + "line": 197, + "column": 64 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "newTx" + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 8 + }, + "to": { + "line": 198, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 8 + }, + "to": { + "line": 198, + "column": 14 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 8 + }, + "to": { + "line": 198, + "column": 13 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "lastTx" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 18 + }, + "to": { + "line": 198, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "RECORD", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 20 + }, + "to": { + "line": 198, + "column": 21 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "id" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 27 + }, + "to": { + "line": 198, + "column": 27 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 30 + }, + "to": { + "line": 198, + "column": 32 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 38 + }, + "to": { + "line": 198, + "column": 43 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "None" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 46 + }, + "to": { + "line": 198, + "column": 49 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 198, + "column": 55 + }, + "to": { + "line": 198, + "column": 59 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": false + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 199, + "column": 8 + }, + "to": { + "line": 199, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 199, + "column": 8 + }, + "to": { + "line": 199, + "column": 16 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 199, + "column": 8 + }, + "to": { + "line": 199, + "column": 15 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 199, + "column": 20 + }, + "to": { + "line": 199, + "column": 31 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PLUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 199, + "column": 20 + }, + "to": { + "line": 199, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 199, + "column": 31 + }, + "to": { + "line": 199, + "column": 31 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 1 + } + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 200, + "column": 8 + }, + "to": { + "line": 200, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 200, + "column": 18 + }, + "to": { + "line": 200, + "column": 41 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 200, + "column": 20 + }, + "to": { + "line": 200, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 200, + "column": 31 + }, + "to": { + "line": 200, + "column": 39 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + } + ] + } + ] + } + ] + }, + "decls": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 191, + "column": 9 + }, + "to": { + "line": 195, + "column": 9 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "newTx", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 191, + "column": 18 + }, + "to": { + "line": 195, + "column": 9 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "RECORD", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 192, + "column": 13 + }, + "to": { + "line": 192, + "column": 14 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "id" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 192, + "column": 20 + }, + "to": { + "line": 192, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 193, + "column": 13 + }, + "to": { + "line": 193, + "column": 15 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 193, + "column": 21 + }, + "to": { + "line": 193, + "column": 29 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "approve" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 193, + "column": 32 + }, + "to": { + "line": 193, + "column": 35 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 193, + "column": 41 + }, + "to": { + "line": 193, + "column": 45 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaBool", + "value": false + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 194, + "column": 13 + }, + "to": { + "line": 194, + "column": 18 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 194, + "column": 24 + }, + "to": { + "line": 194, + "column": 30 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_sender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 194, + "column": 33 + }, + "to": { + "line": 194, + "column": 39 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "spender" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 194, + "column": 45 + }, + "to": { + "line": 194, + "column": 52 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_spender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 194, + "column": 55 + }, + "to": { + "line": 194, + "column": 59 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 194, + "column": 65 + }, + "to": { + "line": 194, + "column": 70 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_value" + } + ] + } + } + ] + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 203, + "column": 1 + }, + "to": { + "line": 215, + "column": 75 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "CommitApprove", + "formalParams": [ + { + "kind": "OperParam", + "name": "_tx", + "arity": 0 + } + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 204, + "column": 5 + }, + "to": { + "line": 215, + "column": 75 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 204, + "column": 8 + }, + "to": { + "line": 204, + "column": 26 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 204, + "column": 8 + }, + "to": { + "line": 204, + "column": 14 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 204, + "column": 8 + }, + "to": { + "line": 204, + "column": 10 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 204, + "column": 12 + }, + "to": { + "line": 204, + "column": 14 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "tag" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 204, + "column": 18 + }, + "to": { + "line": 204, + "column": 26 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "approve" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 205, + "column": 8 + }, + "to": { + "line": 205, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 205, + "column": 8 + }, + "to": { + "line": 205, + "column": 27 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 205, + "column": 8 + }, + "to": { + "line": 205, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 205, + "column": 31 + }, + "to": { + "line": 205, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_MINUS", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 205, + "column": 31 + }, + "to": { + "line": 205, + "column": 49 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 205, + "column": 53 + }, + "to": { + "line": 205, + "column": 59 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "SET_ENUM", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 205, + "column": 55 + }, + "to": { + "line": 205, + "column": 57 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 206, + "column": 8 + }, + "to": { + "line": 206, + "column": 40 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 206, + "column": 18 + }, + "to": { + "line": 206, + "column": 40 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 206, + "column": 20 + }, + "to": { + "line": 206, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "balanceOf" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 206, + "column": 31 + }, + "to": { + "line": 206, + "column": 38 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "nextTxId" + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 9 + }, + "to": { + "line": 215, + "column": 75 + } + }, + "type": "Untyped", + "kind": "LetInEx", + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 9 + }, + "to": { + "line": 215, + "column": 75 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "AND", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 12 + }, + "to": { + "line": 208, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 12 + }, + "to": { + "line": 208, + "column": 18 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 12 + }, + "to": { + "line": 208, + "column": 17 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "lastTx" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 22 + }, + "to": { + "line": 208, + "column": 49 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 24 + }, + "to": { + "line": 208, + "column": 26 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 35 + }, + "to": { + "line": 208, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 37 + }, + "to": { + "line": 208, + "column": 40 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "fail" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 44 + }, + "to": { + "line": 208, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 208, + "column": 44 + }, + "to": { + "line": 208, + "column": 47 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "fail" + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 209, + "column": 13 + }, + "to": { + "line": 215, + "column": 75 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "IF_THEN_ELSE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 209, + "column": 16 + }, + "to": { + "line": 209, + "column": 19 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 209, + "column": 16 + }, + "to": { + "line": 209, + "column": 19 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "fail" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 211, + "column": 15 + }, + "to": { + "line": 211, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "UNCHANGED", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 211, + "column": 25 + }, + "to": { + "line": 211, + "column": 33 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 214, + "column": 15 + }, + "to": { + "line": 215, + "column": 75 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 214, + "column": 15 + }, + "to": { + "line": 214, + "column": 24 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "PRIME", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 214, + "column": 15 + }, + "to": { + "line": 214, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 17 + }, + "to": { + "line": 215, + "column": 75 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXCEPT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 19 + }, + "to": { + "line": 215, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "allowance" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 36 + }, + "to": { + "line": 215, + "column": 73 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 37 + }, + "to": { + "line": 215, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "TUPLE", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 38 + }, + "to": { + "line": 215, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 38 + }, + "to": { + "line": 215, + "column": 40 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 42 + }, + "to": { + "line": 215, + "column": 47 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 50 + }, + "to": { + "line": 215, + "column": 60 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 50 + }, + "to": { + "line": 215, + "column": 52 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 54 + }, + "to": { + "line": 215, + "column": 60 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "spender" + } + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 65 + }, + "to": { + "line": 215, + "column": 73 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 65 + }, + "to": { + "line": 215, + "column": 67 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 215, + "column": 69 + }, + "to": { + "line": 215, + "column": 73 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + } + ] + } + ] + } + ] + } + ] + }, + "decls": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 13 + }, + "to": { + "line": 207, + "column": 61 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "fail", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 21 + }, + "to": { + "line": 207, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 21 + }, + "to": { + "line": 207, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "LT", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 21 + }, + "to": { + "line": 207, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 21 + }, + "to": { + "line": 207, + "column": 23 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 25 + }, + "to": { + "line": 207, + "column": 29 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "value" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 33 + }, + "to": { + "line": 207, + "column": 33 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaInt", + "value": 0 + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 38 + }, + "to": { + "line": 207, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EQ", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 38 + }, + "to": { + "line": 207, + "column": 47 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 38 + }, + "to": { + "line": 207, + "column": 40 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 42 + }, + "to": { + "line": 207, + "column": 47 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "sender" + } + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 51 + }, + "to": { + "line": 207, + "column": 61 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "FUN_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 51 + }, + "to": { + "line": 207, + "column": 53 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "_tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 207, + "column": 55 + }, + "to": { + "line": 207, + "column": 61 + } + }, + "type": "Untyped", + "kind": "ValEx", + "value": { + "kind": "TlaStr", + "value": "spender" + } + } + ] + } + ] + } + ] + } + } + ] + } + ] + } + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 218, + "column": 1 + }, + "to": { + "line": 231, + "column": 28 + } + }, + "type": "Untyped", + "kind": "TlaOperDecl", + "name": "Next", + "formalParams": [ + + ], + "isRecursive": false, + "body": { + "source": { + "filename": "ERC20", + "from": { + "line": 219, + "column": 5 + }, + "to": { + "line": 231, + "column": 28 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 219, + "column": 8 + }, + "to": { + "line": 221, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 219, + "column": 8 + }, + "to": { + "line": 221, + "column": 48 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "sender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 219, + "column": 30 + }, + "to": { + "line": 219, + "column": 33 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 219, + "column": 8 + }, + "to": { + "line": 221, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 219, + "column": 8 + }, + "to": { + "line": 221, + "column": 48 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "toAddr" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 219, + "column": 30 + }, + "to": { + "line": 219, + "column": 33 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 220, + "column": 10 + }, + "to": { + "line": 221, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 220, + "column": 10 + }, + "to": { + "line": 221, + "column": 48 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "value" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 220, + "column": 23 + }, + "to": { + "line": 220, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "AMOUNTS" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 221, + "column": 12 + }, + "to": { + "line": 221, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 221, + "column": 12 + }, + "to": { + "line": 221, + "column": 48 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "SubmitTransfer" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 221, + "column": 27 + }, + "to": { + "line": 221, + "column": 32 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "sender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 221, + "column": 35 + }, + "to": { + "line": 221, + "column": 40 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "toAddr" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 221, + "column": 43 + }, + "to": { + "line": 221, + "column": 47 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "value" + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 222, + "column": 8 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 222, + "column": 8 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "sender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 222, + "column": 40 + }, + "to": { + "line": 222, + "column": 43 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 222, + "column": 8 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 222, + "column": 8 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "fromAddr" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 222, + "column": 40 + }, + "to": { + "line": 222, + "column": 43 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 222, + "column": 8 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 222, + "column": 8 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "toAddr" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 222, + "column": 40 + }, + "to": { + "line": 222, + "column": 43 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 223, + "column": 10 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 223, + "column": 10 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "value" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 223, + "column": 23 + }, + "to": { + "line": 223, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "AMOUNTS" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 224, + "column": 12 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 224, + "column": 12 + }, + "to": { + "line": 224, + "column": 62 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "SubmitTransferFrom" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 224, + "column": 31 + }, + "to": { + "line": 224, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "sender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 224, + "column": 39 + }, + "to": { + "line": 224, + "column": 46 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "fromAddr" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 224, + "column": 49 + }, + "to": { + "line": 224, + "column": 54 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "toAddr" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 224, + "column": 57 + }, + "to": { + "line": 224, + "column": 61 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "value" + } + ] + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 225, + "column": 8 + }, + "to": { + "line": 227, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 225, + "column": 8 + }, + "to": { + "line": 227, + "column": 48 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "sender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 225, + "column": 31 + }, + "to": { + "line": 225, + "column": 34 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 225, + "column": 8 + }, + "to": { + "line": 227, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 225, + "column": 8 + }, + "to": { + "line": 227, + "column": 48 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "spender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 225, + "column": 31 + }, + "to": { + "line": 225, + "column": 34 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "ADDR" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 226, + "column": 10 + }, + "to": { + "line": 227, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 226, + "column": 10 + }, + "to": { + "line": 227, + "column": 48 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "value" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 226, + "column": 23 + }, + "to": { + "line": 226, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "AMOUNTS" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 227, + "column": 12 + }, + "to": { + "line": 227, + "column": 48 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 227, + "column": 12 + }, + "to": { + "line": 227, + "column": 48 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "SubmitApprove" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 227, + "column": 26 + }, + "to": { + "line": 227, + "column": 31 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "sender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 227, + "column": 34 + }, + "to": { + "line": 227, + "column": 40 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "spender" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 227, + "column": 43 + }, + "to": { + "line": 227, + "column": 47 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "value" + } + ] + } + ] + } + ] + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 228, + "column": 8 + }, + "to": { + "line": 231, + "column": 28 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "EXISTS3", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 228, + "column": 8 + }, + "to": { + "line": 231, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tx" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 228, + "column": 18 + }, + "to": { + "line": 228, + "column": 36 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "pendingTransactions" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 229, + "column": 9 + }, + "to": { + "line": 231, + "column": 28 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OR", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 229, + "column": 12 + }, + "to": { + "line": 229, + "column": 29 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 229, + "column": 12 + }, + "to": { + "line": 229, + "column": 29 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "CommitTransfer" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 229, + "column": 27 + }, + "to": { + "line": 229, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tx" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 230, + "column": 12 + }, + "to": { + "line": 230, + "column": 33 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 230, + "column": 12 + }, + "to": { + "line": 230, + "column": 33 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "CommitTransferFrom" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 230, + "column": 31 + }, + "to": { + "line": 230, + "column": 32 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tx" + } + ] + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 231, + "column": 12 + }, + "to": { + "line": 231, + "column": 28 + } + }, + "type": "Untyped", + "kind": "OperEx", + "oper": "OPER_APP", + "args": [ + { + "source": { + "filename": "ERC20", + "from": { + "line": 231, + "column": 12 + }, + "to": { + "line": 231, + "column": 28 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "CommitApprove" + }, + { + "source": { + "filename": "ERC20", + "from": { + "line": 231, + "column": 26 + }, + "to": { + "line": 231, + "column": 27 + } + }, + "type": "Untyped", + "kind": "NameEx", + "name": "tx" + } + ] + } + ] + } + ] + } + ] + } + } + ] + } + ] +} \ No newline at end of file diff --git a/tla_specifications/ERC20/ERC20.tla b/tla_specifications/ERC20/ERC20.tla new file mode 100644 index 0000000..9ea292b --- /dev/null +++ b/tla_specifications/ERC20/ERC20.tla @@ -0,0 +1,325 @@ +----------------------------- MODULE ERC20 ------------------------------------ +(* + * Modeling ERC20 tokens of Ethereum and the Approve-TransferFrom Attack: + * + * EIP-20: https://eips.ethereum.org/EIPS/eip-20 + * + * Attack scenario: + * https://docs.google.com/document/d/1YLPtQxZu1UAvO9cZ1O2RPXBbT0mooh4DYKjA_jp-RLM/edit# + * + * This TLA+ specification is designed for model checking with Apalache. + * We do not model 256-bit integers here, as we are not interested in overflows. + * + * Igor Konnov, Informal Systems, 2021-2022 + *) + +(* + Type definitions for the module ERC20. + An account address, in our case, simply an uninterpreted type ADDR. + A transaction (a la discriminated union but all fields are packed together): + @typeAlias: TX = [ + tag: Str, + id: Int, + fail: Bool, + sender: ADDR, + spender: ADDR, + fromAddr: ADDR, + toAddr: ADDR, + value: Int + ]; + A state of the state machine: + @typeAlias: STATE = [ + balanceOf: ADDR -> Int, + allowance: <> -> Int, + pendingTransactions: Set(TX), + lastTx: TX, + nextTxId: Int + ]; + *) + +EXTENDS Integers, Apalache + +CONSTANTS + \* Set of all addresses. + \* + \* @type: Set(ADDR); + ADDR, + \* Set of the amounts to use. + \* + \* @type: Set(Int); + AMOUNTS + +VARIABLES + \* Token balance for every account. This is exactly as `balanceOf` in ERC20. + \* + \* @type: ADDR -> Int; + balanceOf, + \* Allowance to transfer tokens + \* from owner (1st element) by spender (2nd element). + \* This is exactly as `allowance` of ERC20. + \* + \* @type: <> -> Int; + allowance + +\* Variables that model Ethereum transactions, not the ERC20 state machine. +VARIABLES + \* Pending transactions to be executed against the contract. + \* Note that we have a set of transactions instead of a sequence, + \* as the order of transactions on Ethereum is not predefined. + \* To make it possible to submit two 'equal' transactions, + \* we introduce a unique transaction id. + \* + \* @type: Set(TX); + pendingTransactions, + \* The last executed transaction. + \* + \* @type: TX; + lastTx, + \* A serial number to assign unique ids to transactions + \* @type: Int; + nextTxId + +\* Initialize an ERC20 token. +Init == + /\ balanceOf = [a \in ADDR |-> 100] + \* no account is allowed to withdraw from another account + /\ allowance = [ pair \in ADDR \X ADDR |-> 0 ] + \* no pending transactions + /\ pendingTransactions = {} + /\ nextTxId = 0 + /\ lastTx = [ id |-> 0, tag |-> "None", fail |-> FALSE ] + +(* EIP-20: +The following action submits a transaction to the blockchain. + +Transfers _value amount of tokens to address _toAddr, and MUST fire the Transfer +event. The function SHOULD throw if the message caller’s account balance does +not have enough tokens to spend. + +Note Transfers of 0 values MUST be treated as normal transfers and fire the +Transfer event. +*) +SubmitTransfer(_sender, _toAddr, _value) == + LET newTx == [ id |-> nextTxId, tag |-> "transfer", fail |-> FALSE, + sender |-> _sender, toAddr |-> _toAddr, value |-> _value ] + IN + /\ pendingTransactions' = pendingTransactions \union { newTx } + /\ lastTx' = [ id |-> 0, tag |-> "None", fail |-> FALSE ] + /\ nextTxId' = nextTxId + 1 + /\ UNCHANGED <> + +(* + Process a Transfer transaction that was submitted with SubmitTransfer. + *) +CommitTransfer(_tx) == + /\ _tx.tag = "transfer" + /\ pendingTransactions' = pendingTransactions \ { _tx } + /\ LET fail == + \/ _tx.value < 0 + \/ _tx.value > balanceOf[_tx.sender] + \/ _tx.sender = _tx.toAddr + IN + /\ lastTx' = [ _tx EXCEPT !.fail = fail ] + /\ IF fail + THEN UNCHANGED <> + ELSE \* transaction succeeds + \* update the balances of the 'sender' and 'toAddr' addresses + /\ balanceOf' = [ + balanceOf EXCEPT ![_tx.sender] = @ - _tx.value, + ![_tx.toAddr] = @ + _tx.value + ] + /\ UNCHANGED <> + +(* EIP-20: +Transfers _value amount of tokens from address _fromAddr to address _toAddr, and +MUST fire the Transfer event. + +The transferFrom method is used for a withdraw workflow, allowing contracts to +transfer tokens on your behalf. This can be used for example to allow a +contract to transfer tokens on your behalf and/or to charge fees in +sub-currencies. The function SHOULD throw unless the _fromAddr account has +deliberately authorized the sender of the message via some mechanism. + +Note Transfers of 0 values MUST be treated as normal transfers and fire the +Transfer event. +*) +SubmitTransferFrom(_sender, _fromAddr, _toAddr, _value) == + LET newTx == [ + id |-> nextTxId, + tag |-> "transferFrom", fail |-> FALSE, sender |-> _sender, + fromAddr |-> _fromAddr, toAddr |-> _toAddr, value |-> _value + ] + IN + /\ pendingTransactions' = pendingTransactions \union { newTx } + /\ lastTx' = [ id |-> 0, tag |-> "None", fail |-> FALSE ] + /\ nextTxId' = nextTxId + 1 + /\ UNCHANGED <> + +(* + Process a TranferFrom transaction that was submitted with SubmitTransferFrom. + *) +CommitTransferFrom(_tx) == + /\ _tx.tag = "transferFrom" + /\ pendingTransactions' = pendingTransactions \ { _tx } + /\ LET fail == + \/ _tx.value < 0 + \/ _tx.value > balanceOf[_tx.fromAddr] + \/ _tx.value > allowance[_tx.fromAddr, _tx.sender] + \/ _tx.fromAddr = _tx.toAddr + IN + /\ lastTx' = [ _tx EXCEPT !.fail = fail ] + /\ IF fail + THEN UNCHANGED <> + ELSE \* transaction succeeds + \* update the balances of the 'fromAddr' and 'toAddr' addresses + /\ balanceOf' = [ balanceOf EXCEPT + ![_tx.fromAddr] = @ - _tx.value, + ![_tx.toAddr] = @ + _tx.value + ] + \* decrease the allowance for the sender + /\ allowance' = [ allowance EXCEPT + ![_tx.fromAddr, _tx.sender] = @ - _tx.value + ] + /\ UNCHANGED nextTxId + +(* EIP-20: +Allows _spender to withdraw from your account multiple times, up to the _value +amount. If this function is called again it overwrites the current allowance +with _value. +*) +SubmitApprove(_sender, _spender, _value) == + LET newTx == [ + id |-> nextTxId, + tag |-> "approve", fail |-> FALSE, + sender |-> _sender, spender |-> _spender, value |-> _value + ] + IN + /\ pendingTransactions' = pendingTransactions \union { newTx } + /\ lastTx' = [ id |-> 0, tag |-> "None", fail |-> FALSE ] + /\ nextTxId' = nextTxId + 1 + /\ UNCHANGED <> + +\* Process an Approve transaction that was submitted with SubmitApprove. +CommitApprove(_tx) == + /\ _tx.tag = "approve" + /\ pendingTransactions' = pendingTransactions \ { _tx } + /\ UNCHANGED <> + /\ LET fail == _tx.value < 0 \/ _tx.sender = _tx.spender IN + /\ lastTx' = [ _tx EXCEPT !.fail = fail ] + /\ IF fail + THEN \* transaction fails + UNCHANGED allowance + ELSE \* transaction succeeds + \* set the allowance for the pair <> to value + allowance' = + [ allowance EXCEPT ![_tx.sender, _tx.spender] = _tx.value ] + +\* The transition relation, which chooses one of the actions +Next == + \/ \E sender, toAddr \in ADDR: + \E value \in AMOUNTS: + SubmitTransfer(sender, toAddr, value) + \/ \E sender, fromAddr, toAddr \in ADDR: + \E value \in AMOUNTS: + SubmitTransferFrom(sender, fromAddr, toAddr, value) + \/ \E sender, spender \in ADDR: + \E value \in AMOUNTS: + SubmitApprove(sender, spender, value) + \/ \E tx \in pendingTransactions: + \/ CommitTransfer(tx) + \/ CommitTransferFrom(tx) + \/ CommitApprove(tx) + + +(* False invariants to debug the spec *) + +\* Claim that no `TransferFrom` transaction is ever processed. +\* This is false. Use this false invariant to see an example of how +\* `TransferFrom` is processed. +NoTransferFrom == + LET Example == + /\ ~lastTx.fail + /\ lastTx.tag = "transferFrom" + /\ lastTx.value > 0 + IN + ~Example + +\* Claim that no `Approve` transaction is ever processed. +\* This is false. Use this false invariant to see an example of how +\* `Approve` is processed. +NoApprove == + LET Example == + /\ ~lastTx.fail + /\ lastTx.tag = "approve" + /\ lastTx.value > 0 + IN + ~Example + +\* EXPECTED PROPERTIES + +\* No transferFrom should be possible, while there is a pending approval +\* for a smaller amount. This invariant is violated, as explained in: +\* +\* https://docs.google.com/document/d/1YLPtQxZu1UAvO9cZ1O2RPXBbT0mooh4DYKjA_jp-RLM/edit# +NoTransferFromWhileApproveInFlight == + LET BadExample == + /\ lastTx.tag = "transferFrom" + /\ lastTx.value > 0 + /\ ~lastTx.fail + /\ \E approval \in pendingTransactions: + /\ approval.tag = "approve" + /\ approval.sender = lastTx.fromAddr + /\ approval.spender = lastTx.sender + /\ lastTx.sender /= lastTx.toAddr + /\ approval.value < lastTx.value + /\ approval.value > 0 + IN + ~BadExample + +\* Make sure that the account balances never go negative. +NoNegativeBalances == + \A a \in ADDR: + balanceOf[a] >= 0 + +\* A trace invariant: For every pair <>, the sum of transfers +\* via TransferFrom is no greater than the maximum allowance. +\* It is quite hard to formulate this property, as there are scenarios, +\* where this behavior is actually expected. +\* In pure TLA+, we would have to write a temporal property. +\* In Apalache, we are just writing a trace invariant. +\* +\* @type: Seq(STATE) => Bool; +NoTransferAboveApproved(trace) == + \A spender, fromAddr \in ADDR: + LET TransferIndices == { + i \in DOMAIN trace: + LET tx == trace[i].lastTx IN + /\ tx.tag = "transferFrom" + /\ ~tx.fail + /\ tx.fromAddr = fromAddr + /\ tx.sender = spender + /\ tx.value > 0 + } + IN + \* the sum of all transfers from 'fromAddr' to 'toAddr' + LET sumTransfers == + LET Add(sum, i) == sum + trace[i].lastTx.value IN + ApaFoldSet(Add, 0, TransferIndices) + IN + \* there exists an approval for the whole transfer sum + LET existsApprovalForSumInPast == + \E i \in DOMAIN trace: + LET tx_i == trace[i].lastTx IN + \* all transfers are made after the approval + /\ \A j \in TransferIndices: j > i + /\ tx_i.tag = "approve" + /\ ~tx_i.fail + \* the sender of this transaction is allowing the spender + \* to spend at most the sum of the made transfers. + /\ tx_i.value >= sumTransfers + /\ spender = tx_i.spender + /\ fromAddr = tx_i.sender + IN + sumTransfers > 0 => existsApprovalForSumInPast + +=============================================================================== diff --git a/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-21_17911601904741265504/detailed.log b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-21_17911601904741265504/detailed.log new file mode 100644 index 0000000..1162266 --- /dev/null +++ b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-21_17911601904741265504/detailed.log @@ -0,0 +1,13 @@ +11:21:22.011 [main] INFO a.f.a.t.Tool$ - # APALACHE version: v0.20.3-1485-gb46aa9e76 | build: v0.20.3-1485-gb46aa9e76 +11:21:22.192 [main] INFO a.f.a.t.Tool$ - Parse ERC20.tla +11:21:22.195 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser +11:21:22.334 [main] ERROR a.f.a.t.Tool$ - Error by TLA+ parser: *** Abort messages: 1 + +Unknown location + +Cannot find source file for module ERC20_typedefs imported in module ERC20. + + + +11:21:22.335 [main] INFO a.f.a.t.Tool$ - It took me 0 days 0 hours 0 min 0 sec +11:21:22.335 [main] INFO a.f.a.t.Tool$ - Total time: 0.319 sec diff --git a/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-21_17911601904741265504/run.txt b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-21_17911601904741265504/run.txt new file mode 100644 index 0000000..056337f --- /dev/null +++ b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-21_17911601904741265504/run.txt @@ -0,0 +1 @@ + parse --output=ERC20.json ERC20.tla diff --git a/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-34_5532659583529748549/detailed.log b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-34_5532659583529748549/detailed.log new file mode 100644 index 0000000..cce2372 --- /dev/null +++ b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-34_5532659583529748549/detailed.log @@ -0,0 +1,8 @@ +11:21:34.854 [main] INFO a.f.a.t.Tool$ - # APALACHE version: v0.20.3-1485-gb46aa9e76 | build: v0.20.3-1485-gb46aa9e76 +11:21:34.967 [main] INFO a.f.a.t.Tool$ - Parse ERC20.tla +11:21:34.970 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser +11:21:35.331 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK] +11:21:35.331 [main] INFO a.f.a.t.Tool$ - Parsed successfully +Root module: ERC20 with 21 declarations. +11:21:35.331 [main] INFO a.f.a.t.Tool$ - It took me 0 days 0 hours 0 min 0 sec +11:21:35.332 [main] INFO a.f.a.t.Tool$ - Total time: 0.474 sec diff --git a/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-34_5532659583529748549/run.txt b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-34_5532659583529748549/run.txt new file mode 100644 index 0000000..056337f --- /dev/null +++ b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T11-21-34_5532659583529748549/run.txt @@ -0,0 +1 @@ + parse --output=ERC20.json ERC20.tla diff --git a/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-20-28_8051551923294457393/detailed.log b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-20-28_8051551923294457393/detailed.log new file mode 100644 index 0000000..9265fa3 --- /dev/null +++ b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-20-28_8051551923294457393/detailed.log @@ -0,0 +1,8 @@ +12:20:28.568 [main] INFO a.f.a.t.Tool$ - # APALACHE version: v0.20.3-1485-gb46aa9e76 | build: v0.20.3-1485-gb46aa9e76 +12:20:28.683 [main] INFO a.f.a.t.Tool$ - Parse ERC20.tla +12:20:28.686 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser +12:20:28.992 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK] +12:20:28.992 [main] INFO a.f.a.t.Tool$ - Parsed successfully +Root module: ERC20 with 16 declarations. +12:20:28.993 [main] INFO a.f.a.t.Tool$ - It took me 0 days 0 hours 0 min 0 sec +12:20:28.993 [main] INFO a.f.a.t.Tool$ - Total time: 0.421 sec diff --git a/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-20-28_8051551923294457393/run.txt b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-20-28_8051551923294457393/run.txt new file mode 100644 index 0000000..056337f --- /dev/null +++ b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-20-28_8051551923294457393/run.txt @@ -0,0 +1 @@ + parse --output=ERC20.json ERC20.tla diff --git a/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-27-27_7551923235785992484/detailed.log b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-27-27_7551923235785992484/detailed.log new file mode 100644 index 0000000..1ae3004 --- /dev/null +++ b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-27-27_7551923235785992484/detailed.log @@ -0,0 +1,8 @@ +12:27:27.790 [main] INFO a.f.a.t.Tool$ - # APALACHE version: v0.20.3-1485-gb46aa9e76 | build: v0.20.3-1485-gb46aa9e76 +12:27:27.904 [main] INFO a.f.a.t.Tool$ - Parse ERC20.tla +12:27:27.907 [main] INFO a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser +12:27:28.209 [main] DEBUG a.f.a.i.p.PassChainExecutor - PASS #0: SanyParser [OK] +12:27:28.209 [main] INFO a.f.a.t.Tool$ - Parsed successfully +Root module: ERC20 with 16 declarations. +12:27:28.210 [main] INFO a.f.a.t.Tool$ - It took me 0 days 0 hours 0 min 0 sec +12:27:28.210 [main] INFO a.f.a.t.Tool$ - Total time: 0.417 sec diff --git a/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-27-27_7551923235785992484/run.txt b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-27-27_7551923235785992484/run.txt new file mode 100644 index 0000000..056337f --- /dev/null +++ b/tla_specifications/ERC20/_apalache-out/ERC20.tla/2022-08-07T12-27-27_7551923235785992484/run.txt @@ -0,0 +1 @@ + parse --output=ERC20.json ERC20.tla diff --git a/tla_specifications/ERC20/config.json b/tla_specifications/ERC20/config.json new file mode 100644 index 0000000..1acb032 --- /dev/null +++ b/tla_specifications/ERC20/config.json @@ -0,0 +1,39 @@ +{ + "processes": [ + { + "process_id": "alice", + "actions": [ + "\\E toAddr \\in ADDR: \\E value \\in AMOUNTS : SubmitTransfer(\"alice_OF_ADDR\", toAddr, value)", + "\\E fromAddr \\in ADDR: \\E toAddr \\in ADDR: \\E value \\in AMOUNTS : SubmitTransferFrom(\"alice_OF_ADDR\", fromAddr, toAddr, value)", + "\\E spender \\in ADDR: \\E value \\in AMOUNTS : SubmitApprove(\"alice_OF_ADDR\", spender, value)" + ] + }, + { + "process_id": "bob", + "actions": [ + "\\E toAddr \\in ADDR: \\E value \\in AMOUNTS : SubmitTransfer(\"bob_OF_ADDR\", toAddr, value)", + "\\E fromAddr \\in ADDR: \\E toAddr \\in ADDR: \\E value \\in AMOUNTS : SubmitTransferFrom(\"bob_OF_ADDR\", fromAddr, toAddr, value)", + "\\E spender \\in ADDR: \\E value \\in AMOUNTS : SubmitApprove(\"bob_OF_ADDR\", spender, value)" + ] + }, + { + "process_id": "blockchain", + "actions": [ + "\\E tx \\in pendingTransactions: CommitTransfer(tx)", + "\\E tx \\in pendingTransactions: CommitTransferFrom(tx)", + "\\E tx \\in pendingTransactions: CommitApprove(tx)" + ] + } + ], + "shared_variables": ["pendingTransactions", "lastTx", "nextTxId"], + "constants": [ + { + "name": "ADDR", + "value": "{\"alice_OF_ADDR\", \"bob_OF_ADDR\"}" + }, + { + "name": "AMOUNTS", + "value": "{0, 100, 500}" + } + ] +}