Return the reason that a refinement/consistency/determinism check failed over GRPC

[seblund]

The main idea is to return the cause of a query non-error-failure over GRPC so that we can display the information to users in the GUI instead of printing it to the console.
This involves first changing the query.proto to include a cause message when a check fails and secondly to update the verification checks in the code to return causes when checks fail

Changing query proto

The current message:

message QueryResponse {
  Query query = 1;

  message RefinementResult {
    bool success = 1;
    repeated StateTuple relation = 2;
  }

  message ComponentResult { Component component = 1; }
  message ConsistencyResult { bool success = 1; }
  message DeterminismResult { bool success = 1; }

  oneof result {
    RefinementResult refinement = 3;
    ComponentResult component = 4;
    ConsistencyResult consistency = 5;
    DeterminismResult determinism = 6;
    string error = 7;
  }
}

Should become something like:

message QueryResponse {
  Query query = 1;

  message RefinementResult {
    message Success {
      repeated StateTuple relation = 1;
    }
    message Failure {
      string cause = 1;
    }
    oneof result {
      Success success = 1;
      Failure failure = 2;
    }
  }

  message ComponentResult { Component component = 1; }
  message ConsistencyResult {
    message Success {}
    message Failure {
      string cause = 1;
    }
    oneof result {
      Success success = 1;
      Failure failure = 2;
    }
  }
  message DeterminismResult { 
    message Success {}
    message Failure {
      string cause = 1;
    }
    oneof result {
      Success success = 1;
      Failure failure = 2;
    }
  }

  oneof result {
    RefinementResult refinement = 3;
    ComponentResult component = 4;
    ConsistencyResult consistency = 5;
    DeterminismResult determinism = 6;
    string error = 7;
  }
}

Changing verification checks

I propose introducing enums (or structs) for verification checks equivalent to the messages in the protos.
Fx. change the refinement check return type such that we can never return Ok(false) in the refinement check but instead must return an enum:

enum RefinementResult {
    Success(Vec<State>),
    Failure(String)
}

The failure should then contain much of what we already print in the code e.g. Failure(format!("Refinement check failed for Output {:?} from location pair {:?}", ...)) and Failure(format!("Refinement check because {:?} is not consistent", ...)).