Skip to content

Commit 26b96ad

Browse files
claudeclaude
committed
feat(types): add native type-system decoration layer + Sigma variant
Introduces a unified native type-system layer so backends that already understand richer type disciplines can expose that understanding through ECHIDNA's IR instead of delegating opaquely. This is Step 1 + Step 2 of the plan: the low-risk foundation; per-backend wiring (Step 3) can follow incrementally. Changes: 1. Core IR gap closed: adds `Term::Sigma` (dependent pair / Σ type) as the dual of `Term::Pi`. Pi-only was a genuine IR gap — dependent products were representable but dependent pairs were not. 2. New `src/rust/types/` module with `TypeInfo` — an optional sidecar decoration attachable to `Hypothesis`, `Definition`, and `Variable`. `TypeInfo` spans eight dimensions: - `Universe` (level + cumulativity + impredicativity + HoTT n-level) - `Multiplicity` (QTT Zero/One/Omega, Linear, Affine, Shared, Graded(n)) - `EffectRow` (row-polymorphic algebraic effects: IO, State, Exception, NonDet, Async, Div, Ghost, Tot, Custom) - `refinement: Term` (refinement predicate {x:T | P x}) - `Modality` (alethic Box/Diamond; epistemic Knows/Believes; Common, Distributed; deontic Obligation/Permission; Provability; Custom) - `TemporalOp` (LTL G/F/X/U/R, past-time Since/Triggered, CTL AG/EG/AF/EF/AX/EX, μ-calculus Mu/Nu) - `Semiring` (Boolean, Natural, Tropical {min-plus/max-plus}, Viterbi, Lukasiewicz, Custom) - `relational_arity` (1 = ordinary, 2 = dyadic/parametric, n = n-ary) All decorations are optional — backends that don't understand a field simply ignore it. `TypeInfo::default()` is the no-decoration case and serialises as `{}`. 3. Plumbing: `Hypothesis`, `Definition`, and `Variable` gain an optional `type_info: Option<TypeInfo>` field with `#[serde(default, skip_serializing_if)]` so prior-format JSON still deserialises cleanly. Added `new()` and `with_type_info()` constructor helpers on all three structs. 4. Sigma rendering wired into every backend that renders `Pi`: - Lean: `(x : A) × B` - Agda: `Σ A λ x → B` - Idris2: `(x : A ** B)` - HOL4: existential approximation (no native Σ) - HOL Light: existential approximation - Mizar: `ex x being A st B` - PVS: `EXISTS` approximation - ACL2: `(and A B)` approximation Also wired into aspect tagging (new `sigma_count` TheoremFeatures field aggregated into `Aspect::DependentTypes`), GNN graph construction (sigma binder nodes), and GNN one-hot embeddings (index 13 reserved). 5. Tests: 11 new unit tests in `src/rust/types/mod.rs` covering multiplicity attachment, effect-row composition, epistemic modality, tropical semiring, refinement predicates, HoTT universe levels, dyadic relational arity, JSON roundtripping, empty-decoration compactness, Sigma rendering+roundtrip, and backwards-compatible deserialisation of prior-format Hypothesis JSON without `type_info`. What this enables (follow-on work, not in this commit): - Idris2 backend reading `multiplicity` → emits 0/1/ω bindings - F* backend reading `effects` + `refinement` - Lean 4 reading `universe.impredicative` / `homotopy_level` - PVS reading `refinement` → predicate subtype - SPIN/NuSMV/PRISM reading `temporal` - Alloy reading `relational_arity` - Future epistemic / tropical backends reading `modality` / `semiring` - GNN guided search discriminating on type-info features Compatibility: - All changes are additive. `Option<TypeInfo>` is None by default; existing code paths are unchanged. - ~40 struct-literal construction sites updated to include `type_info: None` — mechanical, inspected change. Note: a pre-existing unrelated build issue exists in `src/rust/provers/z3.rs` (`super::outcome::ProverOutcome` references a module that does not exist in `src/rust/provers/`, and an orphan `async fn check` outside the `ProverBackend` trait). Verified to exist on a clean tree prior to this commit; this change does not regress it. https://claude.ai/code/session_01FYkVX52Tdn6Arp9dWfPLxq
1 parent aaeef38 commit 26b96ad

30 files changed

Lines changed: 744 additions & 2 deletions

