Crate legalis_verifier 

Legalis-Verifier: Formal verification for Legalis-RS legal statutes.

This crate provides static analysis and verification tools for detecting logical inconsistencies, circular references, and constitutional conflicts in legal statutes.

Modules

certification_framework

Certification Framework Module

distributed_verification

Distributed Verification Module

formal_methods

Formal Methods Integration for Legalis-Verifier

ml_verification

Machine Learning Verification for Legalis-Verifier

Structs

Ambiguity

Represents a detected ambiguity in a statute.

AmbiguousTerm

Represents an ambiguous term found in statutes.

BatchVerificationResult

Result of batch verification across multiple statutes.

CachedProof

Cached proof for a statute

CentralityMetrics

Centrality metrics for a single statute

ChangeImpact

Impact of a statute change on the system.

CiConfig

CI/CD configuration generator.

Clock

A clock variable used in timed automata.

Coalition

Represents a coalition of stakeholders

ComplexityMetrics

Complexity metrics for a statute.

ComplianceCertification

Compliance certification document

ComplianceItem

A compliance checklist item.

CompositePrinciple

A composite principle combining multiple principles.

ConflictCascade

Represents a conflict cascade - how conflicts propagate through statute dependencies

ConflictExplanation

Conflict explanation for laypersons

ConflictSummary

Conflict summary

ConstitutionalPrinciple

A constitutional principle to check against.

CoverageGap

Gap in statute coverage - a scenario not handled by any statute.

CoverageInfo

Code coverage information for condition analysis.

CrossReferenceError

Represents a cross-reference validation error.

Deadline

Deadline constraint for temporal verification.

DeadlineVerificationResult

Result of deadline verification.

DeadlineViolation

A deadline violation.

DependencyGraph

Fine-grained dependency graph

DependencyNode

Fine-grained dependency tracking for statutes

DiagnosticLocation

Diagnostic location for IDE integration.

DuplicateCandidate

Represents a potential duplicate statute.

EncryptedStatute

Encrypted statute representation for homomorphic computation

EncryptedVerificationResult

Encrypted verification result

EnhancedCoverageGap

Enhanced coverage gap with more detailed analysis

EvolutionMetrics

Evolution metrics for a statute

EvolutionSummary

Evolution summary

EvolutionTracker

Tracks evolution for multiple statutes

ExecutiveSummary

Executive summary of verification results

GameOutcome

Represents an outcome in the game

GameTheoreticModel

Represents a game-theoretic model

GraphMetrics

Graph metrics for statute dependency network

IdeDiagnostic

LSP-compatible diagnostic for IDE integration.

ImpactAssessment

Impact assessment for a statute or set of statutes.

IncrementalState

Incremental verification state for tracking statute changes.

InteractiveProof

Interactive proof explorer data structure

JurisdictionalRuleSet

A jurisdictional rule set containing principles for a specific jurisdiction.

LazyVerificationConfig

Lazy verification configuration

MarkovChain

Discrete-Time Markov Chain (DTMC)

MarkovState

Represents a state in a Markov chain

MarkovTransition

Represents a transition between states with probability

MechanismAnalysis

Mechanism design analysis result

MechanismIssue

Represents a mechanism design issue

MetricsDashboard

Comprehensive dashboard containing all metrics

MultiPartyVerificationResult

Multi-party computation result Allows multiple parties to jointly verify statutes without sharing their private inputs

NaturalLanguageExplanation

Natural language explanation for a verification error

NotificationConfig

Notification configuration.

NotificationMessage

Notification message.

OptimizationSuggestion

Optimization suggestion for statute conditions.

PreCommitHook

Git pre-commit hook configuration.

Precedent

Represents a legal precedent that may be relevant to a statute.

PrecedentRegistry

Registry for managing precedents.

PrincipleCheckResult

Result of a constitutional principle check.

PrincipleDefinition

A principle definition in the DSL.

PrincipleRegistry

Principle registry managing multiple jurisdictions.

PrivacyBudget

Differential privacy parameters

PrivateAggregation

Differentially private aggregation result

ProofCache

Incremental proof maintenance

ProofCacheStats

Proof cache statistics

ProofCertificate

