1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
//! Data model for `.formal` algebraic-law specification files.
/// A parsed machine-readable algebraic-law specification.
#[derive(Debug, Clone, Eq, PartialEq, serde::Deserialize)]
pub struct FormalLawSpec {
/// Schema version for forward-compatible parsing.
pub schema_version: u16,
/// Canonical law name from `LAW_CATALOG`.
pub law: String,
/// Rust enum variant name.
pub variant: String,
/// Human-readable mathematical claim.
pub natural_language: String,
/// Parser-friendly mathematical statement.
pub mathematical_statement: String,
/// Free variables quantified by the statement.
#[serde(default)]
pub variables: Vec<FormalVariable>,
/// Symbolic parameters supplied by the enum payload.
#[serde(default)]
pub parameters: Vec<FormalParameter>,
/// Preconditions required before the postcondition is meaningful.
#[serde(default)]
pub preconditions: Vec<String>,
/// The asserted law body.
pub postcondition: String,
/// Citation into `SPEC.md`.
pub citation: String,
}
/// One free variable in a formal law statement.
#[derive(Debug, Clone, Eq, PartialEq, serde::Deserialize)]
pub struct FormalVariable {
/// Variable name used in the mathematical statement.
pub name: String,
/// Variable type in the law domain.
#[serde(rename = "type")]
pub ty: String,
/// Variable role, such as `input` or `witness`.
pub role: String,
}
/// One symbolic law parameter supplied by an `AlgebraicLaw` payload.
#[derive(Debug, Clone, Eq, PartialEq, serde::Deserialize)]
pub struct FormalParameter {
/// Parameter name used in the mathematical statement.
pub name: String,
/// Parameter type.
#[serde(rename = "type")]
pub ty: String,
/// Parameter source in the Rust enum payload.
pub source: String,
}