Contract parameters and support for dimensions on parameters and variables.

[NicolasRouquette]

Summary:

1. Add support for parameters, e.g.:

instead of writing this:

def fuel_tank(epsilon_tank:float,m_dot_in:float,m_dot_out:float,c_f:float,):
    ft = PolyhedralIoContract.from_strings(
        input_vars=["T_out","q_w"],
        output_vars=["T_in"],
        assumptions=[],
        guarantees=[f"-{epsilon_tank} <= {m_dot_out*c_f} * T_out - {m_dot_in*c_f}*T_in - q_w <= {epsilon_tank}"]
    )
    return ft

we would like to write this:

def fuel_tank():
    ft = PolyhedralIoContract.from_strings(
        input_vars=["T_out","q_w"],
        output_vars=["T_in"],
        parameters=["epsilon_tank", "m_dot_in", "m_dot_out", "c_f"]
        assumptions=[],
        guarantees=["-epsilon_tank <= m_dot_out*c_f*T_out - m_dot_in*c_f*T_in - q_w <= epsilon_tank"]
    )
    return ft

The requirement is that the constraints must be linear w.r.t the variables but may be polynomial w.r.t the parameters as in the example above.

There should be an operation for binding parameter values that, given a contract (w/ zero or more parameters) and a binding of parameter/values, produces a contract where all parameters are bound to values and the occurrence of parameters in assumptions/constraints have been replaced with their values.

The contract algebra operations (compose, quotient, merge, refine) require that the contracts have bound parameters.

Finally, we need support for tracking a dimension unit for contract variables and parameters. This would be used to perform additional well-formedness verification on all assumption/guarantee constraints, specifically, that the dimensional counterpart yields a consistent dimensional equation.

Discussed in #235

^{Originally posted by NicolasRouquette March 5, 2023}
In the space mission case study, I defined several functions to generate contracts using specific values of constant parameters, e.g:

# Parameters:
# - s: index of the timeline variables
# - generation: (min, max) rate of battery charge during the task instance
def CHARGING_power(s: int, generation: tuple[float, float]) -> PolyhedralContract:
  spec = PolyhedralContract.from_string(
    input_vars = [
      f"soc{s}_entry",          # initial battery SOC
      f"duration_charging{s}",  # variable task duration
    ],
    output_vars = [
      f"soc{s}_exit",           # final battery SOC
    ],
    assumptions = [
      # Task has a positive scheduled duration
      f"-duration_charging{s} <= 0",

      # Battery SOC must be positive
      f"-soc{s}_entry <= 0",
    ],
    guarantees = [
      # duration*generation(min) <= soc{exit} - soc{entry} <= duration*generation(max)
      f" soc{s}_exit - soc{s}_entry - {generation[1]}*duration_charging{s} <= 0",
      f"-soc{s}_exit + soc{s}_entry + {generation[0]}*duration_charging{s} <= 0",

      # Battery cannot exceed maximum SOC
      f"soc{s}_exit <= 100.0",
      
      # Battery should not completely discharge
      f"-soc{s}_exit <= 0",
    ])
  return spec

These function arguments define contract hyperparameters that would be useful for generating contracts using statistical sampling techniques to vary how many distinct instances of this contract to compose (i.e. the s argument) and the generation range for each instance.