diff options
author | Son Ho | 2024-06-04 13:52:44 +0200 |
---|---|---|
committer | Son Ho | 2024-06-04 13:52:44 +0200 |
commit | 3ad6c4712fd41efec55f29af5ccc31f68a0e12cf (patch) | |
tree | 89f3b6999e1697595f1c3fbb2d9c4d8c60a69e49 /tests/fstar/betree/Betree.Clauses.Template.fst | |
parent | 2a7a18d6a07ea4967ba9ec0763e6b7d04849dc7e (diff) | |
parent | 4a31acdff7a5dfdc26bf25ad25bb8266b790f891 (diff) |
Merge branch 'main' into son/loops2
Diffstat (limited to '')
-rw-r--r-- | tests/fstar/betree/Betree.Clauses.Template.fst (renamed from tests/fstar/betree/BetreeMain.Clauses.Template.fst) | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/tests/fstar/betree/BetreeMain.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst index b317dca4..fad8c5ba 100644 --- a/tests/fstar/betree/BetreeMain.Clauses.Template.fst +++ b/tests/fstar/betree/Betree.Clauses.Template.fst @@ -1,46 +1,46 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: templates for the decreases clauses *) -module BetreeMain.Clauses.Template +(** [betree]: templates for the decreases clauses *) +module Betree.Clauses.Template open Primitives -open BetreeMain.Types +open Betree.Types #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" -(** [betree_main::betree::{betree_main::betree::List<T>#1}::len]: decreases clause +(** [betree::betree::{betree::betree::List<T>#1}::len]: decreases clause Source: 'src/betree.rs', lines 276:4-276:24 *) unfold let betree_List_len_decreases (t : Type0) (self : betree_List_t t) : nat = admit () -(** [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: decreases clause +(** [betree::betree::{betree::betree::List<T>#1}::split_at]: decreases clause Source: 'src/betree.rs', lines 284:4-284:51 *) unfold let betree_List_split_at_decreases (t : Type0) (self : betree_List_t t) (n : u64) : nat = admit () -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: decreases clause Source: 'src/betree.rs', lines 339:4-339:73 *) unfold let betree_ListPairU64T_partition_at_pivot_decreases (t : Type0) (self : betree_List_t (u64 & t)) (pivot : u64) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: decreases clause Source: 'src/betree.rs', lines 789:4-792:34 *) unfold let betree_Node_lookup_first_message_for_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: decreases clause Source: 'src/betree.rs', lines 636:4-636:80 *) unfold let betree_Node_lookup_in_bindings_decreases (key : u64) (bindings : betree_List_t (u64 & u64)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: decreases clause Source: 'src/betree.rs', lines 819:4-819:90 *) unfold let betree_Node_apply_upserts_decreases @@ -48,35 +48,35 @@ let betree_Node_apply_upserts_decreases (key : u64) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: decreases clause +(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: decreases clause Source: 'src/betree.rs', lines 395:4-395:63 *) unfold let betree_Internal_lookup_in_children_decreases (self : betree_Internal_t) (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup]: decreases clause Source: 'src/betree.rs', lines 709:4-709:58 *) unfold let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64) (st : state) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: decreases clause Source: 'src/betree.rs', lines 674:4-674:77 *) unfold let betree_Node_filter_messages_for_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: decreases clause Source: 'src/betree.rs', lines 689:4-692:34 *) unfold let betree_Node_lookup_first_message_after_key_decreases (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: decreases clause Source: 'src/betree.rs', lines 502:4-505:5 *) unfold let betree_Node_apply_messages_to_internal_decreases @@ -84,14 +84,14 @@ let betree_Node_apply_messages_to_internal_decreases (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: decreases clause Source: 'src/betree.rs', lines 653:4-656:32 *) unfold let betree_Node_lookup_mut_in_bindings_decreases (key : u64) (bindings : betree_List_t (u64 & u64)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: decreases clause Source: 'src/betree.rs', lines 444:4-447:5 *) unfold let betree_Node_apply_messages_to_leaf_decreases @@ -99,7 +99,7 @@ let betree_Node_apply_messages_to_leaf_decreases (new_msgs : betree_List_t (u64 & betree_Message_t)) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: decreases clause +(** [betree::betree::{betree::betree::Internal#4}::flush]: decreases clause Source: 'src/betree.rs', lines 410:4-415:26 *) unfold let betree_Internal_flush_decreases (self : betree_Internal_t) @@ -107,7 +107,7 @@ let betree_Internal_flush_decreases (self : betree_Internal_t) (content : betree_List_t (u64 & betree_Message_t)) (st : state) : nat = admit () -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: decreases clause +(** [betree::betree::{betree::betree::Node#5}::apply_messages]: decreases clause Source: 'src/betree.rs', lines 588:4-593:5 *) unfold let betree_Node_apply_messages_decreases (self : betree_Node_t) |