fix(kani): regenerate generated harnesses and update verif artifacts

Regenerated harnesses now use kani_depth1() for String params.
Creusot COMA artifacts updated to match.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Author: crumplecup

crates/elicit_proofs/src/kani/diag.rs

@@ -222,7 +222,14 @@ fn diag_explain_ready_non_explain_view() {
     let proof = elicitation::contracts::Established::<ArchivePanelConsistent>::assert();
     let plan = ExplainPlan::kani_depth0();
     let mode = ExplainNodeMode::kani_depth0();
-    let _ = explain_ready(state, proof, String::kani_depth1(), String::kani_depth1(), plan, mode);
+    let _ = explain_ready(
+        state,
+        proof,
+        String::kani_depth1(),
+        String::kani_depth1(),
+        plan,
+        mode,
+    );
 }
 
 /// Theory Q: explain_ready with ExplainView state but drop the result immediately.

crates/elicit_proofs/src/kani/gallery/level18.rs

@@ -102,11 +102,15 @@ pub fn g18_rename(state: G18State, new_label: String) -> G18State {
 #[kani::proof_for_contract(g18_rename)]
 fn gallery18a_vacuous_empty() {
     // Witness (depth2-equivalent): active with empty label — assume will prune
-    let witness = G18State::Active { label: String::new() };
+    let witness = G18State::Active {
+        label: String::new(),
+    };
     kani::assume(g18_consistent(&witness));
     forget(witness);
     // Actual input (depth1-equivalent): also empty — same problem
-    let state = G18State::Active { label: String::new() };
+    let state = G18State::Active {
+        label: String::new(),
+    };
     let new_label = String::from("b");
     let result = g18_rename(state, new_label);
     forget(result);
@@ -126,11 +130,15 @@ fn gallery18a_vacuous_empty() {
 #[kani::proof_for_contract(g18_rename)]
 fn gallery18b_literal_depth1_nonempty() {
     // Witness: depth2-equivalent, non-empty so assume passes, then forgotten
-    let witness = G18State::Active { label: String::from("ab") };
+    let witness = G18State::Active {
+        label: String::from("ab"),
+    };
     kani::assume(g18_consistent(&witness));
     forget(witness);
     // Actual input: depth1-equivalent with concrete non-empty string
-    let state = G18State::Active { label: String::from("a") };
+    let state = G18State::Active {
+        label: String::from("a"),
+    };
     let new_label = String::from("b");
     let result = g18_rename(state, new_label);
     forget(result);
@@ -147,10 +155,14 @@ fn gallery18b_literal_depth1_nonempty() {
 #[cfg(kani)]
 #[kani::proof_for_contract(g18_rename)]
 fn gallery18c_literal_depth1_drop() {
-    let witness = G18State::Active { label: String::from("ab") };
+    let witness = G18State::Active {
+        label: String::from("ab"),
+    };
     kani::assume(g18_consistent(&witness));
     forget(witness);
-    let state = G18State::Active { label: String::from("a") };
+    let state = G18State::Active {
+        label: String::from("a"),
+    };
     let new_label = String::from("b");
     // result is dropped here (not forgotten) — exercises DFCC's free check
     let _result = g18_rename(state, new_label);
@@ -165,7 +177,9 @@ fn gallery18c_literal_depth1_drop() {
 #[cfg(kani)]
 #[kani::proof_for_contract(g18_rename)]
 fn gallery18d_symbolic_depth2_drop() {
-    let witness = G18State::Active { label: String::from("ab") };
+    let witness = G18State::Active {
+        label: String::from("ab"),
+    };
     kani::assume(g18_consistent(&witness));
     forget(witness);
     // Symbolic two-char string — same construction as current kani_depth2
@@ -188,10 +202,14 @@ fn gallery18d_symbolic_depth2_drop() {
 #[cfg(kani)]
 #[kani::proof_for_contract(g18_rename)]
 fn gallery18e_literal_depth2_nonempty() {
-    let witness = G18State::Active { label: String::from("abc") };
+    let witness = G18State::Active {
+        label: String::from("abc"),
+    };
     kani::assume(g18_consistent(&witness));
     forget(witness);
-    let state = G18State::Active { label: String::from("ab") };
+    let state = G18State::Active {
+        label: String::from("ab"),
+    };
     let new_label = String::from("c");
     let result = g18_rename(state, new_label);
     forget(result);
@@ -218,12 +236,16 @@ fn gallery18f_symbolic_depth1_one_char() {
     let c2: char = kani::any();
     let mut witness_label = c1.to_string();
     witness_label.push(c2);
-    let witness = G18State::Active { label: witness_label };
+    let witness = G18State::Active {
+        label: witness_label,
+    };
     kani::assume(g18_consistent(&witness));
     forget(witness);
     // Actual input: ONE symbolic char — the true inductive depth1 step
     let one_char: char = kani::any();
-    let state = G18State::Active { label: one_char.to_string() };
+    let state = G18State::Active {
+        label: one_char.to_string(),
+    };
     let new_label = String::from("b");
     let result = g18_rename(state, new_label);
     forget(result);

crates/elicit_proofs/src/kani/generated/archive_connection.rs

@@ -7,9 +7,9 @@
 
 #[cfg(kani)]
 use elicit_server::archive::vsm::{
-    archive_connection_consistent, begin_connect_kv, begin_connect_sql, connection_error,
-    disconnect, finish_connect_kv, finish_connect_sql, reconnect, ArchiveConnectionConsistent,
-    ArchiveConnectionState,
+    ArchiveConnectionConsistent, ArchiveConnectionState, archive_connection_consistent,
+    begin_connect_kv, begin_connect_sql, connection_error, disconnect, finish_connect_kv,
+    finish_connect_sql, reconnect,
 };
 #[cfg(kani)]
 use elicit_server::archive::{BackendKind, DatabaseDescriptor};

crates/elicit_proofs/src/kani/generated/archive_nav.rs

@@ -5,15 +5,15 @@
 // The `kani` cfg key is set by the Kani toolchain, not by cargo.
 #![allow(unexpected_cfgs)]
 
+#[cfg(kani)]
+use elicit_server::archive::NavTree;
 #[cfg(kani)]
 use elicit_server::archive::vsm::{
-    apply_filter, archive_nav_consistent, clear_filter, collapse_schema, expand_schema, load_nav,
-    move_cursor_down, move_cursor_up, nav_loaded, nav_refresh, ArchiveNavConsistent,
-    ArchiveNavState,
+    ArchiveNavConsistent, ArchiveNavState, apply_filter, archive_nav_consistent, clear_filter,
+    collapse_schema, expand_schema, load_nav, move_cursor_down, move_cursor_up, nav_loaded,
+    nav_refresh,
 };
 #[cfg(kani)]
-use elicit_server::archive::NavTree;
-#[cfg(kani)]
 use elicitation::Established;
 
 #[cfg(kani)]

crates/elicit_proofs/src/kani/generated/archive_overlay.rs

@@ -7,9 +7,9 @@
 
 #[cfg(kani)]
 use elicit_server::archive::vsm::{
-    archive_overlay_consistent, close_overlay, open_export_picker, open_help, open_save_prompt,
-    open_saved_browser, picker_move_down, picker_move_up, prompt_backspace, prompt_push,
-    saved_browser_down, saved_browser_up, ArchiveOverlayConsistent, ArchiveOverlayState,
+    ArchiveOverlayConsistent, ArchiveOverlayState, archive_overlay_consistent, close_overlay,
+    open_export_picker, open_help, open_save_prompt, open_saved_browser, picker_move_down,
+    picker_move_up, prompt_backspace, prompt_push, saved_browser_down, saved_browser_up,
 };
 #[cfg(kani)]
 use elicit_server::archive::{ExportFormat, SavedQuery};

crates/elicit_proofs/src/kani/generated/archive_panel.rs

@@ -13,11 +13,11 @@ use elicit_server::archive::display::{
 };
 #[cfg(kani)]
 use elicit_server::archive::vsm::{
-    abort_edits, admin_ready, archive_panel_consistent, begin_edit, column_detail, commit_edits,
-    constraints_ready, data_grid_ready, ddl_ready, erd_ready, explain_ready, export_ready,
-    history_ready, indexes_ready, monitor_ready, open_connection_editor, open_export_panel,
-    open_help_panel, open_saved_panel, open_sql_editor, panel_error, panel_loading, query_complete,
-    saved_ready, ArchivePanelConsistent, ArchivePanelState,
+    ArchivePanelConsistent, ArchivePanelState, abort_edits, admin_ready, archive_panel_consistent,
+    begin_edit, column_detail, commit_edits, constraints_ready, data_grid_ready, ddl_ready,
+    erd_ready, explain_ready, export_ready, history_ready, indexes_ready, monitor_ready,
+    open_connection_editor, open_export_panel, open_help_panel, open_saved_panel, open_sql_editor,
+    panel_error, panel_loading, query_complete, saved_ready,
 };
 #[cfg(kani)]
 use elicit_server::archive::{

verif/elicit_proofs_rlib/creusot/generated/archive_connection/begin_connect_kv_creusot.coma

@@ -13,7 +13,7 @@ let%span sarchive_connection'8 = "/home/erik/repos/elicitation/crates/elicit_pro
 let%span sarchive_connection'9 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 59 15 59 52
 let%span sarchive_connection'10 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 60 14 60 54
 let%span sarchive_connection'11 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 25 16 25 20
-let%span sconnection = "/home/erik/repos/elicitation/crates/elicit_server/src/archive/vsm/connection.rs" 154 0 161 1
+let%span sconnection = "/home/erik/repos/elicitation/crates/elicit_server/src/archive/vsm/connection.rs" 152 0 152 59
 
 use creusot.prelude.Any
 

verif/elicit_proofs_rlib/creusot/generated/archive_connection/begin_connect_sql_creusot.coma

@@ -13,7 +13,7 @@ let%span sarchive_connection'8 = "/home/erik/repos/elicitation/crates/elicit_pro
 let%span sarchive_connection'9 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 37 15 37 52
 let%span sarchive_connection'10 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 38 14 38 54
 let%span sarchive_connection'11 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 25 16 25 20
-let%span sconnection = "/home/erik/repos/elicitation/crates/elicit_server/src/archive/vsm/connection.rs" 133 0 141 1
+let%span sconnection = "/home/erik/repos/elicitation/crates/elicit_server/src/archive/vsm/connection.rs" 131 0 131 59
 
 use creusot.prelude.Any
 

verif/elicit_proofs_rlib/creusot/generated/archive_connection/connection_error_creusot.coma

@@ -13,7 +13,7 @@ let%span sarchive_connection'8 = "/home/erik/repos/elicitation/crates/elicit_pro
 let%span sarchive_connection'9 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 162 15 162 52
 let%span sarchive_connection'10 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 163 14 163 54
 let%span sarchive_connection'11 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 25 16 25 20
-let%span sconnection = "/home/erik/repos/elicitation/crates/elicit_server/src/archive/vsm/connection.rs" 233 0 240 1
+let%span sconnection = "/home/erik/repos/elicitation/crates/elicit_server/src/archive/vsm/connection.rs" 231 0 231 59
 
 use creusot.prelude.Any
 

verif/elicit_proofs_rlib/creusot/generated/archive_connection/disconnect_creusot.coma

@@ -11,7 +11,7 @@ let%span sarchive_connection'6 = "/home/erik/repos/elicitation/crates/elicit_pro
 let%span sarchive_connection'7 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 122 15 122 52
 let%span sarchive_connection'8 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 123 14 123 54
 let%span sarchive_connection'9 = "/home/erik/repos/elicitation/crates/elicit_proofs/src/creusot/generated/archive_connection.rs" 25 16 25 20
-let%span sconnection = "/home/erik/repos/elicitation/crates/elicit_server/src/archive/vsm/connection.rs" 202 0 208 1
+let%span sconnection = "/home/erik/repos/elicitation/crates/elicit_server/src/archive/vsm/connection.rs" 200 0 200 59
 
 use creusot.prelude.Any