Note on acceptable structure of contracts to Gear

[abadithela]

This note documents the discussion on carefully checking the set of assumptions and guaranteers of a contract if we expect gear to give a non-trivial output

The relevant examples for this discussion are in the confmatrix branch: simple_car_ped.json and simple_car_ped_trivial.json.

In particular, simple_car_ped_trivial.json illustrates a typical input that we might expect from a user. The guarantees of contract 2 in simple_car_ped_trivial.json is the following:

• $P - 5p = 4$
• $0.99 \leq P \leq1$

while the guarantees of contract 2 in simple_car_ped.json is just $P - 5p = 4$. The extra guarantee on the bounds of $P$ in the trivial version ensures that the second contract guarantees more towards the top-level contract, and therefore the resulting quotient will have to guarantee less:

Contract1:
InVars: {<Var x_e>}
OutVars:{<Var P>}
A: -1*x_e <= -1, 1*x_e <= 1
G: -1*P <= -0.99, 1*P <= 1.0
Contract2:
InVars: {<Var p>}
OutVars:{<Var P>}
A: 1*p <= 1, -1*p <= 0
G: -1*P + 5*p <= 4.0, -1*P <= -0.99, 1*P + -5*p <= -4.0
Contract quotient:
InVars: {<Var x_e>}
OutVars:{<Var p>}
A: -1*x_e <= -1, 1*x_e <= 1
G: 5.00000000000000*p <= 5.00000000000000, -1*p <= 0

As we see above, the quotient contract does not return useful bounds on $p$ except that it is between 0 and 1, which is already known to the user. In contrast, if the quotient from simple_car_ped.json gives us the desired answer:

Contract1:
InVars: {<Var x_e>}
OutVars:{<Var P>}
A: -1*x_e <= -1, 1*x_e <= 1
G: 1*P <= 1.0, -1*P <= -0.99
Contract2:
InVars: {<Var p>}
OutVars:{<Var P>}
A: 1*p <= 1, -1*p <= 0
G: 5*p + -1*P <= 4, -5*p + 1*P <= -4
Contract quotient:
InVars: {<Var x_e>}
OutVars:{<Var p>}
A: -1*x_e <= -1, 1*x_e <= 1
G: 5*p <= 5.00000000000000, -5*p <= -4.99000000000000

This shows that Gear does not check for consistency between the different guarantees provided by a contract; it just assumes that the guarantees will hold. Therefore, by removing the extra bounding constraint, we get the desired non-trivial answer. In both cases, Gear worked correctly. However, this illustrates the importance of conveying to the user how to (and how not to) construct the contract to correctly represent their components functions.

[iincer]

I agree: while the results are a bit surprising, the tool is working as expected in both cases. Your considerations should be part of a methodology section in the documentation. Regarding the first example, since C2 promises what the top-level requires, the quotient does not have to guarantee much. In the second example, the quotient has to put more constraints on $p$ to make sure the top-level guarantees are met.

I am a bit confused by this comment: This shows that Gear does not check for consistency between the different guarantees provided by a contract. Where would things have gone differently had a consistency check been in place?