let add (x : {v : float | v < 0 }) (y : {v : float | v < 0 }) : { v : float | v >= 0} = x x + yy
For the function declaration typing rule, we need to:
1- Loop through all inputs and use vc_gen_substitute to get the truth conditions "x < 0" and "y < 0".
2- Apply vc_gen_substitue for the function return type to get "add >= 0"
3 - Process the function body to get " add = x x + y y"
4 - Create the verification conditions "not ((x < 0 and y < 0 and add = xx + yy ) -> (add >= 0))"
5 - Use z3_solve on verification condition to prove property
let add (x : {v : float | v < 0 }) (y : {v : float | v < 0 }) : { v : float | v >= 0} = x x + yy
For the function declaration typing rule, we need to: 1- Loop through all inputs and use vc_gen_substitute to get the truth conditions "x < 0" and "y < 0". 2- Apply vc_gen_substitue for the function return type to get "add >= 0" 3 - Process the function body to get " add = x x + y y" 4 - Create the verification conditions "not ((x < 0 and y < 0 and add = xx + yy ) -> (add >= 0))" 5 - Use z3_solve on verification condition to prove property