fix(lib): no Inf/NaN scores, every export documented, ECHIDNA receipt check, dead sources removed

Project.toml

@@ -3,15 +3,15 @@
 name = "Axiology"
 uuid = "868b87ec-ec5d-47a0-ab5f-c8a8ecbd97bd"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
-version = "0.1.0"
+version = "0.1.1"
 license = "MPL-2.0"
 
 [deps]
 Statistics = "10745b16-79ce-11e8-11f9-7d13ad32a3b2"
-LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e"
 
 [compat]
-julia = "1.9"
+Statistics = "1"
+julia = "1.10"
 
 [extras]
 Test = "8dfed614-e22c-5e08-85e1-65c5234f0b40"

src/Axiology.jl

@@ -4,80 +4,60 @@
 """
     Axiology
 
-The Axiology.jl module provides a robust framework for integrating value theory
-into machine learning models. In an era where AI systems increasingly influence
-critical decisions, understanding and explicitly managing their ethical and
-economic implications is paramount. This module allows practitioners and researchers
-to define, optimize, and formally verify various values within their ML pipelines.
-
-The term "Axiology" (from Greek ἀξία, axía, "value"; and -λογία, -logia, "theory")
-refers to the philosophical study of value. In this context, Axiology.jl brings
-this study into the computational domain, providing tools to operationalize and
-reason about values such as fairness, welfare, profit, efficiency, and safety.
-
-Key Features & Applications:
-----------------------------
-1.  **Value Type System**: Define diverse ethical and economic values (e.g., `Fairness`,
-    `Welfare`, `Profit`, `Efficiency`, `Safety`) as first-class citizens. This allows
-    for explicit representation of desired model behaviors beyond traditional performance metrics.
-2.  **Value Satisfaction Checking**: Assess whether a given ML model's behavior or
-    outcome `satisfy` predefined value criteria (e.g., is a model "fair" according
-    to a specific metric and threshold?).
-3.  **Multi-Objective Optimization**: Address the inherent trade-offs between
-    competing values (e.g., fairness vs. efficiency, profit vs. safety). The module
-    supports finding optimal model configurations that balance multiple objectives.
-4.  **Pareto Frontier Analysis**: Explore the set of non-dominated solutions in
-    multi-objective optimization, providing insights into the best possible trade-offs
-    between different values.
-5.  **Value Verification**: Lay the groundwork for formal verification of value properties,
-    ensuring that models adhere to their intended ethical and economic principles
-    under various conditions.
-
-Axiology.jl aims to foster more transparent, accountable, and ethically aligned AI systems
-by moving beyond black-box optimization towards explicit value-driven design. It provides
-a bridge between philosophical considerations of value and the practical implementation
-of machine learning.
+Value theory for machine-learning and decision systems: make the values a
+system is meant to serve explicit, typed and checkable.
+
+Axiology (from Greek ἀξία, *axía*, "value", and -λογία, *-logia*, "study") is the
+philosophical study of value. This package gives a small set of value concepts a
+computational form so they can be stated, scored and compared:
+
+1. **Value types** — `Fairness`, `Welfare`, `Profit`, `Efficiency` and `Safety`,
+   all subtypes of `Value`, each carrying its metric, threshold or target, and a
+   weight.
+2. **Satisfaction checks** — `satisfy(value, state)` reports whether a system
+   state (a `Dict` of predictions, utilities, profit, timings, …) meets the value.
+3. **Fairness and welfare measures** — `demographic_parity`, `equalized_odds`,
+   `equal_opportunity`, `disparate_impact`, `individual_fairness`;
+   `utilitarian_welfare`, `rawlsian_welfare`, `egalitarian_welfare`.
+4. **Multi-objective comparison** — `value_score`, `weighted_score`,
+   `normalize_scores`, `dominated` and `pareto_frontier` compare candidate
+   states across several values without hiding the trade-offs.
+5. **Verification evidence** — `verify_value` checks the shape of a
+   caller-supplied attestation, and `verify_receipt` strictly checks an ECHIDNA
+   `echidna.prove.result/1` receipt. Neither runs a prover. `safety_verdict`
+   reports `:entailed`, `:refuted` or `:unresolved` so missing safety evidence
+   stays visible.
 
 # Example
 
 ```julia
 using Axiology
 
-# Define a fairness criterion
-fairness = Fairness(
-    metric = :demographic_parity,
-    protected_attributes = [:gender, :race],
-    threshold = 0.05
-)
+fairness = Fairness(metric = :demographic_parity,
+                    protected_attributes = [:group],
+                    threshold = 0.05)
 
-# Simulate a model's state or evaluation results
-model_evaluation_state = Dict(
-    :predictions => [0.8, 0.7, 0.6, 0.9, 0.5, 0.75],
-    :protected => [:male, :female, :male, :female, :male, :female],
-    :actual_labels => [1, 1, 0, 1, 0, 1],
-    :disparity => 0.03 # Assuming a pre-calculated disparity for demographic_parity
+state = Dict(
+    :predictions => [1, 0, 1, 1, 0, 1],
+    :protected   => [:a, :a, :b, :b, :b, :a],
 )
 
-# Check if the model satisfies the defined fairness criterion
-@assert satisfy(fairness, model_evaluation_state)  # True if disparity < threshold
+satisfy(fairness, state)  # true: both groups have a positive rate of 2/3
 
-# Define multiple competing values for optimization
-values_to_optimize = [
-    Welfare(metric = :utilitarian, weight = 0.4),
-    Fairness(metric = :equalized_odds, weight = 0.3),
-    Efficiency(metric = :computation_time, weight = 0.3)
+values = [
+    Welfare(metric = :utilitarian, weight = 0.5),
+    Fairness(metric = :demographic_parity, threshold = 0.1, weight = 0.5),
 ]
-
-# (Conceptual) Find solutions on the Pareto frontier for a given system
-# In practice, `system` would represent an ML model or decision-making process
-# and `pareto_frontier` would search its configuration space.
-# solutions = pareto_frontier(my_ml_system_configs, values_to_optimize)
+candidates = [
+    Dict(:utilities => [3.0, 3.0], :predictions => [1, 1], :protected => [:a, :b]),
+    Dict(:utilities => [9.0, 0.0], :predictions => [1, 0], :protected => [:a, :b]),
+]
+pareto_frontier(candidates, values)  # both survive: one is fairer, the other has more welfare
 ```
 """
 module Axiology
 
 using Statistics
