How to Manually Test Solidity Code Converted into F-star?

[zak100]

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 can't 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.

 

[jedishrfu]

I don’t know if this will help but when doing java code we can setup junit tests to exercise the code. This is a somewhat manual process best done with an IDE like Netbeans or Eclipse. Junit is a framework for writing th testcases. It doesn’t read your code and write them.

I imagine whatever you’re referring to does the same thing. You have to look at your code and write inputs that exercise the conditional and looping logic and then compare actual output to expected output.

 

[zak100]

Hi,
Thanks for your reply.

Hi,
What I understand is that:
Initially balance is zero. Then store some value in the balance using msg.value : let's suppose 500. & let's suppose in 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.