Proof certificate for formal verification

ProofStep

Represents a step in a verification proof

QualityMetrics

Overall quality score for a statute.

QualitySummary

Quality metrics summary

QuickFix

Quick fix suggestion for IDE code actions.

RedundancyInstance

Represents a redundancy in the statute set

RegulatoryFiling

Regulatory filing report for submitting to regulatory bodies

RegulatoryImpact

Regulatory impact assessment for a statute.

RegulatoryOverlap

Represents a regulatory overlap between statutes

ReportSchedule

Schedule configuration for automated report generation

ReportScheduler

Manages multiple report schedules

ReportTemplate

Report template for customizable report generation

RiskFactor

Risk factor for statute analysis

RiskQuantification

Risk quantification analysis result

ScheduledReportResult

Result of a scheduled report execution

SequenceConstraint

Sequence constraint specifying required event ordering.

SequenceVerificationResult

Result of sequence constraint verification.

SequenceViolation

A sequence constraint violation.

SimilarityScore

Semantic similarity score between two items (0.0 = completely different, 1.0 = identical).

Stakeholder

Represents a stakeholder in the legal system

StakeholderConflict

Represents a conflict between multiple stakeholders

StatisticalCheckResult

Statistical model checking result

StatuteCluster

Cluster/community in the statute graph

StatuteConflict

Represents a conflict between two or more statutes.

StatuteEvolution

Evolution history for a statute

StatuteFilingInfo

Information about a statute in a regulatory filing

StatuteInteraction

Represents an interaction between two statutes

StatutePattern

Common pattern found in statutes

StatuteStatistics

Statistical summary of a statute collection.

StatuteVerifier

Verifier for legal statutes.

StatuteVersion

Version entry in statute evolution history

Strategy

Represents a strategy in a game-theoretic model

SummaryStatistics

Statistics for executive summary

TeeConfig

Trusted Execution Environment (TEE) configuration

TeeVerificationResult

TEE-based verification result

TemporalState

A state in a temporal model.

TerminologyInconsistency

Represents a terminology inconsistency.

TextEdit

Text edit for applying quick fixes.

TimedAutomaton

A timed automaton.

TimedLocation

A location (state) in a timed automaton.

TimedTransition

A transition in a timed automaton.

TransitionSystem

A transition system for temporal logic verification.

VerificationBudget

Budget for verification operations.

VerificationDiff

Difference between two verification results

VerificationPathNode

Verification path node for visualization

VerificationProof

A complete verification proof

VerificationRequest

API request for statute verification.

VerificationResponse

API response for statute verification.

VerificationResult

Result of a verification check.

VerificationSummary

Summary of verification results for certification

WhatIfScenario

What-if scenario for testing statute changes

ZeroKnowledgeProof

Zero-knowledge proof for statute verification Allows proving that a statute satisfies certain properties without revealing the statute details

Enums

AmbiguityType

Types of ambiguities that can be detected in statutes.

CiPlatform

CI/CD platform type.

ClockConstraint

Clock constraint in timed automata.

CombinationMode

How to combine principle results.

ComplexityLevel

Complexity levels for statutes.

ComplexityTrend

Trend in statute complexity over time

ConflictNature

Nature of stakeholder conflicts

ConflictType

Types of conflicts that can occur between statutes.

CrossReferenceErrorType

Types of cross-reference errors.

CtlFormula

Computation Tree Logic (CTL) formula.

CtlStarFormula

CTL* formula combining LTL and CTL path quantifiers. CTL* is a superset of both LTL and CTL, allowing arbitrary mixing of path quantifiers (E, A) with linear temporal operators (X, F, G, U, R).

CtlStarPathFormula

CTL* path formula (used after path quantifiers).

DependencyType

Type of dependency between statutes

GapType

Types of coverage gaps

ImpactLevel

Impact level classification.

InteractionType

Types of interactions between statutes

LtlFormula

Linear Temporal Logic (LTL) formula.

MechanismProperty

Represents a mechanism design property

NotificationChannel

Notification channel.

NotificationType

Notification type.

OverlapArea

Areas where statutes can overlap

PatternType

Type of statute pattern

PrincipleCheck

Types of constitutional checks.