-using LinearAlgebra
 
 # Core value types
 export Value, Fairness, Welfare, Profit, Efficiency, Safety
@@ -88,6 +68,7 @@ export disparate_impact_metric, individual_fairness_metric
 export utilitarian_metric, rawlsian_metric, egalitarian_metric
 export pareto_metric, kaldor_hicks_metric, computation_time_metric
 export satisfy, maximize, verify_value
+export verify_receipt, safety_verdict, PROVE_RESULT_SCHEMA
 export pareto_frontier, dominated, value_score
 export weighted_score, normalize_scores
 

src/fairness.jl

@@ -1,6 +1,23 @@
 # SPDX-License-Identifier: MPL-2.0
 # Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
+"""
+    demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64
+
+Return the demographic-parity disparity: the largest difference in mean
+prediction (the positive-prediction rate, for binary predictions) between any
+two protected groups. `0.0` means perfect parity.
+
+Returns `0.0` when fewer than two groups are present.
+
+# Example
+
+```julia
+predictions = [1, 0, 1, 1, 0, 1]
+protected = [:A, :A, :B, :B, :B, :A]
+demographic_parity(predictions, protected)  # 0.0 (both groups have rate 2/3)
+```
+"""
 function demographic_parity(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64
     @assert length(predictions) == length(protected_attributes) "Lengths must match."
     unique_groups = unique(protected_attributes)
@@ -17,6 +34,28 @@ function demographic_parity(predictions::AbstractVector, protected_attributes::A
     return maximum(rates) - minimum(rates)
 end
 
+"""
+    equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real},
+                   protected_attributes::AbstractVector)::Float64
+
+Return the equalized-odds disparity: the larger of the maximum between-group
+difference in true-positive rate (TPR) and in false-positive rate (FPR).
+`0.0` means the groups are treated alike on both rates.
+
+A group with no positive labels has no defined TPR and is left out of the TPR
+comparison; likewise a group with no negative labels is left out of the FPR
+comparison. Each comparison needs at least two groups with a defined rate and
+otherwise contributes `0.0`. Returns `0.0` when fewer than two groups are present.
+
+# Example
+
+```julia
+predictions = [1, 0, 1, 1, 0, 1]
+labels      = [1, 0, 0, 1, 0, 1]
+protected   = [:A, :A, :B, :B, :B, :A]
+equalized_odds(predictions, labels, protected)
+```
+"""
 function equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real},
                         protected_attributes::AbstractVector)::Float64
     @assert length(predictions) == length(labels) == length(protected_attributes) "Lengths must match."
