Reorganize the Lean tests and extract the Polonius tests to Lean

1 files changed, 185 insertions, 0 deletions

diff --git a/tests/lean/betree/BetreeMain/Clauses/Template.lean b/tests/lean/betree/BetreeMain/Clauses/Template.lean
new file mode 100644
index 00000000..1d18174e
--- /dev/null
+++ b/tests/lean/betree/BetreeMain/Clauses/Template.lean
@@ -0,0 +1,185 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [betree_main]: templates for the decreases clauses
+import Base.Primitives
+import BetreeMain.Types
+
+/- [betree_main::betree::List::{1}::len]: termination measure -/
+@[simp]
+def betree_list_len_terminates (T : Type) (self : betree_list_t T) := self
+
+/- [betree_main::betree::List::{1}::len]: decreases_by tactic -/
+syntax "betree_list_len_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_list_len_decreases $self) =>`(tactic| sorry)
+
+/- [betree_main::betree::List::{1}::split_at]: termination measure -/
+@[simp]
+def betree_list_split_at_terminates (T : Type) (self : betree_list_t T)
+  (n : UInt64) :=
+  (self, n)
+
+/- [betree_main::betree::List::{1}::split_at]: decreases_by tactic -/
+syntax "betree_list_split_at_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_list_split_at_decreases $self $n) =>`(tactic| sorry)
+
+/- [betree_main::betree::List::{2}::partition_at_pivot]: termination measure -/
+@[simp]
+def betree_list_partition_at_pivot_terminates (T : Type)
+  (self : betree_list_t (UInt64 × T)) (pivot : UInt64) :=
+  (self, pivot)
+
+/- [betree_main::betree::List::{2}::partition_at_pivot]: decreases_by tactic -/
+syntax "betree_list_partition_at_pivot_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_list_partition_at_pivot_decreases $self $pivot) =>
+  `(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::lookup_in_bindings]: termination measure -/
+@[simp]
+def betree_node_lookup_in_bindings_terminates (key : UInt64)
+  (bindings : betree_list_t (UInt64 × UInt64)) :=
+  (key, bindings)
+
+/- [betree_main::betree::Node::{5}::lookup_in_bindings]: decreases_by tactic -/
+syntax "betree_node_lookup_in_bindings_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_lookup_in_bindings_decreases $key $bindings) =>
+  `(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: termination measure -/
+@[simp]
+def betree_node_lookup_first_message_for_key_terminates (key : UInt64)
+  (msgs : betree_list_t (UInt64 × betree_message_t)) :=
+  (key, msgs)
+
+/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: decreases_by tactic -/
+syntax "betree_node_lookup_first_message_for_key_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_lookup_first_message_for_key_decreases $key $msgs) =>
+  `(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::apply_upserts]: termination measure -/
+@[simp]
+def betree_node_apply_upserts_terminates
+  (msgs : betree_list_t (UInt64 × betree_message_t)) (prev : Option UInt64)
+  (key : UInt64) (st : State) :=
+  (msgs, prev, key, st)
+
+/- [betree_main::betree::Node::{5}::apply_upserts]: decreases_by tactic -/
+syntax "betree_node_apply_upserts_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_apply_upserts_decreases $msgs $prev $key $st) =>
+  `(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::lookup]: termination measure -/
+@[simp]
+def betree_node_lookup_terminates (self : betree_node_t) (key : UInt64)
+  (st : State) :=
+  (self, key, st)
+
+/- [betree_main::betree::Node::{5}::lookup]: decreases_by tactic -/
+syntax "betree_node_lookup_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_lookup_decreases $self $key $st) =>`(tactic| sorry)
+
+/- [betree_main::betree::Internal::{4}::lookup_in_children]: termination measure -/
+@[simp]
+def betree_internal_lookup_in_children_terminates (self : betree_internal_t)
+  (key : UInt64) (st : State) :=
+  (self, key, st)
+
+/- [betree_main::betree::Internal::{4}::lookup_in_children]: decreases_by tactic -/
+syntax "betree_internal_lookup_in_children_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_internal_lookup_in_children_decreases $self $key $st) =>
+  `(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: termination measure -/
+@[simp]
+def betree_node_lookup_mut_in_bindings_terminates (key : UInt64)
+  (bindings : betree_list_t (UInt64 × UInt64)) :=
+  (key, bindings)
+
+/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: decreases_by tactic -/
+syntax "betree_node_lookup_mut_in_bindings_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_lookup_mut_in_bindings_decreases $key $bindings) =>
+  `(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: termination measure -/
+@[simp]
+def betree_node_apply_messages_to_leaf_terminates
+  (bindings : betree_list_t (UInt64 × UInt64))
+  (new_msgs : betree_list_t (UInt64 × betree_message_t)) :=
+  (bindings, new_msgs)
+
+/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: decreases_by tactic -/
+syntax "betree_node_apply_messages_to_leaf_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_apply_messages_to_leaf_decreases $bindings
+$new_msgs) =>`(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::filter_messages_for_key]: termination measure -/
+@[simp]
+def betree_node_filter_messages_for_key_terminates (key : UInt64)
+  (msgs : betree_list_t (UInt64 × betree_message_t)) :=
+  (key, msgs)
+
+/- [betree_main::betree::Node::{5}::filter_messages_for_key]: decreases_by tactic -/
+syntax "betree_node_filter_messages_for_key_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_filter_messages_for_key_decreases $key $msgs) =>
+  `(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: termination measure -/
+@[simp]
+def betree_node_lookup_first_message_after_key_terminates (key : UInt64)
+  (msgs : betree_list_t (UInt64 × betree_message_t)) :=
+  (key, msgs)
+
+/- [betree_main::betree::Node::{5}::lookup_first_message_after_key]: decreases_by tactic -/
+syntax "betree_node_lookup_first_message_after_key_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_lookup_first_message_after_key_decreases $key $msgs) =>
+  `(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: termination measure -/
+@[simp]
+def betree_node_apply_messages_to_internal_terminates
+  (msgs : betree_list_t (UInt64 × betree_message_t))
+  (new_msgs : betree_list_t (UInt64 × betree_message_t)) :=
+  (msgs, new_msgs)
+
+/- [betree_main::betree::Node::{5}::apply_messages_to_internal]: decreases_by tactic -/
+syntax "betree_node_apply_messages_to_internal_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_apply_messages_to_internal_decreases $msgs
+$new_msgs) =>`(tactic| sorry)
+
+/- [betree_main::betree::Node::{5}::apply_messages]: termination measure -/
+@[simp]
+def betree_node_apply_messages_terminates (self : betree_node_t)
+  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
+  (msgs : betree_list_t (UInt64 × betree_message_t)) (st : State) :=
+  (self, params, node_id_cnt, msgs, st)
+
+/- [betree_main::betree::Node::{5}::apply_messages]: decreases_by tactic -/
+syntax "betree_node_apply_messages_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_node_apply_messages_decreases $self $params $node_id_cnt
+$msgs $st) =>`(tactic| sorry)
+
+/- [betree_main::betree::Internal::{4}::flush]: termination measure -/
+@[simp]
+def betree_internal_flush_terminates (self : betree_internal_t)
+  (params : betree_params_t) (node_id_cnt : betree_node_id_counter_t)
+  (content : betree_list_t (UInt64 × betree_message_t)) (st : State) :=
+  (self, params, node_id_cnt, content, st)
+
+/- [betree_main::betree::Internal::{4}::flush]: decreases_by tactic -/
+syntax "betree_internal_flush_decreases" term+ : tactic
+macro_rules
+| `(tactic| betree_internal_flush_decreases $self $params $node_id_cnt $content
+$st) =>`(tactic| sorry)
+