Skip to main content

check_negative_control

lean_agent_core::accept

Function check_negative_control 

Source 
pub fn check_negative_control(control: Option<&NegativeControl>) -> GuardStatus
Expand description

Guard 4. Compile the formal negation of the claim and require it to fail; if both the claim and its negation pass, the claim is vacuous and is rejected.

TODO(loop-phase): this needs the claim manifest (the negation source and name) that the loop has not produced yet. Until a NegativeControl is supplied the guard is a documented no-op so guards 1-3 stay live on their own.