ProofStepType

Types of proof steps

RedundancyType

Types of redundancy

ReportOutputFormat

Output format for scheduled reports

ReportSection

Section in a report template

RiskLevel

Risk level classification.

Severity

Severity level for verification errors.

StatuteChange

Represents a change between two statute versions.

VerificationError

Errors from verification process.

Functions

ambiguity_report

Generates an ambiguity detection report for a statute.

analyze_centrality

Computes centrality metrics for each statute

analyze_change_impact

Analyzes the impact of changing a statute in a collection.

analyze_coalitions

Analyzes potential coalitions among stakeholders

analyze_complexity

Analyzes the complexity of a statute.

analyze_coverage

Analyzes code coverage for conditions in statutes.

analyze_coverage_gaps

Analyzes statute coverage and identifies potential gaps.

analyze_enhanced_coverage_gaps

Analyzes coverage gaps in statutes with enhanced detection

analyze_graph_metrics

Computes overall graph metrics for statute dependencies

analyze_quality

Analyzes statute quality and returns comprehensive metrics.

analyze_regulatory_impact

Analyzes the regulatory impact of a statute.

analyze_stakeholder_conflicts

Analyzes conflicts between multiple stakeholders

analyze_statute_interactions

Analyzes interactions between statutes

analyze_statute_risk

Analyzes statute risk using multiple factors

analyze_statute_statistics

Analyzes a collection of statutes and returns comprehensive statistics.

assess_impact

Performs an impact assessment on a statute.

assess_multiple_impacts

Performs impact assessment on multiple statutes and generates a comprehensive report.

batch_ambiguity_report

Generates an ambiguity detection report for multiple statutes.

batch_verification_report

Generates a batch verification report.

batch_verify

Performs batch verification on multiple statutes and returns aggregate results.

build_verification_path

Builds a verification path from a statute and result

change_impact_report

Generates a change impact report.

check_accessibility

Performs accessibility verification on a statute.

check_due_process

Performs due process verification on a statute.

check_equal_protection

Checks equal protection principles (comprehensive).

check_equality

Performs a comprehensive equality check on a statute.

check_freedom_of_expression

Checks freedom of expression principles.

check_privacy_impact

Performs privacy impact assessment on a statute.

check_procedural_due_process

Checks procedural due process principles (detailed).

check_property_rights

Checks property rights principles.

check_proportionality

Performs proportionality checking on a statute.

check_retroactivity

Checks if the statute violates the principle of non-retroactivity (ex post facto).

check_terminology_consistency

Checks for terminology consistency across statutes.

coalition_analysis_report

Generates a coalition analysis report

compare_statutes

Compares two versions of a statute and identifies changes.

complexity_report

Generates a complexity report for multiple statutes.

compliance_certification_report

Exports compliance certification as a formatted report

compliance_checklist_report

Generates a compliance checklist report for a statute.

compliance_report_template

Creates a compliance-focused report template

compress_proof

Compresses a proof by removing redundant steps

conflict_cascade_report

Report on conflict cascades

conflict_detection_report

Generates a conflict detection report.

consolidated_compliance_checklist

Generates a consolidated compliance checklist for multiple statutes.

cross_reference_report

Generates a cross-reference validation report.

daily_compliance_schedule

Creates a daily compliance report schedule

dashboard_markdown_summary

Generates a markdown summary of the dashboard

detect_ambiguities

Detects ambiguities in a statute.

detect_clusters

Detects clusters/communities in the statute graph using simple heuristic

detect_duplicates

Detects potential duplicate or near-duplicate statutes.

detect_nash_equilibria

Detects Nash equilibria in statute interactions

detect_regulatory_overlaps

Detects regulatory overlaps between statutes

detect_statute_conflicts

Detects conflicts between statutes.

differential_private_analysis

Performs differentially private aggregation analysis

duplicate_detection_report

Generates a duplicate detection report.

enhanced_coverage_gap_report

Report on enhanced coverage gaps

evolution_report

Generates an evolution report for tracked statutes

execute_scheduled_report

Executes a scheduled report generation

executive_summary_report

Exports executive summary as a formatted report

explain_conflict

Explains statute conflicts in layperson terms

explain_error

