Constraints

The constraints module handles plausibility checks and visual placement rules. It deliberately sits next to, but separate from, Legal Verification.

Constraint Families

fn transaction_input() -> vendor_constraints
fn transaction_input() -> invoice_arithmetic
fn pipeline_graph() -> layout_constraints
fn vendor_constraints() -> constraint_evaluation
fn invoice_arithmetic() -> constraint_evaluation
fn layout_constraints() -> visualization_model
match constraint_evaluation => Required -> block_pipeline
match constraint_evaluation => Strong -> recoverable_issue
match constraint_evaluation => Medium -> warning_issue
match constraint_evaluation => Weak -> advisory_issue

flowchart TD
    transaction_input["transaction_input"]
    vendor_constraints["vendor_constraints"]
    invoice_arithmetic["invoice_arithmetic"]
    pipeline_graph["pipeline_graph"]
    layout_constraints["layout_constraints"]
    constraint_evaluation["constraint_evaluation"]
    visualization_model["visualization_model"]
    match_constraint_evaluation{"match constraint_evaluation"}
    block_pipeline["block_pipeline"]
    recoverable_issue["recoverable_issue"]
    warning_issue["warning_issue"]
    advisory_issue["advisory_issue"]
    transaction_input --> vendor_constraints
    transaction_input --> invoice_arithmetic
    pipeline_graph --> layout_constraints
    vendor_constraints --> constraint_evaluation
    invoice_arithmetic --> constraint_evaluation
    layout_constraints --> visualization_model
    match_constraint_evaluation -->|"Required"|block_pipeline
    match_constraint_evaluation -->|"Strong"|recoverable_issue
    match_constraint_evaluation -->|"Medium"|warning_issue
    match_constraint_evaluation -->|"Weak"|advisory_issue

Kasuari Use

Kasuari-style strengths are used for constraints where failure is graded:

Required: must pass before the pipeline proceeds.
Strong: recoverable issue; normally needs repair or review.
Medium: warning; may proceed with an audit note.
Weak: advisory signal.

This is appropriate for vendor plausibility and document-shape expectations because historical data is rarely a hard legal proof.

Z3 Boundary

Use Z3 when the application needs proof-like yes/no behavior:

tax rule satisfaction
reconciliation balance equations
workbook export invariants
mutually exclusive classifications
workflow transition guards

Use this module’s constraint evaluation when the question is “how plausible is this value?” rather than “is this formula satisfiable?”

VendorConstraintSet

#![allow(unused)]
fn main() {
pub struct VendorConstraintSet {
    pub vendor: String,
    pub constraints: Vec<Constraint>,
}
}

Typical checks:

amount range
date window
description pattern
account format

InvoiceConstraintSolver checks invoice arithmetic such as subtotal, tax, and total consistency. Today it is a lightweight plausibility solver; future work can route strict arithmetic proof obligations through Z3 where audit explanations need counterexamples.

LayoutSolver

The visualization system also uses constraints to keep graph nodes readable. Match arms, default lanes, and rejoin points are layout constraints, not financial constraints.

Keyboard shortcuts

l3dg3rr Ledger Documentation