How to test the given code?

🗄️ Archive
1

Hi,
I read a research paper (Formal Verification of Smart Contracts) for verification and validation of solidity code. It uses F* (F-star). However, it has to convert the solidity code into F-star. I cant find the converter. Can some body please guide me how to manually test the code? Code is given below:

indent preformatted text by 4 spaces
1.	contract MyBank {
2.	mapping (address)==>uint) balances;
3.	function Deposit() {
4.	balances[msg.sender] += msg.value;
5.	}|
6.	function Withdraw(uint amount) {
7.	if(balances[msg.sender] >=amount) {
8.	msg.sender.send(amount);
9.	balances[msg.sender] -= amount;
10.	}
11.	}
12.	function Balance() constant returns(uint) {
13.	return balances[msg.sender];
14.	}

A quick response is really appreciated.

Zulfi.

2

Hi,
What I understand is that:
Initially balance is zero. Then store some value in the balance using msg.value : lets suppose 500. & in lets suppose Withdraw(700) it checks that balance is greater than amount so it sends the amount & deducts balance which seems fine. However a conversion of the code into F* is shown below (from research paper:
https://www.cs.umd.edu/~aseem/solidetherplas.pdf

1. module MyBank

2. open Solidity

3. type state = f balances: mapping address uint; g

4. val store : state = fbalances = ref empty mapg

5. let deposit () : Eth unit =

6. update map store.balances msg.sender

7. (add (lookup store.balances msg.sender) msg.value)

8. let withdraw (amount:uint) : Eth unit =

9. if (ge (lookup store.balances msg.sender) amount) then

10. send msg.sender amount;

11. update map store.balances msg.sender

12. (sub (lookup store.balances msg.sender) amount)

13. let balance () : Eth uint =

14. lookup store.balances msg.sender

and when its analyzed using F*, it gives following error:

Using the effect system of F?, we now show how to detect
some vulnerable patterns such as unchecked send results in
translated contracts. The base construction is a combined
exception and state monad (see [9] for details) with the
following signature:
EST (a:Type) = h0:heap // input heap
->send failed:bool // send failure flag
->Tot (option (a * heap) // result and new heap, or exception

  • bool) // new failure flag. Its : * bool

return (a:Type) (x:a) : EST a =
fun h0 b0->Some (x, h0), b0

bind (a:Type) (b:Type) (f:EST a) (g:a->EST b) : EST b =
fun h0 b0->
match f h0 b0 with
| None, b1->None, b1 // exception in f: no output heap
| Some (x, h1), b1->g x h1 b1 // run g, carry failure flag

Some body please guide me.

Zulfi.