jeannin / zelus Goto Github PK

The goal for this task is to extend base variables and base functions to be refinement variables and refinement functions where the refinement types expression is exp = True

Compiler refactoring task

mUtils.ml is a new file that will store the implementation for MARVeLus utility functions, such as printing data structures and the debug print interface.

This task consists of moving those definitions from z3refinement.ml to mUtils.ml. Make sure that the z3refinement.ml code still runs properly after the changes.

The following expression does not pass the compiler check
let add (x : {v:int |v>0} ) (y : {v:int|v>0} ) : { v:int | v >= x && v >= y} = let z = x + y in z

However, if int is replaced with a float it works:

let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in z

The issue is that MARVeLus has no type inference mechanism to determine the type of z, which then default to float. When assigning "z = x + y" in Z3, it implicitly creates a new float x and a new float y, which then breaks the system.

let x_abs x : {v : float | v >= 0} = if x < 0 then -x else x

For this example we want to check both options of the if statement and prove that either branch makes the return condition of the function true

VC: "not ( ((x < 0) -> (-x >= 0)) and ( not (x < 0) -> (x >= 0)) )"

Currently, MARVLus handles refinement and base variables differently. Base variables are simply added to the environment while typing rules are applied to refinement variables to verify their satisfiability.

This process can be generalized by treating base variables as trivially true refinement variables.

An implementation idea is to create a function a vc_gen_refinement_variable function that:

• has inputs variable_name, base_type, refinement_expression and rhs_expression
• applies the typing rule for refinement variables (current MARVLus implementation)

For base variables a "True" expression is passed as the refinement_expression variable

(* let x0 : int = 3 *)

This does not compile correctly, code create a Z3 null type and cannot be used.

Past prototyping used create_z3_var when the type was unknown and this caused many variables to be assumed "float" type. This is the source of many z3(type error) exceptions.

We should replace all the occurrences of create_z3_var with create_z3_var_typed or any other function that will give the correct type to a z3 variable.

For an example, see the create_base_var_from_pattern function that uses pattern matching in a Zelus pattern construct to figure out base type and variable name.

let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in z
let f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add 1. y

After proof, the add constraint is only added to add's local environment and cannot be used in the proof for f6

When translating refinement_variable_test.zls to refinement_variable_test.ml, the custom refinement type type nat = {v : int | v >= 0} gets translated to be type nat = , which causes error.

Issue description:

let add ( x : int{x > 0} ) ( y : int{y > 0} ) : int{ add_return >= x && add_return >= y} = x + y
let f2 ( x : int{x < 0} ) : int{ f2_return > 0} = add (x * x) (x * x)

fails with the following message: this is a combinatorial expression and is expected to be static

Action:

Understand why is it failing and fix the issue.

Similar to the refinement and base variables issue described in #22 , MARVLus handles refinement and base functions differently. There is no special handling for base functions while typing rules are applied to refinement functions to verify their satisfiability at declaration and at use.

This process can be generalized by treating base functions as having a trivially true refinement output type.

An implementation idea is to create a function a vc_gen_refinement_fun function that:

• has inputs function_name, kind, is_atomic, argument_list, function_body, function_location and return_refinement_type
• applies the typing rule for refinement functions (current MARVLus implementation)

For base functions, a "True" expression is passed as the return_refinement_type input variable

Unhandled cases on 'prove_function' make it return '42', which was a magic number used to track errors. Make sure to replace this with exceptions that throw meaningful messages.

Goal: Add a keyword for temporal logic operators (box, diamond) that will take an expression as input, them translate it to Z3 expression.

The refinement types branch has currently no support for such keywords. This could be implemented by adding new keywords "box" and "diamond" that will take one expression as input. The compiler will translate the input into a Z3 expression and apply the logical steps required by the operator.

An example of such refinement type annotation is written below:

let rec (a, b) = body : btype {box(expression)} in output

Multi-step task
[Easier task] - Add new keywords 'box' and 'diamond' to the parser
[Harder task] - Implement Z3 translation of temporal logic operators

e.g.

let x = -1 in let x:int{x<0} = 2 in x

Which x is int{x<0} referring to?

Use the type constraint/type expression pattern (from functions) anywhere other variables can be declared

Since we have parsed the new syntax and carried it to the verifying stage, we should call Z3 substitution function in the correct place to replace the alias variable with the real variable

Compiler refactoring task

