Merge pull request #2 from hyperpolymath/feat/tier3-prover-coverage

feat(trust+executor): Tier-3 prover coverage

Author: hyperpolymath

src/executor/container.rs

@@ -640,6 +640,16 @@ fn prover_extension(prover: &ProverKind) -> String {
         "pvs" => ".pvs".to_string(),
         "acl2" => ".lisp".to_string(),
         "hol4" => ".sml".to_string(),
+        // Tier-3 dependent-type / VC / ATP / protocol-checker systems
+        "idris2" | "idris" => ".idr".to_string(),
+        "fstar" => ".fst".to_string(),
+        "dafny" => ".dfy".to_string(),
+        "why3" => ".mlw".to_string(),
+        "vampire" | "eprover" | "spass" => ".p".to_string(),
+        "tamarin" => ".spthy".to_string(),
+        "proverif" => ".pv".to_string(),
+        "dreal" | "alt-ergo" => ".smt2".to_string(),
+        "abc" => ".aig".to_string(),
         _ => ".txt".to_string(),  // Default for unknown provers
     }
 }
@@ -678,6 +688,18 @@ mod tests {
         assert_eq!(prover_extension(&ProverKind::new("metamath")), ".mm");
         assert_eq!(prover_extension(&ProverKind::new("z3")), ".smt2");
         assert_eq!(prover_extension(&ProverKind::new("agda")), ".agda");
+
+        // Tier-3
+        assert_eq!(prover_extension(&ProverKind::new("idris2")), ".idr");
+        assert_eq!(prover_extension(&ProverKind::new("fstar")), ".fst");
+        assert_eq!(prover_extension(&ProverKind::new("dafny")), ".dfy");
+        assert_eq!(prover_extension(&ProverKind::new("why3")), ".mlw");
+        assert_eq!(prover_extension(&ProverKind::new("vampire")), ".p");
+        assert_eq!(prover_extension(&ProverKind::new("eprover")), ".p");
+        assert_eq!(prover_extension(&ProverKind::new("tamarin")), ".spthy");
+        assert_eq!(prover_extension(&ProverKind::new("proverif")), ".pv");
+        assert_eq!(prover_extension(&ProverKind::new("dreal")), ".smt2");
+        assert_eq!(prover_extension(&ProverKind::new("abc")), ".aig");
     }
 
     #[test]

src/trust/confidence.rs

@@ -204,6 +204,16 @@ pub fn is_small_kernel(prover: &ProverKind) -> bool {
         "acl2" => false,     // Built on Common Lisp
         "hol4" => true,      // Small ML kernel
 
+        // Tier-3 small-kernel systems
+        "idris2" | "idris" => true,  // Dependent-type kernel
+        "fstar" => true,             // F* type-theory kernel
+
+        // Tier-3 large-TCB systems
+        "vampire" | "eprover" | "spass" => false,  // Large first-order ATPs
+        "dafny" | "why3" | "alt-ergo" => false,    // VC-based tools
+        "tamarin" | "proverif" => false,           // Protocol model checkers
+        "dreal" | "abc" => false,                  // Numerical / hardware checkers
+
         // Unknown provers: assume false (conservative estimate)
         _ => false,
     }
@@ -251,6 +261,19 @@ mod tests {
         assert!(!is_small_kernel(&ProverKind::new("mizar")));
         assert!(!is_small_kernel(&ProverKind::new("pvs")));
         assert!(!is_small_kernel(&ProverKind::new("acl2")));
+
+        // Tier-3 small-kernel
+        assert!(is_small_kernel(&ProverKind::new("idris2")));
+        assert!(is_small_kernel(&ProverKind::new("fstar")));
+
+        // Tier-3 large-TCB
+        assert!(!is_small_kernel(&ProverKind::new("vampire")));
+        assert!(!is_small_kernel(&ProverKind::new("eprover")));
+        assert!(!is_small_kernel(&ProverKind::new("dafny")));
+        assert!(!is_small_kernel(&ProverKind::new("why3")));
+        assert!(!is_small_kernel(&ProverKind::new("tamarin")));
+        assert!(!is_small_kernel(&ProverKind::new("proverif")));
+        assert!(!is_small_kernel(&ProverKind::new("dreal")));
     }
 
     #[test]