icarus_lowerable: reassess asp_solver and ternary_logic witnesses after #10370 (Closes #10450)

bootstrap/tests/icarus_lowerable.rs

@@ -7584,15 +7584,15 @@ fn lowerability_models_keep_real_source_signatures() {
             ("pub fn sacred_scale() -> f64", r#"{ name := "sacred_scale", params := [], ret := (some (.struct "f64")), body := [] }"#),
         ]),
         ("ar_asp_solver", "specs/ar/asp_solver.t27", vec![
-            ("pub struct Program { pub clauses: Vec<Clause>, pub constraints: Vec<Clause>, }", r#"structs := [("Program", [("clauses", (.struct "[Clause]")), ("constraints", (.struct "[Clause]"))])]"#),
-            ("pub fn solve(prog: Program) -> Vec<AnswerSet>", r#"{ name := "solve", params := [("prog", (.struct "Program"))], ret := (some (.struct "[AnswerSet]")), body := [] }"#),
+            ("pub struct Program { pub clauses: [Clause; MAX_CLAUSES as usize], pub nclauses: u32, pub constraints: [Clause; MAX_CLAUSES as usize], pub nconstraints: u32, }", r#"("Program", [("clauses", (.array 16 (.struct "Clause"))), ("nclauses", .u32), ("constraints", (.array 16 (.struct "Clause"))), ("nconstraints", .u32)])"#),
+            ("pub fn solve(prog: Program) -> SolveResult", r#"{ name := "solve", params := [("prog", (.struct "Program"))], ret := (some (.struct "SolveResult")), body := [] }"#),
         ]),
         // #6658: the model was empty and proved the empty module lowerable.
         ("ar_ternary_logic", "specs/ar/ternary_logic.t27", vec![
-            ("pub fn k3_and(a: Trit, b: Trit) -> Trit", r#"{ name := "k3_and", params := [("a", (.struct "Trit")), ("b", (.struct "Trit"))], ret := (some (.struct "Trit")), body := [] }"#),
-            ("pub fn backward_chain(goal: Trit, rules: Vec<Rule>) -> Trit", r#"{ name := "backward_chain", params := [("goal", (.struct "Trit")), ("rules", (.struct "[Rule]"))], ret := (some (.struct "Trit")), body := [] }"#),
-            ("pub fn resolve(clause_a: Vec<Trit>, clause_b: Vec<Trit>) -> Vec<Trit>", r#"{ name := "resolve", params := [("clause_a", (.struct "[Trit]")), ("clause_b", (.struct "[Trit]"))], ret := (some (.struct "[Trit]")), body := [] }"#),
-            ("pub fn apply_restraint(values: Vec<Trit>) -> Vec<Trit>", r#"{ name := "apply_restraint", params := [("values", (.struct "[Trit]"))], ret := (some (.struct "[Trit]")), body := [] }"#),
+            ("pub fn k3_and(a: i8, b: i8) -> i8", r#"{ name := "k3_and", params := [("a", .i8), ("b", .i8)], ret := (some .i8), body := [] }"#),
+            ("pub fn backward_chain(goal: i8, rules: Vec<Rule>) -> i8", r#"{ name := "backward_chain", params := [("goal", .i8), ("rules", (.struct "[]const Rule"))], ret := (some .i8), body := [] }"#),
+            ("pub fn resolve(clause_a: impl AsRef<[i8]>, clause_b: impl AsRef<[i8]>) -> Vec<i8>", r#"{ name := "resolve", params := [("clause_a", (.struct "[]const i8")), ("clause_b", (.struct "[]const i8"))], ret := (some (.struct "[]i8")), body := [] }"#),
+            ("pub fn apply_restraint(values: impl AsRef<[i8]>) -> Vec<i8>", r#"{ name := "apply_restraint", params := [("values", (.struct "[]const i8"))], ret := (some (.struct "[]i8")), body := [] }"#),
         ]),
     ] {
         let output = Command::new(bin()).arg("gen-rust").arg(repo.join(source))

proofs/lean4/Trinity/IcarusLowerable/Completeness.lean

@@ -40,12 +40,15 @@ def api_tri_net_api_module : Module := {
   benches := [{ name := "", params := [], ret := none, body := [] }, { name := "", params := [], ret := none, body := [] }]
 }
 
--- Negative signature projection from specs/ar/asp_solver.t27. Program has
--- variable-length Clause fields and solve returns variable-length AnswerSet.
--- This shallow AST keeps these unmodeled types under their source names.
--- The old unused marker left an empty module; it could not prove false.
+-- Negative signature projection from specs/ar/asp_solver.t27. Since #8980 its
+-- arrays are fixed (MAX_CLAUSES 16, MAX_CLAUSE_LITS 4, MAX_LARGS 2, MAX_LITS 16,
+-- MAX_ANSWERS 4); `string` (Literal.name/args, reached via Clause) keeps it
+-- unlowerable. Function bodies are left out.
 def ar_asp_solver_env : Env := {
-  structs := [("Program", [("clauses", (.struct "[Clause]")), ("constraints", (.struct "[Clause]"))])],
+  structs := [
+    ("Literal", [("name", .string), ("is_negated", .bool), ("args", (.array 2 .string)), ("nargs", .u32)]), ("Clause", [("lits", (.array 4 (.struct "Literal"))), ("count", .u32)]), ("LitList", [("items", (.array 16 (.struct "Literal"))), ("count", .u32)]),
+    ("Program", [("clauses", (.array 16 (.struct "Clause"))), ("nclauses", .u32), ("constraints", (.array 16 (.struct "Clause"))), ("nconstraints", .u32)]),
+    ("AnswerSet", [("literals", (.struct "LitList")), ("proven", .bool), ("cost", .i32)]), ("SolveResult", [("answers", (.array 4 (.struct "AnswerSet"))), ("count", .u32), ("steps", .u32), ("trace_len", .u32)])],
   constructors := [],
   enums := [],
   imports := [],
@@ -57,7 +60,7 @@ def ar_asp_solver_module : Module := {
   name := "ar_asp_solver",
   imports := [],
   globals := [],
-  functions := [{ name := "solve", params := [("prog", (.struct "Program"))], ret := (some (.struct "[AnswerSet]")), body := [] }],
+  functions := [{ name := "solve", params := [("prog", (.struct "Program"))], ret := (some (.struct "SolveResult")), body := [] }],
   tests := [],
   benches := []
 }
@@ -171,22 +174,13 @@ def ar_restraint_module : Module := {
 }
 
 -- Negative signature projection from specs/ar/ternary_logic.t27 (#6658).
--- The previous model was EMPTY (no functions, globals or tests), so
--- `native_decide` proved the empty module lowerable -- true of nothing in
--- the spec. This one keeps every declaration the classifier reads, with
--- unmodeled types under their source names, as ar_asp_solver does:
---   * `Trit` is neither a primitive nor a struct declared in this module,
---     so the Rust classifier already rejects k3_and's interface, and the
---     Lean predicate rejects `.struct "Trit"` (not in `structs`).
---   * resolve and apply_restraint take and return variable-length `[Trit]`;
---     backward_chain takes variable-length `[Rule]`. Those three stay
---     unlowerable even when `Trit` is declared as a lowerable type -- see
---     `ar_ternary_logic_slices_block_with_trit_declared` below.
--- Function bodies are left out (as for ar_asp_solver): the interfaces
--- alone decide the verdict, and they are the part a regenerated signature
--- can be compared against. Tests and benches carry the spec's names.
+-- Since #8980 a Trit is an `i8` (-1, 0, +1), so the scalar K3 functions are
+-- lowerable. Unlowerable, by name under their source types: resolve,
+-- apply_restraint and backward_chain (variable-length slices, no fixed width;
+-- see `ar_ternary_logic_slices_block`) and pool_take (`usize`). Bodies are
+-- left out; the interfaces alone decide.
 def ar_ternary_logic_env : Env := {
-  structs := [("Rule", [("antecedent", (.struct "Trit")), ("consequent", (.struct "Trit"))])],
+  structs := [("Rule", [("antecedent", .i8), ("consequent", .i8)])],
   constructors := [],
   enums := [],
   imports := [],
@@ -197,24 +191,19 @@ def ar_ternary_logic_env : Env := {
 def ar_ternary_logic_module : Module := {
   name := "ar_ternary_logic",
   imports := [],
-  globals := [.constDecl "K_FALSE" (.struct "Trit") (some (.enumVal "Trit" "FALSE")), .constDecl "K_UNKNOWN" (.struct "Trit") (some (.enumVal "Trit" "UNKNOWN")), .constDecl "K_TRUE" (.struct "Trit") (some (.enumVal "Trit" "TRUE"))],
-  functions := [{ name := "k3_and", params := [("a", (.struct "Trit")), ("b", (.struct "Trit"))], ret := (some (.struct "Trit")), body := [] }, { name := "k3_or", params := [("a", (.struct "Trit")), ("b", (.struct "Trit"))], ret := (some (.struct "Trit")), body := [] }, { name := "k3_not", params := [("a", (.struct "Trit"))], ret := (some (.struct "Trit")), body := [] }, { name := "k3_implies", params := [("a", (.struct "Trit")), ("b", (.struct "Trit"))], ret := (some (.struct "Trit")), body := [] }, { name := "k3_equiv", params := [("a", (.struct "Trit")), ("b", (.struct "Trit"))], ret := (some (.struct "Trit")), body := [] }, { name := "forward_chain", params := [("rule", (.struct "Rule")), ("fact", (.struct "Trit"))], ret := (some (.struct "Trit")), body := [] }, { name := "backward_chain", params := [("goal", (.struct "Trit")), ("rules", (.struct "[Rule]"))], ret := (some (.struct "Trit")), body := [] }, { name := "resolve", params := [("clause_a", (.struct "[Trit]")), ("clause_b", (.struct "[Trit]"))], ret := (some (.struct "[Trit]")), body := [] }, { name := "is_restraint", params := [("t", (.struct "Trit"))], ret := (some .bool), body := [] }, { name := "apply_restraint", params := [("values", (.struct "[Trit]"))], ret := (some (.struct "[Trit]")), body := [] }],
+  globals := [.constDecl "K_FALSE" .i8 (some (.intLit (-1))), .constDecl "K_UNKNOWN" .i8 (some (.intLit 0)), .constDecl "K_TRUE" .i8 (some (.intLit 1)), .constDecl "K3_VALUES" (.array 3 .i8) (some (.arrayLit .i8 [(.identifier "K_FALSE"), (.identifier "K_UNKNOWN"), (.identifier "K_TRUE")])), .varDecl "trit_pool" (.array 256 .i8) none, .varDecl "trit_pool_used" (.struct "usize") (some (.intLit 0))],
+  functions := [{ name := "pool_take", params := [("n", (.struct "usize"))], ret := (some (.struct "usize")), body := [] }, { name := "holds", params := [("t", .i8)], ret := (some .bool), body := [] }, { name := "k3_and", params := [("a", .i8), ("b", .i8)], ret := (some .i8), body := [] }, { name := "k3_or", params := [("a", .i8), ("b", .i8)], ret := (some .i8), body := [] }, { name := "k3_not", params := [("a", .i8)], ret := (some .i8), body := [] }, { name := "k3_implies", params := [("a", .i8), ("b", .i8)], ret := (some .i8), body := [] }, { name := "k3_equiv", params := [("a", .i8), ("b", .i8)], ret := (some .i8), body := [] }, { name := "forward_chain", params := [("rule", (.struct "Rule")), ("fact", .i8)], ret := (some .i8), body := [] }, { name := "backward_chain", params := [("goal", .i8), ("rules", (.struct "[]const Rule"))], ret := (some .i8), body := [] }, { name := "resolve", params := [("clause_a", (.struct "[]const i8")), ("clause_b", (.struct "[]const i8"))], ret := (some (.struct "[]i8")), body := [] }, { name := "is_restraint", params := [("t", .i8)], ret := (some .bool), body := [] }, { name := "apply_restraint", params := [("values", (.struct "[]const i8"))], ret := (some (.struct "[]i8")), body := [] }],
   tests := [{ name := "k3_and_truth_table", params := [], ret := none, body := [] }, { name := "k3_or_truth_table", params := [], ret := none, body := [] }, { name := "k3_not_truth_table", params := [], ret := none, body := [] }, { name := "k3_no_tautology_or_not_false", params := [], ret := none, body := [] }, { name := "k3_no_tautology_or_not_true", params := [], ret := none, body := [] }, { name := "k3_no_tautology_or_not_unknown_violation", params := [], ret := none, body := [] }, { name := "k3_no_tautology_exists_violating_value", params := [], ret := none, body := [] }, { name := "k3_no_tautology_all_values_tested", params := [], ret := none, body := [] }, { name := "k3_restraint_from_no_tautology", params := [], ret := none, body := [] }, { name := "k3_implication_ex_falso", params := [], ret := none, body := [] }, { name := "k3_implication_when_antecedent_true", params := [], ret := none, body := [] }, { name := "k3_implication_when_consequent_true", params := [], ret := none, body := [] }, { name := "k3_implication_with_unknown", params := [], ret := none, body := [] }, { name := "k3_equiv_reflexive", params := [], ret := none, body := [] }, { name := "k3_equiv_symmetric", params := [], ret := none, body := [] }, { name := "k3_equiv_transitive", params := [], ret := none, body := [] }, { name := "k3_equiv_when_both_true", params := [], ret := none, body := [] }, { name := "k3_equiv_when_both_false", params := [], ret := none, body := [] }, { name := "k3_equiv_when_opposite", params := [], ret := none, body := [] }, { name := "forward_chain_modus_ponens_true", params := [], ret := none, body := [] }, { name := "forward_chain_modus_ponens_false_consequent", params := [], ret := none, body := [] }, { name := "forward_chain_with_unknown_fact", params := [], ret := none, body := [] }, { name := "forward_chain_no_match", params := [], ret := none, body := [] }, { name := "backward_chain_finds_support", params := [], ret := none, body := [] }, { name := "backward_chain_no_support", params := [], ret := none, body := [] }, { name := "backward_chain_multiple_rules", params := [], ret := none, body := [] }, { name := "resolve_complementary_literals", params := [], ret := none, body := [] }, { name := "resolve_non_complementary", params := [], ret := none, body := [] }, { name := "is_restraint_true_for_unknown", params := [], ret := none, body := [] }, { name := "is_restraint_false_for_false", params := [], ret := none, body := [] }, { name := "is_restraint_false_for_true", params := [], ret := none, body := [] }, { name := "apply_restraint_replaces_unknown", params := [], ret := none, body := [] }, { name := "apply_restraint_preserves_known", params := [], ret := none, body := [] }],
   benches := [{ name := "k3_and_latency", params := [], ret := none, body := [] }, { name := "k3_or_latency", params := [], ret := none, body := [] }, { name := "k3_not_latency", params := [], ret := none, body := [] }, { name := "k3_implies_latency", params := [], ret := none, body := [] }, { name := "k3_equiv_latency", params := [], ret := none, body := [] }, { name := "forward_chain_latency", params := [], ret := none, body := [] }, { name := "backward_chain_latency", params := [], ret := none, body := [] }, { name := "resolve_latency", params := [], ret := none, body := [] }, { name := "apply_restraint_latency", params := [], ret := none, body := [] }]
 }
 
-/-- #6658: the variable-length `[Trit]` / `[Rule]` interfaces block on their
-    own. Declare `Trit` as a lowerable one-field struct and every scalar K3
-    function becomes lowerable; exactly the three functions with a slice in
-    their signature still are not. -/
-def ar_ternary_logic_trit_declared_env : Env :=
-  { ar_ternary_logic_env with
-    structs := ("Trit", [("v", .i8)]) :: ar_ternary_logic_env.structs }
-
-theorem ar_ternary_logic_slices_block_with_trit_declared :
+/-- #6658: the slice interfaces block on their own. Exactly the three functions
+    with a slice in their signature, plus `pool_take` (which takes `usize`),
+    are unlowerable; every scalar K3 function over `i8` is lowerable. -/
+theorem ar_ternary_logic_slices_block :
     (ar_ternary_logic_module.functions.filter
-        (fun f => !Function.isLowerable ar_ternary_logic_trit_declared_env f)).map (fun f => f.name)
-      = ["backward_chain", "resolve", "apply_restraint"] := by native_decide
+        (fun f => !Function.isLowerable ar_ternary_logic_env f)).map (fun f => f.name)
+      = ["pool_take", "backward_chain", "resolve", "apply_restraint"] := by native_decide
 
 def automation_wrapup_auto_env : Env := {
   structs := [],