mDefs.ml is a new file that will store data structures definition, including custom types, environment, function environment, type environment.

This task consists of moving those definitions from z3refinement.ml to mDefs.ml. Make sure that the z3refinement.ml code still runs properly after the changes.

The current implementation does not support custom refinement types to be declared beforehand / have an alias to identify that custom data type.

1- Adding the pattern below to the Zelus parser
type type_name = { reference_variable : base_type | Phi(reference_variable ) }
i.e type nat = {v : int | v > = 0}, which defines all natural numbers

[Easier task] - Add the custom data type definition to the parser

let add (x : {v:float|v>0} ) (y : {v:float|v>0} ) : { v:float | v >= x && v >= y} = let z = x +. y in z

let f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add y y

The previous code does not type checks, with the following error:

File "refinement_function_test.zls", line 59, characters 5-6:
add y y
^
Type error: this is a combinatorial expression and is expected to be static.

It seems that the first y argument is causing trouble because the following passes the type check
let f6 (x : {v : float | v < 0 }) : {v : float | v > 0} = let y = x *. x in add 1. y

The current implementation does not have an environment to hold custom data types defined in MARVLus.

Goal: Create a custom data type environment to hold the custom data type

The environment will be a map [string, custom type data structure], where "string" will be the custom data type alias, and the custom data type structure will be defined as below,

custom_t {
string base_type;
string reference_variable;
z3_expression Phi(reference_variable);
}

[Harder task] - Create a custom data type data structure and an environment to hold these data structures

The custom refinement data types uses an alias to reference the type variable itself.
e.g:
type nat = {v : int | v > = 0} , in this example v is the alias used for the type variable.

This task aims to implement the vc_gen_substitute function that will take a inputs a variable and perform a Z3 substitution.

e.g:
type nat = {v : int | v > = 0} let y : nat = 4
vc_gen_substitute(y) would looks for v >= 0 in nat definition and replace v with the variable y by using the Z3 Ocaml API.

The verification condition for the above example would be:
y = 4 -> y >= 0

Reference:

Look for substitute function in https://z3prover.github.io/api/html/ml/Z3.Expr.html

Test file to run after compiler changes and verify all steps are working

Issue description:

let pi = 3.14159
let y0 : int{ -y0 >= pi} = 4.0

Will compile successfully because (-y0) is interpreted as "42". The dummy value we use when there is no handling.

Action:
Implement operator and function application checks inside refinement variable declaration.

renaming this to see if it goes back to task board

The acc.zls file generates the following lines in the output of compilation:

[DEBUG] : return definition: (= vxf |42.0|)
[DEBUG] : exception ignored: AstTranslationNotImplemented vc_gen_expression: Etuple
[DEBUG] : Eseq : (e1 = |42.0| e2 = |42.0|)

[DEBUG] : Body exp :|42.0|

Where 42.0 is an undesired magic number in the code. This problem can cause issues in the verification conditions, since it adds an additional unrealistic constraint. Issue needs more investigation.

Change refinement type expressions from let x:int{x>0}=1 to let x:{int z | z>0} = 1

| Erefinementdecl of name * name * exp * exp * is_static
| Econstdecl of name * is_static * exp

For now, we store non-refinement variable declaration like let var : type = exp as trivially true refinement variable in Erefinementdecl, but for declaration without type annotation (like let var = exp), we are still storing it in Econstdecl.

We hope to finally use a pattern called Econstdecl (which has the same name as the original one but with some modifications on inner data structure) to store all variable declarations

The let rec keyword is parsed to a list of equation expressions. However, the equation handler equation_desc on zparser.mly has no support for refinement types and the following example does not compile:

let rec (a, b) : btype {box(expression)} = body in output

For reference, take a look at the simple_type and type_expression implementation for refinement types on zparser.mly. We need to add a similar pattern match construct for equations.

[Easier task] - Add a pattern match for refinement types on the parse equation handler. This will enable refinement type annotation for let rec expressions.

Old syntax of defining refinement type in function:
let add (x : int{x > 0}) (y : int{y > 0}) : int{add_return > 0} = x+y
New syntax should be:
let add (x : {v : int | v > 0}) (y : {v : int | v > 0}) : {v : int | v > 0} = x+y

Instead of using the variable name directly in the refinement expression, we use an alias (e.g. v here) to refer to it.
So the parsing stage should carry additional information: the name of alias, to the verifying stage (in z3refinement.ml)

