litex-lang 0.9.82-beta

A simple formal proof language and verifier, learnable in 2 hours
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22

use crate::prelude::*;
use std::result::Result;

impl Runtime {
    pub fn verify_not_forall_fact(
        &mut self,
        not_forall: &NotForallFact,
        verify_state: &VerifyState,
    ) -> Result<StmtResult, RuntimeError> {
        if !verify_state.well_defined_already_verified {
            self.verify_not_forall_fact_well_defined(not_forall, verify_state)?;
        }

        if let Some(cached_result) =
            self.verify_fact_from_cache_using_display_string(&not_forall.clone().into())
        {
            return Ok(cached_result);
        }

        Ok(StmtUnknown::new().into())
    }
}