feat(types): wire backend consumers + fix z3 build + outcome module

src/rust/exchange/dedukti.rs

@@ -211,6 +211,18 @@ impl DeduktiExporter {
                     Self::term_to_dedukti(body)
                 )
             },
+            Term::Sigma {
+                param,
+                param_type,
+                body,
+            } => {
+                format!(
+                    "(dk_sigma {} ({} => {}))",
+                    Self::term_to_dedukti(param_type),
+                    param,
+                    Self::term_to_dedukti(body)
+                )
+            },
             Term::Type(level) => format!("Type {}", level),
             Term::Sort(level) => format!("Sort {}", level),
             Term::Universe(level) => format!("Type {}", level),
@@ -224,6 +236,32 @@ impl DeduktiExporter {
         if trimmed.starts_with('(') && trimmed.ends_with(')') {
             // Unwrap parentheses and recurse
             Self::dedukti_to_term(&trimmed[1..trimmed.len() - 1])
+        } else if trimmed.starts_with("dk_sigma ") {
+            // Sigma type: dk_sigma A (x => B)
+            let rest = trimmed.trim_start_matches("dk_sigma ").trim();
+            // Split into the type part and the binder part (x => B)
+            if let Some(paren_start) = rest.find('(') {
+                let type_part = rest[..paren_start].trim();
+                let binder_part = rest[paren_start..].trim();
+                let inner = if binder_part.starts_with('(') && binder_part.ends_with(')') {
+                    &binder_part[1..binder_part.len() - 1]
+                } else {
+                    binder_part
+                };
+                if let Some(arrow_pos) = inner.find("=>") {
+                    let param = inner[..arrow_pos].trim().to_string();
+                    let body_str = inner[arrow_pos + 2..].trim();
+                    Term::Sigma {
+                        param,
+                        param_type: Box::new(Self::dedukti_to_term(type_part)),
+                        body: Box::new(Self::dedukti_to_term(body_str)),
+                    }
+                } else {
+                    Term::Const(trimmed.to_string())
+                }
+            } else {
+                Term::Const(trimmed.to_string())
+            }
         } else if trimmed.contains("->") {
             // Pi type: A -> B
             let parts: Vec<&str> = trimmed.splitn(2, "->").collect();
@@ -416,6 +454,28 @@ mod tests {
         assert_eq!(dk, "x");
     }
 
+    #[test]
+    fn test_term_to_dedukti_sigma() {
+        let term = Term::Sigma {
+            param: "x".to_string(),
+            param_type: Box::new(Term::Const("Nat".to_string())),
+            body: Box::new(Term::Const("Prop".to_string())),
+        };
+        let dk = DeduktiExporter::term_to_dedukti(&term);
+        assert!(dk.contains("dk_sigma"), "Sigma should render as dk_sigma, got: {}", dk);
+        assert!(dk.contains("Nat"), "Sigma param type should appear, got: {}", dk);
+    }
+
+    #[test]
+    fn test_dedukti_to_term_sigma() {
+        let dk = "dk_sigma Nat (x => Prop)";
+        let term = DeduktiExporter::dedukti_to_term(dk);
+        match term {
+            Term::Sigma { ref param, .. } => assert_eq!(param, "x"),
+            _ => panic!("Expected Sigma term, got: {:?}", term),
+        }
+    }
+
     #[test]
     fn test_import_with_definition() {
         let module = DeduktiModule {

src/rust/gnn/embeddings.rs

@@ -190,9 +190,11 @@ impl TermFeatureExtractor {
         // Feature [29]: Contains quantifier (forall, exists, pi)
         if offset < FEATURE_DIM {
             features[offset] = if node.label.contains("pi_")
+                || node.label.contains("sigma_")
                 || node.label.contains("forall")
                 || node.label.contains("exists")
                 || node.label.contains("Pi")
+                || node.label.contains("Sigma")
             {
                 1.0
             } else {
@@ -310,6 +312,8 @@ fn infer_term_kind_from_label(label: &str) -> usize {
         3 // Lambda
     } else if label.starts_with("pi_") {
         4 // Pi
+    } else if label.starts_with("sigma_") {
+        13 // Sigma
     } else if label.starts_with("let_") {
         7 // Let
     } else if label.starts_with("fix_") {

src/rust/gnn/graph.rs

@@ -17,7 +17,7 @@
 use serde::{Deserialize, Serialize};
 use std::collections::HashMap;
 
-use crate::core::{Context, Goal, Hypothesis, ProofState, Term, Theorem};
+use crate::core::{Context, Definition, Goal, Hypothesis, ProofState, Term, Theorem};
 
 /// Kind of node in the proof graph.
 ///
@@ -63,6 +63,12 @@ pub enum EdgeKind {
     DependsOn,
     /// Reverse of DependsOn (premise is useful for goal)
     UsefulFor,
+    /// Source has the target as its QTT multiplicity annotation
+    HasMultiplicity,
+    /// Source has the target as its algebraic effect annotation
+    HasEffect,
+    /// Source has the target as its modal decoration
+    HasModality,
 }
 
 /// A single node in the proof graph.
@@ -185,18 +191,25 @@ impl ProofGraphBuilder {
         // Phase 2: Add hypothesis nodes from context
         let hyp_ids = self.add_hypotheses_from_context(&state.context);
 
+        // Phase 2b: Add definition nodes from context
+        let def_ids = self.add_definitions_from_context(&state.context);
+
         // Phase 3: Add premise/theorem nodes from context
         for theorem in &state.context.theorems {
             let pid = self.add_premise(theorem);
             premise_node_ids.push(pid);
         }
 
-        // Phase 4: Add dependency edges from goals to hypotheses/premises
+        // Phase 4: Add dependency edges from goals to hypotheses/definitions/premises
         if let Some(gid) = goal_node_id {
             for &hid in &hyp_ids {
                 self.add_edge(gid, hid, EdgeKind::DependsOn, 1.0);
                 self.add_edge(hid, gid, EdgeKind::UsefulFor, 1.0);
             }
+            for &did in &def_ids {
+                self.add_edge(gid, did, EdgeKind::DependsOn, 0.9);
+                self.add_edge(did, gid, EdgeKind::UsefulFor, 0.9);
+            }
             for &pid in &premise_node_ids {
                 self.add_edge(gid, pid, EdgeKind::DependsOn, 0.8);
                 self.add_edge(pid, gid, EdgeKind::UsefulFor, 0.8);
@@ -278,6 +291,11 @@ impl ProofGraphBuilder {
             self.expand_term(body, hid, 1);
         }
 
+        // Wire type_info annotations as edges
+        if let Some(ref info) = hyp.type_info {
+            self.add_type_info_edges(hid, info);
+        }
+
         hid
     }
 
@@ -288,11 +306,49 @@ impl ProofGraphBuilder {
             let label = format!("{}: {}", var.name, var.ty);
             let vid = self.add_node(NodeKind::Hypothesis, &label, 0);
             self.expand_term(&var.ty, vid, 1);
+
+            // Wire type_info annotations as edges
+            if let Some(ref info) = var.type_info {
+                self.add_type_info_edges(vid, info);
+            }
+
             ids.push(vid);
         }
         ids
     }
 
+    /// Add definition nodes from the global context.
+    fn add_definitions_from_context(&mut self, ctx: &Context) -> Vec<usize> {
+        let mut ids = Vec::new();
+        for def in &ctx.definitions {
+            let did = self.add_definition(def);
+            ids.push(did);
+        }
+        ids
+    }
+
+    /// Add a definition node.
+    fn add_definition(&mut self, def: &Definition) -> usize {
+        let label = format!("{}: {}", def.name, def.ty);
+        let did = self.add_node(NodeKind::Hypothesis, &label, 0);
+
+        // Expand the definition type
+        let type_id = self.expand_term(&def.ty, did, 1);
+        if let Some(tid) = type_id {
+            self.add_edge(did, tid, EdgeKind::HasType, 1.0);
+        }
+
+        // Expand the definition body
+        self.expand_term(&def.body, did, 1);
+
+        // Wire type_info annotations as edges
+        if let Some(ref info) = def.type_info {
+            self.add_type_info_edges(did, info);
+        }
+
+        did
+    }
+
     /// Add a premise (theorem/lemma) node.
     fn add_premise(&mut self, theorem: &Theorem) -> usize {
         let label = format!("{}: {}", theorem.name, theorem.statement);
@@ -456,6 +512,32 @@ impl ProofGraphBuilder {
         }
     }
 
+    /// Add edges from a node to represent its [`TypeInfo`] annotations.
+    ///
+    /// Creates labelled subterm nodes for multiplicity, effect, and modality
+    /// decorations and connects them with the appropriate edge kind.
+    fn add_type_info_edges(&mut self, node_id: usize, info: &crate::types::TypeInfo) {
+        if let Some(ref mult) = info.multiplicity {
+            let label = format!("mult:{:?}", mult);
+            let mid = self.add_node(NodeKind::Subterm, &label, 1);
+            self.add_edge(node_id, mid, EdgeKind::HasMultiplicity, 1.0);
+        }
+
+        if !info.effects.is_empty() {
+            for eff in &info.effects.effects {
+                let label = format!("effect:{:?}", eff);
+                let eid = self.add_node(NodeKind::Subterm, &label, 1);
+                self.add_edge(node_id, eid, EdgeKind::HasEffect, 1.0);
+            }
+        }
+
+        if let Some(ref modality) = info.modality {
+            let label = format!("modality:{:?}", modality);
+            let mid = self.add_node(NodeKind::Subterm, &label, 1);
+            self.add_edge(node_id, mid, EdgeKind::HasModality, 1.0);
+        }
+    }
+
     /// Add shared-structure edges between premise nodes that share constants.
     ///
     /// Two premises sharing named constants likely have semantic overlap,

src/rust/provers/fstar.rs

@@ -17,6 +17,7 @@ use tokio::process::Command;
 
 use super::{ProverBackend, ProverConfig, ProverKind};
 use crate::core::{Goal, ProofState, Tactic, TacticResult, Term};
+use crate::types::{Effect, TypeInfo};
 
 /// F* backend
 pub struct FStarBackend {
@@ -33,12 +34,51 @@ impl FStarBackend {
         for (i, axiom) in state.context.axioms.iter().enumerate() {
             input.push_str(&format!("assume val axiom_{} : {}\n", i, axiom));
         }
+        // Emit definitions with effect and refinement annotations from TypeInfo
+        for def in &state.context.definitions {
+            let effect_str = def
+                .type_info
+                .as_ref()
+                .map(Self::effect_to_fstar)
+                .unwrap_or_default();
+            let refinement_str = def
+                .type_info
+                .as_ref()
+                .and_then(|ti| ti.refinement.as_ref())
+                .map(|pred| format!("{{v:{} | {}}}", def.ty, pred))
+                .unwrap_or_else(|| format!("{}", def.ty));
+            input.push_str(&format!("val {} : {}{}\n", def.name, effect_str, refinement_str));
+        }
         if let Some(goal) = state.goals.first() {
             input.push_str(&format!("\nval goal : {}\n", goal.target));
         }
         Ok(input)
     }
 
+    /// Convert effect row from [`TypeInfo`] to an F* effect annotation prefix.
+    fn effect_to_fstar(ti: &TypeInfo) -> String {
+        if ti.effects.is_empty() {
+            return String::new();
+        }
+        let effect_name = ti
+            .effects
+            .effects
+            .first()
+            .map(|e| match e {
+                Effect::Pure | Effect::Tot => "Tot",
+                Effect::IO => "IO",
+                Effect::State => "ST",
+                Effect::Exception => "Exn",
+                Effect::Div => "Div",
+                Effect::Ghost => "GTot",
+                Effect::NonDet => "ALL",
+                Effect::Async => "ALL",
+                Effect::Custom(s) => s.as_str(),
+            })
+            .unwrap_or("Tot");
+        format!("{} ", effect_name)
+    }
+
     fn parse_result(&self, output: &str) -> Result<bool> {
         let lower = output.to_lowercase();
         if lower.contains("verified") || lower.contains("all verification conditions discharged") {

src/rust/provers/idris2.rs

@@ -30,6 +30,7 @@ use crate::core::{
     Theorem,
 };
 use crate::provers::{ProverBackend, ProverConfig, ProverKind};
+use crate::types::Multiplicity;
 
 /// Idris 2 backend implementation
 pub struct Idris2Backend {
@@ -105,17 +106,6 @@ enum Idris2Term {
     AutoImplicit(String, Box<Idris2Term>),
 }
 
-/// Quantitative type theory multiplicities
-#[derive(Debug, Clone, Copy, PartialEq, Eq)]
-enum Multiplicity {
-    /// Unrestricted (0, 1, or many uses)
-    Unrestricted,
-    /// Linear (exactly 1 use)
-    Linear,
-    /// Erased (0 uses at runtime)
-    Erased,
-}
-
 impl Idris2Backend {
     pub fn new(config: ProverConfig) -> Self {
         Idris2Backend {
@@ -178,6 +168,17 @@ impl Idris2Backend {
         }
     }
 
+    /// Convert a [`Multiplicity`] to the Idris 2 QTT annotation string.
+    fn multiplicity_to_idris2(m: &Multiplicity) -> &'static str {
+        match m {
+            Multiplicity::Zero => "0",
+            Multiplicity::One | Multiplicity::Linear => "1",
+            Multiplicity::Omega | Multiplicity::Shared => "",
+            Multiplicity::Affine => "1", // closest QTT approximation
+            Multiplicity::Graded(_) => "",
+        }
+    }
+
     /// Convert universal Term to Idris 2 syntax
     fn term_to_idris2(&self, term: &Term) -> String {
         match term {
@@ -815,11 +816,17 @@ impl ProverBackend for Idris2Backend {
         output.push_str("import Data.Vect\n");
         output.push_str("import Data.Nat\n\n");
 
-        // Definitions
+        // Definitions (emit QTT multiplicity annotations when present)
         for def in &state.context.definitions {
             let ty_str = self.term_to_idris2(&def.ty);
             let body_str = self.term_to_idris2(&def.body);
-            output.push_str(&format!("{} : {}\n", def.name, ty_str));
+            let mult_prefix = def
+                .type_info
+                .as_ref()
+                .and_then(|ti| ti.multiplicity.as_ref())
+                .map(|m| format!("{} ", Self::multiplicity_to_idris2(m)))
+                .unwrap_or_default();
+            output.push_str(&format!("{}{} : {}\n", mult_prefix, def.name, ty_str));
             output.push_str(&format!("{} = {}\n\n", def.name, body_str));
         }
 
@@ -1210,7 +1217,7 @@ mod tests {
         // Test Pi type
         let pi_term = Idris2Term::Pi(
             "a".to_string(),
-            Multiplicity::Unrestricted,
+            Multiplicity::Omega,
             Box::new(Idris2Term::Type),
             Box::new(Idris2Term::Var("a".to_string())),
         );

src/rust/provers/mod.rs

@@ -63,6 +63,7 @@ pub mod mizar;
 pub mod nuprl;
 pub mod nusmv;
 pub mod ortools;
+pub mod outcome;
 pub mod prism;
 pub mod proverif;
 pub mod pvs;