Looks like we need to fetch everything up to inria/zelus:2.2, which is up to commit 56febdf

Compiler refactoring task

mVcGen.ml is a new file that will store the implementation for verification condition generation.

This task consists o implementing an interface that translates from Zelus AST to MARVeLus AST. The problem definition is described below:

• Given a Zelus AST, build a new AST containing Z3 objects, inferred statements, and verification conditions to check.

AST ----mVcGen.ml----> AST

Where:
Zelus {
Zelus data structures
}

MARVeLus {
Zelus data structures
Premises
Verification condition
}

function templates for vc_gen:

let vc_gen_[structure name] ctx env typenv funenv [structure object]: MARVeLus =
(*
comment defining function interface (inputs + outputs)
comment defining function computation
follow ocamldocs guidelines: https://v2.ocaml.org/manual/ocamldoc.html#s%3Aocamldoc-comments
*)
body pattern matching
| ->
...

let add (x : {v : float | v < 0 }) (y : {v : float | v < 0 }) : { v : float | v >= 0} = x * x + y*y

Once the function is called, for example,
let s = add 1 (-.3)

We want to verify that "not ( (x = 1 and y = -3) -> (x < 0 and y < 0))"

In this example, the check should fail since 1 !< 0.

Compiler refactoring task

mCheck.ml is a new file that will traverse through the MARVeLus AST and solve for the verification conditions.

The problem definition is described below:

• Given a MARVeLus AST, traverse the tree and check the verification conditions, return true if all conditions are met, and false otherwise.

AST ----mCheck.ml----> bool

• Side effects: print to the terminal when intermediate checks fail, and add checked conditions to the environment

function templates for vc_check:

let vc_check_[structure name] ctx env typenv funenv [structure object]: bool =
(*
comment defining function interface (inputs + outputs)
comment defining function computation
follow ocamldocs guidelines: https://v2.ocaml.org/manual/ocamldoc.html#s%3Aocamldoc-comments
*)
body pattern matching
| ->
...

Also investigate how to write refinement types for each element

• using fst, snd keywords
• using name types, i.e let (x : {v : int | v > 100}, y : nat)

Formally verifying a robot program often requires a model of the hardware and its connections to its environment. However, such models are no longer necessary when compiling code for execution on real hardware. We therefore need a way to distinguish places in code that are modeled for verification purposes, but will receive real data from physical sensors when executing on actual hardware.

To minimize impact on the other compiler components, the proposed solution is as follows:

• Introduce a new construct, modeled(x, y) where x is the model of a sensor and y is the actual implementation. For instance, x could be the kinematic model of a robot that simulates the position of an actuator, while y is the driver code necessary for obtaining the actual value from the robot's sensors.
• To the verifier, modeled(x, y) is equivalent to x (y is ignored)
• When in --robot mode, modeled(x, y) gets compiled to y in the executable.

Currently, the refinement type implementation is hardcoded for variables and functions. The goal is to be able to add the refinement type annotation everywhere a basic type can be defined.

| Efundecl of name * funexp
| Erefinementfundecl of name * funexp * exp

For now we store both refinement and non-refinement function in Erefinementfundecl which has one more field than Efundecl.

We hope to finally utilize a pattern called Efundecl (which is the original name for function pattern) to hold all functions with as little modification as possible than the original data structure.

Examples without functions work. For example,
type nat = {x : int | x >= 0} let x : nat = 10

Examples with functions are not working due to some clash with Zelus' typing system. Example that doesn't work:
type nat = {x : int | x >= 0} let node main () = let (x : nat) = 1 in x
Error output: "Type error: this expression has type int, but is expected to have type nat.

This example raises an error as expected:

let node sim () =
    let rec (x:{v:float | v > 0.}) = (-5.) fby (-5.) in x

This example does not:

let node sim () =
    let rec (x:{v:float | v > 0.}) = (-5.) in x

Instead, a constraint is added that sets x to 42., which is positive and thus passes the check.

let add (x : {v : float | v < 0 }) (y : {v : float | v < 0 }) : { v : float | v >= 0} = x * x + y*y

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

Old syntax of declaring refinement variables:
let x : int{x > 0} = 1
New syntax should be:
let x : {v : int | v>0} = 1

Instead of using the variable name directly in the refinement expression, we use an alias (e.g. v here) to refer to it.
So the parsing stage should carry additional information: the name of alias, to the verifying stage (in z3refinement.ml)