Skip to content

Commit

Permalink
Update binaries, manual, examples.
Browse files Browse the repository at this point in the history
  • Loading branch information
Vilhelm Sjöberg committed Oct 21, 2020
1 parent 468cec1 commit 2701cd5
Show file tree
Hide file tree
Showing 6 changed files with 28 additions and 22 deletions.
Binary file modified DeepSEA language reference.pdf
Binary file not shown.
Binary file modified binaries/MacOS/dsc
Binary file not shown.
Binary file modified binaries/MacOS/dsc_antchain
Binary file not shown.
Binary file modified binaries/linux/dsc
Binary file not shown.
Binary file modified binaries/linux/dsc_antchain
Binary file not shown.
50 changes: 28 additions & 22 deletions contracts/token/token.ds
Original file line number Diff line number Diff line change
Expand Up @@ -2,29 +2,26 @@

external [[except DataTypeOps]] with "Require token.Invariant.\n"


(* Todo: we should support addresses (160-bit integers) as a builtin type. *)
type addr := uint

const _totalSupply = 100000

object signature ERC20Interface = {
initialize : unit -> uint;
constructor : unit -> unit;
const totalSupply : unit -> int;
const balanceOf : addr -> int;
transfer : addr * int -> bool
const balanceOf : address -> int;
transfer : address * int -> bool;
approve : address * int -> bool;
transferFrom : address * address * int -> bool
}

object FixedSupplyToken : ERC20Interface {
let balances : mapping[addr] int := mapping_init
let balances : mapping[address] int := mapping_init
let allowances : mapping[address] mapping[address] int := mapping_init

(* This is just a hack, we should fix it so that we can actually compile constructors correctly. *)
let initialize () =
balances[msg_sender] := 100000;
0u0
let constructor () =
balances[msg_sender] := 100000

let totalSupply () =
let bal0 = balances[0u0] in
let bal0 = balances[address(0)] in
_totalSupply - bal0

let balanceOf tokenOwner =
Expand All @@ -35,15 +32,24 @@ object FixedSupplyToken : ERC20Interface {
let fromA = msg_sender in
let from_bal = balances[fromA] in
let to_bal = balances[toA] in
if (fromA <> toA /\ from_bal >= tokens)
then begin
balances[fromA] := from_bal-tokens;
balances[toA] := to_bal+tokens;
true
end else
false

(* Todo: the approve() and transferFrom() methods. (Requires hashmappings with two keys.) *)
assert (fromA <> toA /\ from_bal >= tokens);
balances[fromA] := from_bal-tokens;
balances[toA] := to_bal+tokens;
true

let approve (spender, tokens) =
allowances[msg_sender][spender] := tokens;
true

let transferFrom (fromA, toA, tokens) =
let from_bal = balances[fromA] in
let to_bal = balances[toA] in
let allowed = allowances[fromA][toA] in
assert (fromA <> toA /\ from_bal >= tokens /\ allowed >= tokens);
balances[fromA] := from_bal-tokens;
balances[toA] := to_bal+tokens;
true

}

layer signature FIXEDSUPPLYTOKENSig = {
Expand Down

0 comments on commit 2701cd5

Please sign in to comment.