feat(trust+executor): Tier-3 prover coverage (idris2/fstar/ATPs/protocol-checkers)

Extends the slug→string match arms added by Task E with Tier-3 systems
that ECHIDNA already routes to but echidnabot was treating as unknown.

src/executor/container.rs — prover_extension():
  idris2/idris   .idr     fstar     .fst       dafny    .dfy
  why3           .mlw     vampire   .p         eprover  .p
  spass          .p       tamarin   .spthy     proverif .pv
  dreal          .smt2    alt-ergo  .smt2      abc      .aig

src/trust/confidence.rs — is_small_kernel():
  idris2/fstar = true (dependent-type / type-theory kernels)
  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)

Tests extended in both files to cover the new entries.

Closes the Tier-3 portion of the abandoned PR #1; the compile-fix
portion of that PR was independently superseded by 42e7bde with a
cleaner approach.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

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]