amari_flynn/
lib.rs

1//! # Amari Flynn - Probabilistic Contracts and Verification
2//!
3//! Named after Kevin Flynn from Tron: Legacy, who discovered that spontaneous,
4//! imperfect emergence (the ISOs) represented a form of perfection beyond rigid
5//! determinism. This library embodies that philosophy: formal verification should
6//! prove what's impossible while allowing rare, emergent possibilities.
7//!
8//! ## Philosophy: Three Types of Events
9//!
10//! Flynn teaches us to distinguish between three categories of events:
11//!
12//! 1. **Impossible** (P=0): Formally proven to never occur
13//!    - Violates mathematical axioms
14//!    - Proved unreachable via formal verification
15//!    - System invariants guarantee exclusion
16//!
17//! 2. **Rare** (0 < P << 1): Bounded probability, tracked and verified
18//!    - Low but non-zero probability
19//!    - Statistical bounds verified via Monte Carlo
20//!    - Tracked as legitimate possibilities
21//!
22//! 3. **Emergent** (P > 0): Possible but not prescribed, enabling discovery
23//!    - Not predicted or designed
24//!    - Arise spontaneously from system rules
25//!    - The "ISOs" of your system
26//!
27//! ## Core Concept
28//!
29//! Traditional verification asks: "Can this happen?"
30//! Flynn asks: "Is this impossible, rare, or merely unpredicted?"
31//!
32//! This library provides tools to:
33//! - Prove what cannot happen (P=0)
34//! - Bound what rarely happens (P<<1)
35//! - Enable what might emerge (P>0)
36//!
37//! ## Quick Start
38//!
39//! ```rust
40//! use amari_flynn::prelude::*;
41//!
42//! // Create probabilistic values
43//! let coin_flip = Prob::with_probability(0.5, true);
44//!
45//! // Sample from distributions
46//! let die_roll = Uniform::new(1, 6).sample();
47//!
48//! // Track rare events
49//! let miracle_shot = RareEvent::<()>::new(0.001, "critical_hit");
50//! ```
51//!
52//! ## Future Integration with Amari
53//!
54//! A future `geometric` feature will integrate Flynn with Amari's geometric algebra
55//! types, enabling probabilistic contracts over geometric computations.
56//!
57//! ## Roadmap
58//!
59//! - **SMT-LIB2 Backend** (v0.19.0): Generate proof obligations in SMT-LIB2 format
60//!   for Z3, CVC5, and other solvers. See [`backend::smt`].
61//! - **Creusot Support**: Rust-native formal verification
62//! - **External Solver Integration**: Automatic invocation of installed solvers
63//!
64//! ## The ISO Philosophy
65//!
66//! Like the ISOs in Tron: Legacy, the most valuable behaviors in a system
67//! are often those that emerge spontaneously, unpredicted by design. Flynn
68//! enables you to prove safety boundaries while preserving space for emergence.
69//!
70//! > "The ISOs, they were a miracle. They weren't meant to be - they just were."
71//! >
72//! > - Kevin Flynn
73//!
74//! ## Example: Game Mechanics Verification
75//!
76//! ```rust
77//! use amari_flynn::prelude::*;
78//!
79//! // Verify critical hit rate is bounded
80//! let crit_rate = 0.15;
81//! let crit_prob = Prob::with_probability(crit_rate, ());
82//!
83//! // Statistical verification that P(crit) ≤ 0.20
84//! // (leaving room for buffs/modifiers while maintaining balance)
85//! ```
86
87#![warn(missing_docs)]
88#![cfg_attr(not(feature = "std"), no_std)]
89
90#[cfg(feature = "std")]
91extern crate std;
92
93pub mod backend;
94pub mod contracts;
95pub mod distributions;
96pub mod prob;
97pub mod statistical;
98
99/// Prelude module for common imports
100pub mod prelude {
101    pub use crate::backend::monte_carlo::MonteCarloVerifier;
102    pub use crate::backend::smt::{ObligationKind, SmtProofObligation};
103    pub use crate::contracts::{
104        EventVerification, ProbabilisticContract, RareEvent, StatisticalProperty,
105        VerificationResult,
106    };
107    pub use crate::distributions::{Bernoulli, Exponential, Normal, Uniform};
108    pub use crate::prob::Prob;
109}
110
111// Re-export procedural macros
112pub use amari_flynn_macros::*;
amari_flynn/lib.rs

amari_flynn/
lib.rs
