pub struct VerifyState {
pub round: u8,
pub well_defined_already_verified: bool,
pub equality_can_use_known_forall: bool,
}
impl VerifyState {
pub fn new(round: u8, well_defined_already_verified: bool) -> Self {
VerifyState {
round,
well_defined_already_verified,
equality_can_use_known_forall: true,
}
}
pub fn is_final_round(&self) -> bool {
self.round >= 2
}
pub fn new_state_with_round_increased(&self) -> Self {
return Self {
round: self.round + 1,
well_defined_already_verified: self.well_defined_already_verified,
equality_can_use_known_forall: self.equality_can_use_known_forall,
};
}
pub fn make_state_with_req_ok_set_to_true(&self) -> Self {
return Self {
round: self.round,
well_defined_already_verified: true,
equality_can_use_known_forall: self.equality_can_use_known_forall,
};
}
pub fn is_round_0(&self) -> bool {
self.round == 0
}
pub fn make_final_round_state(&self) -> Self {
return Self {
round: 2,
well_defined_already_verified: self.well_defined_already_verified,
equality_can_use_known_forall: self.equality_can_use_known_forall,
};
}
pub fn new_with_final_round(well_defined_already_verified: bool) -> Self {
return Self::new(2, well_defined_already_verified);
}
pub fn without_known_forall_for_equality(&self) -> Self {
return Self {
round: self.round,
well_defined_already_verified: self.well_defined_already_verified,
equality_can_use_known_forall: false,
};
}
}