Hi,
I read a research paper 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:

contract MyBank {
mapping (address)==>uint) balances;
function Deposit() {
balances[msg.sender] += msg.value;
}|
function Withdraw(uint amount) {
if(balances[msg.sender] >=amount) {
msg.sender.send(amount);
balances[msg.sender] -= amount;
}
}
function Balance() constant returns(uint) {
return balances[msg.sender];
}

A quick response is really appreciated.

Zulfi.

 

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):

module MyBank
open Solidity
type state = f balances: mapping address uint; g
val store : state = fbalances = ref empty mapg
let deposit () : Eth unit =
update map store.balances msg.sender
(add (lookup store.balances msg.sender) msg.value)
let withdraw (amount:uint) : Eth unit =
if (ge (lookup store.balances msg.sender) amount) then
send msg.sender amount;
update map store.balances msg.sender
(sub (lookup store.balances msg.sender) amount)
let balance () : Eth uint =
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

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.