‎src/rust/agent/explanations.rs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -301,6 +301,18 @@ impl ExplanationGenerator {
301301
self.format_term(body)
302302
)
303303
},
304+
Term::Sigma {
305+
param,
306+
param_type,
307+
body,
308+
} => {
309+
format!(
310+
"∃{}:{}. {}",
311+
param,
312+
self.format_term(param_type),
313+
self.format_term(body)
314+
)
315+
},
304316
Term::App { func, args } => {
305317
let args_str: Vec<_> = args.iter().map(|a| self.format_term(a)).collect();
306318
format!("({} {})", self.format_term(func), args_str.join(" "))

‎src/rust/aspect.rs‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -419,6 +419,9 @@ pub struct TheoremFeatures {
419419
/// Pi type (dependent function) count
420420
pub pi_count: usize,
421421

422+
/// Sigma type (dependent pair) count
423+
pub sigma_count: usize,
424+
422425
/// Universe levels used
423426
pub universe_levels: HashSet<usize>,
424427

@@ -652,6 +655,9 @@ impl RuleBasedTagger {
652655
},
653656
Term::Pi {
654657
param_type, body, ..
658+
}
659+
| Term::Sigma {
660+
param_type, body, ..
655661
} => {
656662
self.extract_symbols_recursive(param_type, symbols);
657663
self.extract_symbols_recursive(body, symbols);
@@ -748,6 +754,11 @@ impl AspectTagger for RuleBasedTagger {
748754
total_matches += features.pi_count;
749755
}
750756

757+
if features.sigma_count > 0 {
758+
*aspect_counts.entry(Aspect::DependentTypes).or_insert(0) += features.sigma_count;
759+
total_matches += features.sigma_count;
760+
}
761+
751762
if !features.universe_levels.is_empty() {
752763
*aspect_counts.entry(Aspect::Universes).or_insert(0) += 1;
753764
total_matches += 1;
@@ -809,6 +820,13 @@ impl RuleBasedTagger {
809820
self.analyze_term(param_type, features, depth + 1);
810821
self.analyze_term(body, features, depth + 1);
811822
},
823+
Term::Sigma {
824+
param_type, body, ..
825+
} => {
826+
features.sigma_count += 1;
827+
self.analyze_term(param_type, features, depth + 1);
828+
self.analyze_term(body, features, depth + 1);
829+
},
812830
Term::Universe(level) | Term::Type(level) | Term::Sort(level) => {
813831
features.universe_levels.insert(*level);
814832
},

‎src/rust/core.rs‎

Lines changed: 73 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33

44
//! Core types and abstractions for ECHIDNA theorem proving
55
6+
use crate::types::TypeInfo;
67
use serde::{Deserialize, Serialize};
78
use std::collections::HashMap;
89
use std::fmt;
@@ -33,6 +34,17 @@ pub enum Term {
3334
body: Box<Term>,
3435
},
3536

37+
/// Dependent pair / sum (Sigma type) Σ(x: A). B
38+
///
39+
/// Represents dependent pairs where the type of the second component may
40+
/// depend on the value of the first. Non-dependent pairs are expressible
41+
/// as `Sigma { body }` where `body` does not mention `param`.
42+
Sigma {
43+
param: String,
44+
param_type: Box<Term>,
45+
body: Box<Term>,
46+
},
47+
3648
/// Type universe at level
3749
Type(usize),
3850

@@ -121,6 +133,13 @@ impl fmt::Display for Term {
121133
} => {
122134
write!(f, "(Π {}: {}. {})", param, param_type, body)
123135
},
136+
Term::Sigma {
137+
param,
138+
param_type,
139+
body,
140+
} => {
141+
write!(f, "(Σ {}: {}. {})", param, param_type, body)
142+
},
124143
Term::Type(level) => write!(f, "Type{}", level),
125144
Term::Sort(level) => write!(f, "Sort{}", level),
126145
Term::Universe(level) => write!(f, "Type{}", level),
@@ -190,6 +209,26 @@ pub struct Hypothesis {
190209

191210
/// Optional body (for definitions)
192211
pub body: Option<Term>,
212+
213+
/// Optional native type-system decoration (multiplicity, effects, modality,
214+
/// refinement, semiring, …). `None` is semantically equivalent to a plain
215+
/// unannotated hypothesis — backends that don't understand the decoration
216+
/// safely ignore it.
217+
#[serde(default, skip_serializing_if = "Option::is_none")]
218+
pub type_info: Option<TypeInfo>,
219+
}
220+
221+
impl Hypothesis {
222+
/// Construct a plain hypothesis with no type decoration.
223+
pub fn new(name: impl Into<String>, ty: Term) -> Self {
224+
Self { name: name.into(), ty, body: None, type_info: None }
225+
}
226+
227+
/// Attach a [`TypeInfo`] decoration.
228+
pub fn with_type_info(mut self, info: TypeInfo) -> Self {
229+
self.type_info = Some(info);
230+
self
231+
}
193232
}
194233

195234
/// Proof context with available premises
@@ -223,13 +262,47 @@ pub struct Definition {
223262
pub name: String,
224263
pub ty: Term,
225264
pub body: Term,
265+
266+
/// Optional native type-system decoration (see [`TypeInfo`]).
267+
#[serde(default, skip_serializing_if = "Option::is_none")]
268+
pub type_info: Option<TypeInfo>,
269+
}
270+
271+
impl Definition {
272+
/// Construct a plain definition with no type decoration.
273+
pub fn new(name: impl Into<String>, ty: Term, body: Term) -> Self {
274+
Self { name: name.into(), ty, body, type_info: None }
275+
}
276+
277+
/// Attach a [`TypeInfo`] decoration.
278+
pub fn with_type_info(mut self, info: TypeInfo) -> Self {
279+
self.type_info = Some(info);
280+
self
281+
}
226282
}
227283

228284
/// A variable declaration
229285
#[derive(Debug, Clone, Serialize, Deserialize)]
230286
pub struct Variable {
231287
pub name: String,
232288
pub ty: Term,
289+
290+
/// Optional native type-system decoration (see [`TypeInfo`]).
291+
#[serde(default, skip_serializing_if = "Option::is_none")]
292+
pub type_info: Option<TypeInfo>,
293+
}
294+
295+
impl Variable {
296+
/// Construct a plain variable with no type decoration.
297+
pub fn new(name: impl Into<String>, ty: Term) -> Self {
298+
Self { name: name.into(), ty, type_info: None }
299+
}
300+
301+
/// Attach a [`TypeInfo`] decoration.
302+
pub fn with_type_info(mut self, info: TypeInfo) -> Self {
303+
self.type_info = Some(info);
304+
self
305+
}
233306
}
234307

235308
/// A proof tactic/command

‎src/rust/gnn/embeddings.rs‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -350,6 +350,7 @@ fn term_kind_index(term: &Term) -> usize {
350350
Term::Hole(_) => 10,
351351
Term::Meta(_) => 11,
352352
Term::ProverSpecific { .. } => 12,
353+
Term::Sigma { .. } => 13,
353354
}
354355
}
355356

@@ -367,7 +368,8 @@ fn term_depth(term: &Term) -> usize {
367368
let pt = param_type.as_ref().map(|t| term_depth(t)).unwrap_or(0);
368369
1 + pt.max(term_depth(body))
369370
}
370-
Term::Pi { param_type, body, .. } => {
371+
Term::Pi { param_type, body, .. }
372+
| Term::Sigma { param_type, body, .. } => {
371373
1 + term_depth(param_type).max(term_depth(body))
372374
}
373375
Term::Let { ty, value, body, .. } => {
@@ -394,7 +396,7 @@ fn term_arity(term: &Term) -> usize {
394396
| Term::Universe(_) | Term::Hole(_) | Term::Meta(_) | Term::ProverSpecific { .. } => 0,
395397
Term::App { args, .. } => 1 + args.len(), // func + args
396398
Term::Lambda { param_type, .. } => if param_type.is_some() { 2 } else { 1 },
397-
Term::Pi { .. } => 2, // param_type + body
399+
Term::Pi { .. } | Term::Sigma { .. } => 2, // param_type + body
398400
Term::Let { ty, .. } => if ty.is_some() { 3 } else { 2 },
399401
Term::Match { branches, .. } => 1 + branches.len(),
400402
Term::Fix { ty, .. } => if ty.is_some() { 2 } else { 1 },

‎src/rust/gnn/graph.rs‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -372,6 +372,23 @@ impl ProofGraphBuilder {
372372
}
373373
Some(nid)
374374
}
375+
Term::Sigma {
376+
param,
377+
param_type,
378+
body,
379+
} => {
380+
let label = format!("sigma_{}", param);
381+
let nid = self.add_node(NodeKind::Binder, &label, depth);
382+
self.add_edge(parent_id, nid, EdgeKind::Contains, 1.0);
383+
384+
if let Some(tid) = self.expand_term(param_type, nid, depth + 1) {
385+
self.add_edge(nid, tid, EdgeKind::HasType, 1.0);
386+
}
387+
if let Some(bid) = self.expand_term(body, nid, depth + 1) {
388+
self.add_edge(nid, bid, EdgeKind::BindsOver, 1.0);
389+
}
390+
Some(nid)
391+
}
375392
Term::Type(level) | Term::Sort(level) | Term::Universe(level) => {
376393
let label = format!("Type{}", level);
377394
let nid = self.add_or_get_node(NodeKind::TypeExpr, &label, depth);
@@ -642,6 +659,7 @@ mod tests {
642659
name: "h_nat".to_string(),
643660
ty: Term::Const("Nat".to_string()),
644661
body: None,
662+
type_info: None,
645663
};
646664

647665
let theorem = Theorem {
@@ -687,6 +705,7 @@ mod tests {
687705
variables: vec![Variable {
688706
name: "n".to_string(),
689707
ty: Term::Const("Nat".to_string()),
708+
type_info: None,
690709
}],
691710
},
692711
proof_script: Vec::new(),

‎src/rust/gnn/guided_search.rs‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -381,6 +381,7 @@ mod tests {
381381
name: "h".to_string(),
382382
ty: Term::Const("Nat".to_string()),
383383
body: None,
384+
type_info: None,
384385
}],
385386
}],
386387
context: Context {
@@ -390,6 +391,7 @@ mod tests {
390391
variables: vec![Variable {
391392
name: "n".to_string(),
392393
ty: Term::Const("Nat".to_string()),
394+
type_info: None,
393395
}],
394396
},
395397
proof_script: Vec::new(),

‎src/rust/lib.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ pub mod parsers;
2424
pub mod proof_encoding; // CBOR encoding + proof identity hashing
2525
pub mod proof_search; // Chapel parallel proof search (optional feature)
2626
pub mod provers;
27+
pub mod types; // Native type-system decorations (multiplicity, effects, modality, temporal, semiring, …)
2728
pub mod verification;
2829
#[cfg(feature = "verisim")]
2930
pub mod verisim_bridge; // VeriSimDB 8-modality octad integration

‎src/rust/provers/abc.rs‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -269,6 +269,7 @@ impl AbcBackend {
269269
name: input_name.to_string(),
270270
ty: Term::Const("BLIF_INPUT".to_string()),
271271
body: Term::Const(input_name.to_string()),
272+
type_info: None,
272273
});
273274
}
274275
}

‎src/rust/provers/acl2.rs‎

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -980,6 +980,18 @@ impl ACL2Backend {
980980
])
981981
}
982982
},
983+
Term::Sigma {
984+
param: _,
985+
param_type,
986+
body,
987+
} => {
988+
// ACL2 has no dependent pairs; approximate with (and A B).
989+
SExp::List(vec![
990+
SExp::Atom("and".to_string()),
991+
self.term_to_sexp(param_type),
992+
self.term_to_sexp(body),
993+
])
994+
},
983995
Term::Let {
984996
name, value, body, ..
985997
} => SExp::List(vec![
@@ -1250,6 +1262,7 @@ impl ProverBackend for ACL2Backend {
12501262
name,
12511263
ty: Term::Universe(0), // ACL2 doesn't have explicit types
12521264
body: body_term,
1265+
type_info: None,
12531266
});
12541267
},
12551268
ACL2Event::Defthm {
@@ -1291,6 +1304,7 @@ impl ProverBackend for ACL2Backend {
12911304
name,
12921305
ty: Term::Universe(0),
12931306
body: value_term,
1307+
type_info: None,
12941308
});
12951309
},
12961310
_ => {},

