File size: 4,646 Bytes
224e773 | 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 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 | //! HyperKitty Constraint Language (HKCL) Compiler
//!
//! A full compiler pipeline for constraint definitions:
//! 1. Lexer: Tokenize source code with keyword recognition and literal parsing
//! 2. Parser: Build typed AST from token stream
//! 3. AST: Immutable constraint program with named constraints and requirements
//! 4. Evaluator: Execute constraints against variable bindings
//!
//! Grammar:
//! ```text
//! program := constraint*
//! constraint := 'validity' '(' IDENT ')' param '{' requirements 'otherwise' action '}'
//! param := IDENT | STRING
//! requirements := ('require' requirement ';')*
//! requirement := IDENT '(' ')' (* check *)
//! | IDENT (* predicate *)
//! action := 'reject' | 'accept'
//! ```
//!
//! Example:
//! ```ignore
//! validity(V1) "signature valid" {
//! require sig_check();
//! require not_revoked();
//! otherwise reject;
//! }
//! ```
//!
//! NAND Lowering (Future Enhancement):
//! Constraints currently evaluate using boolean algebra. Future versions will:
//! - Lower all requirements to NAND-tree representations
//! - Generate cryptographic commitments (Blake3/Ed25519)
//! - Persist evaluation traces to WORM ledger (immutable log)
//! - Enable formal verification and constraint replay
pub mod lexer;
pub mod parser;
pub mod ast;
pub mod evaluator;
pub mod xslt_processor;
pub use ast::{ConstraintProgram, Constraint, Requirement, OtherwiseAction};
pub use evaluator::Evaluator;
pub use lexer::Lexer;
pub use parser::Parser;
pub use xslt_processor::{
FormalizationMachine, InvariantRegistry, Invariant, ConstraintKind, Polarity,
ProverArtifact, ProverStatus, CorrespondenceObligation, CorrespondenceStatus,
AgdaIterationObligation, ExecutionSchedule, FormalizationSummary,
};
/// Compile HKCL source code into an executable constraint program.
///
/// # Steps:
/// 1. Tokenize: Source → Token stream
/// 2. Parse: Token stream → AST (ConstraintProgram)
/// 3. Validate: Check AST structure (no duplicates, valid names, etc.)
///
/// # Example:
/// ```ignore
/// let source = r#"validity(V) msg { require check(); otherwise reject; }"#;
/// let program = hyperkitty_constraints::compile(source)?;
/// ```
pub fn compile(source: &str) -> hyperkitty_core::Result<ConstraintProgram> {
let mut lexer = Lexer::new(source);
let tokens = lexer.tokenize()?;
let mut parser = Parser::new(tokens);
parser.parse()
}
#[cfg(test)]
mod tests {
use super::*;
use std::collections::HashMap;
#[test]
fn test_compile_simple_program() -> hyperkitty_core::Result<()> {
let source = r#"validity(V1) msg { require check(); otherwise reject; }"#;
let program = compile(source)?;
assert_eq!(program.constraints.len(), 1);
Ok(())
}
#[test]
fn test_full_pipeline() -> hyperkitty_core::Result<()> {
let source = r#"
validity(V1) "check1" {
require always_true();
otherwise reject;
}
validity(V2) "check2" {
require always_true();
otherwise accept;
}
"#;
let program = compile(source)?;
let evaluator = Evaluator::new(program);
let bindings = HashMap::new();
assert!(evaluator.evaluate(&bindings)?);
Ok(())
}
#[test]
fn test_multiple_requirements() -> hyperkitty_core::Result<()> {
let source = r#"
validity(V) msg {
require always_true();
require always_true();
otherwise reject;
}
"#;
let program = compile(source)?;
assert_eq!(program.constraints[0].requires.len(), 2);
Ok(())
}
#[test]
fn test_otherwise_accept() -> hyperkitty_core::Result<()> {
let source = r#"validity(V) msg { require always_false(); otherwise accept; }"#;
let program = compile(source)?;
let evaluator = Evaluator::new(program);
let bindings = HashMap::new();
// Requirement fails but "otherwise accept" means the constraint passes
assert!(evaluator.evaluate(&bindings)?);
Ok(())
}
#[test]
fn test_otherwise_reject() -> hyperkitty_core::Result<()> {
let source = r#"validity(V) msg { require always_false(); otherwise reject; }"#;
let program = compile(source)?;
let evaluator = Evaluator::new(program);
let bindings = HashMap::new();
// Requirement fails and "otherwise reject" means the constraint fails
assert!(!evaluator.evaluate(&bindings)?);
Ok(())
}
}
|