Generates natural language explanation for a verification error

export_dashboard_html

Exports dashboard to HTML

export_dashboard_json

Exports dashboard to JSON

export_dependency_graph

Exports statute dependencies as a GraphViz DOT format graph.

export_dependency_graph_with_conflicts

Exports statute dependencies with conflict highlighting.

export_proof_dot

Exports proof in DOT format for visualization

find_ambiguous_terms

Finds ambiguous terms in a set of statutes.

find_similar_statutes

Finds pairs of statutes with high semantic similarity (potential duplicates).

game_theoretic_report

Generates a game-theoretic analysis report

generate_circular_reference_proof

Generates a proof for circular reference detection

generate_compliance_certification

Generates a compliance certification document

generate_compliance_checklist

Generates a compliance checklist from a statute.

generate_custom_report

Generates a custom report based on a template

generate_executive_summary

Generates an executive summary from verification results

generate_html_report

Generates an HTML report for verification results.

generate_interactive_html_report

Generates an interactive HTML report with filtering, search, and sorting capabilities.

generate_lsp_diagnostics

Generates LSP-compatible diagnostic JSON output.

generate_metrics_dashboard

Generates a comprehensive metrics dashboard

generate_quick_fixes

Generates quick fixes for common verification errors.

generate_regulatory_filing

Generates a regulatory filing report

generate_sarif_report

Generates a SARIF (Static Analysis Results Interchange Format) report.

graph_analysis_report

Generates a comprehensive graph analysis report

lazy_verify

Performs lazy verification on demand

mechanism_design_report

Generates a mechanism design analysis report

mine_patterns

Mines common patterns from a collection of statutes

monte_carlo_verification

Monte Carlo simulation for statute verification

monthly_comprehensive_schedule

Creates a monthly comprehensive report schedule

optimization_and_gaps_report

Generates a report of coverage gaps and optimization suggestions.

pattern_mining_report

Generates a pattern mining report

predict_conflict_cascades

Predicts conflict cascades based on statute dependencies

predict_game_outcomes

Predicts game-theoretic outcomes from statute interactions

proof_comparison_report

Generates a proof comparison report

quality_report

Generates a quality report for multiple statutes.

quality_report_template

Creates a quality-focused report template

redundancy_elimination_report

Report on redundancy elimination suggestions

regulatory_filing_report

Exports regulatory filing as a formatted report

regulatory_impact_report

Generates a regulatory impact report for multiple statutes.

regulatory_overlap_report

Report on regulatory overlaps

risk_quantification_report

Generates a risk quantification report

secure_multiparty_verification

Performs secure multi-party verification

semantic_similarity

Calculates semantic similarity between two statutes.

send_notification

Sends a notification based on configuration.

stakeholder_conflict_report

Generates a stakeholder conflict analysis report

standard_report_template

Creates a standard comprehensive report template

statistical_model_checking_report

Generates a statistical model checking report

statistics_report

Generates a statistical report for a statute collection.

statute_interaction_report

Report on statute interactions

suggest_redundancy_elimination

Detects redundancies and suggests elimination strategies

synthesize_ctl_property

Synthesizes a CTL property from a transition system and examples.

synthesize_ltl_property

Synthesizes a temporal property from positive and negative examples.

tee_verification

Performs verification in a trusted execution environment

term_disambiguation_report

Generates a term disambiguation report for a set of statutes.

terminology_consistency_report

Generates a terminology consistency report.

to_ide_diagnostics

Converts verification results to IDE diagnostics.

validate_cross_references

Validates cross-references between statutes.

verify_ctl

Checks if a CTL formula holds in a transition system.

verify_ctl_star

Verifies a CTL* formula on a transition system.

verify_deadlines

Verifies deadlines in a transition system.

verify_integrity

Verifies the integrity of a set of laws.

verify_ltl

Checks if an LTL formula holds in a transition system.

verify_mechanism_design

Verifies mechanism design properties of statutes

verify_sequences

Verifies sequence constraints in a transition system.

verify_timed_reachability

Verifies reachability in a timed automaton.

weekly_quality_schedule

Creates a weekly quality report schedule

what_if_analysis

Performs what-if analysis on a statute modification