Nodes declaration order in Contracts

[hbourbouh]

Hi Daniel,
It seems that the order of nodes is important for contracts, any node used by a contract should be declared before it in the lustre file.
Example:
`
node mod_real(x, y: real;)
returns( z: real );
(*@contract
guarantee abs_real(z) < abs_real(y);
*)
let
tel

node abs_real (x: real)
returns(y:real);
let
y= if x >= 0.0 then x
else -x;
tel
`
Kind2 error: unknown node or function "abs_real"
Source: parse

Is it possible to fix this in Kind2, or it's for implementation reasons we can not?

Thanks,
Hamza

[daniel-larraz]

Hi Hamza,

It is a technical limitation of the current implementation. We have plans to address this issue and other ones related to contracts in a future rewriting of that part of the code.

Best,
Daniel