‎src/rust/provers/agda.rs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -134,6 +134,16 @@ impl AgdaBackend {
134134
let body_str = self.term_to_agda(body);
135135
format!("({} : {}) → {}", param, param_ty_str, body_str)
136136
},
137+
Term::Sigma {
138+
param,
139+
param_type,
140+
body,
141+
} => {
142+
// Agda: Σ A λ x → B (standard-library)
143+
let param_ty_str = self.term_to_agda(param_type);
144+
let body_str = self.term_to_agda(body);
145+
format!("Σ {} λ {} → {}", param_ty_str, param, body_str)
146+
},
137147
Term::Universe(level) | Term::Type(level) => {
138148
if *level == 0 {
139149
"Set".to_string()
@@ -263,6 +273,7 @@ impl ProverBackend for AgdaBackend {
263273
name: name.clone(),
264274
ty: type_term.clone(),
265275
body: type_term,
276+
type_info: None,
266277
});
267278
},
268279
AgdaDecl::TypeSig { name, ty } => {
@@ -318,6 +329,7 @@ impl ProverBackend for AgdaBackend {
318329
name: param_name,
319330
ty: Term::Universe(0),
320331
body: None,
332+
type_info: None,
321333
});
322334
}
323335
Ok(TacticResult::Success(new_state))

0 commit comments

Comments
 (0)