@@ -51,6 +90,26 @@ function equalized_odds(predictions::AbstractVector{<:Real}, labels::AbstractVec
     return max(max_tpr_disparity, max_fpr_disparity)
 end
 
+"""
+    equal_opportunity(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real},
+                      protected_attributes::AbstractVector)::Float64
+
+Return the equal-opportunity disparity: the maximum between-group difference in
+true-positive rate (TPR) only. `0.0` means individuals who merit a positive
+outcome receive one at the same rate in every group.
+
+Groups with no positive labels have no defined TPR and are left out; if fewer
+than two groups have a defined TPR the result is `0.0`.
+
+# Example
+
+```julia
+predictions = [1, 0, 1, 1, 0, 1]
+labels      = [1, 0, 0, 1, 0, 1]
+protected   = [:A, :A, :B, :B, :B, :A]
+equal_opportunity(predictions, labels, protected)
+```
+"""
 function equal_opportunity(predictions::AbstractVector{<:Real}, labels::AbstractVector{<:Real},
                           protected_attributes::AbstractVector)::Float64
     @assert length(predictions) == length(labels) == length(protected_attributes) "Lengths must match."
@@ -75,6 +134,29 @@ function equal_opportunity(predictions::AbstractVector{<:Real}, labels::Abstract
     return length(tprs) >= 2 ? maximum(tprs) - minimum(tprs) : 0.0
 end
 
+"""
+    disparate_impact(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64
+
+Return the disparate-impact ratio: the lowest group selection rate divided by
+the highest. `1.0` means equal selection rates; values near `0.0` mean strong
+disparity. Under the "four-fifths rule" a ratio below `0.8` is commonly read as
+evidence of adverse impact.
+
+Returns `1.0` when fewer than two groups are present or when no group is ever
+selected.
+
+Note that this is a ratio where *higher is fairer*, the opposite orientation to
+the disparity metrics above; `satisfy(::Fairness, …)` therefore reads a
+`:disparate_impact` threshold as a minimum ratio (e.g. `threshold = 0.8`).
+
+# Example
+
+```julia
+predictions = [1, 0, 1, 1, 0, 1]
+protected   = [:A, :A, :B, :B, :B, :A]
+disparate_impact(predictions, protected)  # 1.0
+```
+"""
 function disparate_impact(predictions::AbstractVector, protected_attributes::AbstractVector)::Float64
     @assert length(predictions) == length(protected_attributes) "Lengths must match."
     unique_groups = unique(protected_attributes)
@@ -93,6 +175,28 @@ function disparate_impact(predictions::AbstractVector, protected_attributes::Abs
     return max_rate > 0.0 ? min_rate / max_rate : 1.0
 end
 
+"""
+    individual_fairness(predictions::AbstractVector, similarity_matrix::AbstractMatrix;
+                        similarity_threshold::Float64 = 0.8)::Float64
+
+Return the mean absolute prediction difference over all pairs of individuals
+whose similarity exceeds `similarity_threshold` ("similar individuals should be
+treated similarly"). `0.0` is best.
+
+`similarity_matrix` must be `n×n` for `n` predictions, with entries normally in
+`[0, 1]`. Returns `0.0` when no pair is similar enough to compare.
+
+# Example
+
+```julia
+predictions = [0.8, 0.2, 0.7, 0.3]
+similarity  = [1.0 0.9 0.1 0.2;
+               0.9 1.0 0.2 0.1;
+               0.1 0.2 1.0 0.85;
+               0.2 0.1 0.85 1.0]
+individual_fairness(predictions, similarity; similarity_threshold = 0.8)
+```
+"""
 function individual_fairness(predictions::AbstractVector, similarity_matrix::AbstractMatrix;
                             similarity_threshold::Float64 = 0.8)::Float64
     n = length(predictions)
@@ -111,6 +215,19 @@ function individual_fairness(predictions::AbstractVector, similarity_matrix::Abs
     return count > 0 ? total_diff / count : 0.0
 end
 
+"""
+    satisfy(value::Fairness, state::Dict)::Bool
+
+Return whether `state` meets the fairness criterion `value`.
+
+`state` must hold `:predictions`, plus `:protected` (or `:protected_attributes`)
+for the group metrics, `:labels` for `:equalized_odds`/`:equal_opportunity`, and
+`:similarity_matrix` for `:individual_fairness`. A missing key raises an error.
+
+For the disparity metrics the check is `disparity <= value.threshold`. For
+`:disparate_impact` it is `ratio >= value.threshold`, so the threshold is a
+minimum ratio there (the default `0.05` is far looser than the usual `0.8`).
+"""
 function satisfy(value::Fairness, state::Dict)::Bool
     predictions = get(state, :predictions, nothing)
     protected = get(state, :protected, get(state, :protected_attributes, nothing))