From 2b40c5c3de1ee2caca2c0072f812fea04b5a0238 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 14:59:10 +0200 Subject: tests: Merge the hashmap test files --- tests/coq/hashmap/Hashmap_Funs.v | 72 +- tests/coq/hashmap/Hashmap_FunsExternal.v | 21 + tests/coq/hashmap/Hashmap_FunsExternal_Template.v | 23 + tests/coq/hashmap/Hashmap_Types.v | 6 +- tests/coq/hashmap/Hashmap_TypesExternal.v | 13 + tests/coq/hashmap/Hashmap_TypesExternal_Template.v | 15 + tests/coq/hashmap_main/HashmapMain_Funs.v | 589 ------------- tests/coq/hashmap_main/HashmapMain_FunsExternal.v | 24 - .../HashmapMain_FunsExternal_Template.v | 26 - tests/coq/hashmap_main/HashmapMain_Types.v | 40 - tests/coq/hashmap_main/HashmapMain_TypesExternal.v | 14 - .../HashmapMain_TypesExternal_Template.v | 15 - tests/coq/hashmap_main/Makefile | 23 - tests/coq/hashmap_main/Primitives.v | 981 --------------------- tests/coq/hashmap_main/_CoqProject | 12 - 15 files changed, 118 insertions(+), 1756 deletions(-) create mode 100644 tests/coq/hashmap/Hashmap_FunsExternal.v create mode 100644 tests/coq/hashmap/Hashmap_FunsExternal_Template.v create mode 100644 tests/coq/hashmap/Hashmap_TypesExternal.v create mode 100644 tests/coq/hashmap/Hashmap_TypesExternal_Template.v delete mode 100644 tests/coq/hashmap_main/HashmapMain_Funs.v delete mode 100644 tests/coq/hashmap_main/HashmapMain_FunsExternal.v delete mode 100644 tests/coq/hashmap_main/HashmapMain_FunsExternal_Template.v delete mode 100644 tests/coq/hashmap_main/HashmapMain_Types.v delete mode 100644 tests/coq/hashmap_main/HashmapMain_TypesExternal.v delete mode 100644 tests/coq/hashmap_main/HashmapMain_TypesExternal_Template.v delete mode 100644 tests/coq/hashmap_main/Makefile delete mode 100644 tests/coq/hashmap_main/Primitives.v delete mode 100644 tests/coq/hashmap_main/_CoqProject (limited to 'tests/coq') diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 778b9d56..89f90210 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -8,15 +8,17 @@ Import ListNotations. Local Open Scope Primitives_scope. Require Import Hashmap_Types. Include Hashmap_Types. +Require Import Hashmap_FunsExternal. +Include Hashmap_FunsExternal. Module Hashmap_Funs. (** [hashmap::hash_key]: - Source: 'tests/src/hashmap.rs', lines 35:0-35:32 *) + Source: 'tests/src/hashmap.rs', lines 37:0-37:32 *) Definition hash_key (k : usize) : result usize := Ok k. (** [hashmap::{hashmap::HashMap}::allocate_slots]: loop 0: - Source: 'tests/src/hashmap.rs', lines 58:4-64:5 *) + Source: 'tests/src/hashmap.rs', lines 60:4-66:5 *) Fixpoint hashMap_allocate_slots_loop (T : Type) (n : nat) (slots : alloc_vec_Vec (List_t T)) (n1 : usize) : result (alloc_vec_Vec (List_t T)) @@ -34,7 +36,7 @@ Fixpoint hashMap_allocate_slots_loop . (** [hashmap::{hashmap::HashMap}::allocate_slots]: - Source: 'tests/src/hashmap.rs', lines 58:4-58:76 *) + Source: 'tests/src/hashmap.rs', lines 60:4-60:76 *) Definition hashMap_allocate_slots (T : Type) (n : nat) (slots : alloc_vec_Vec (List_t T)) (n1 : usize) : result (alloc_vec_Vec (List_t T)) @@ -43,7 +45,7 @@ Definition hashMap_allocate_slots . (** [hashmap::{hashmap::HashMap}::new_with_capacity]: - Source: 'tests/src/hashmap.rs', lines 67:4-71:13 *) + Source: 'tests/src/hashmap.rs', lines 69:4-73:13 *) Definition hashMap_new_with_capacity (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize) (max_load_divisor : usize) : @@ -62,13 +64,13 @@ Definition hashMap_new_with_capacity . (** [hashmap::{hashmap::HashMap}::new]: - Source: 'tests/src/hashmap.rs', lines 83:4-83:24 *) + Source: 'tests/src/hashmap.rs', lines 85:4-85:24 *) Definition hashMap_new (T : Type) (n : nat) : result (HashMap_t T) := hashMap_new_with_capacity T n 32%usize 4%usize 5%usize . (** [hashmap::{hashmap::HashMap}::clear]: loop 0: - Source: 'tests/src/hashmap.rs', lines 88:4-96:5 *) + Source: 'tests/src/hashmap.rs', lines 90:4-98:5 *) Fixpoint hashMap_clear_loop (T : Type) (n : nat) (slots : alloc_vec_Vec (List_t T)) (i : usize) : result (alloc_vec_Vec (List_t T)) @@ -91,7 +93,7 @@ Fixpoint hashMap_clear_loop . (** [hashmap::{hashmap::HashMap}::clear]: - Source: 'tests/src/hashmap.rs', lines 88:4-88:27 *) + Source: 'tests/src/hashmap.rs', lines 90:4-90:27 *) Definition hashMap_clear (T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) := hm <- hashMap_clear_loop T n self.(hashMap_slots) 0%usize; @@ -105,13 +107,13 @@ Definition hashMap_clear . (** [hashmap::{hashmap::HashMap}::len]: - Source: 'tests/src/hashmap.rs', lines 98:4-98:30 *) + Source: 'tests/src/hashmap.rs', lines 100:4-100:30 *) Definition hashMap_len (T : Type) (self : HashMap_t T) : result usize := Ok self.(hashMap_num_entries) . (** [hashmap::{hashmap::HashMap}::insert_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 105:4-122:5 *) + Source: 'tests/src/hashmap.rs', lines 107:4-124:5 *) Fixpoint hashMap_insert_in_list_loop (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) : result (bool * (List_t T)) @@ -133,7 +135,7 @@ Fixpoint hashMap_insert_in_list_loop . (** [hashmap::{hashmap::HashMap}::insert_in_list]: - Source: 'tests/src/hashmap.rs', lines 105:4-105:71 *) + Source: 'tests/src/hashmap.rs', lines 107:4-107:71 *) Definition hashMap_insert_in_list (T : Type) (n : nat) (key : usize) (value : T) (ls : List_t T) : result (bool * (List_t T)) @@ -142,7 +144,7 @@ Definition hashMap_insert_in_list . (** [hashmap::{hashmap::HashMap}::insert_no_resize]: - Source: 'tests/src/hashmap.rs', lines 125:4-125:54 *) + Source: 'tests/src/hashmap.rs', lines 127:4-127:54 *) Definition hashMap_insert_no_resize (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) : result (HashMap_t T) @@ -180,7 +182,7 @@ Definition hashMap_insert_no_resize . (** [hashmap::{hashmap::HashMap}::move_elements_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 191:4-204:5 *) + Source: 'tests/src/hashmap.rs', lines 193:4-206:5 *) Fixpoint hashMap_move_elements_from_list_loop (T : Type) (n : nat) (ntable : HashMap_t T) (ls : List_t T) : result (HashMap_t T) @@ -198,7 +200,7 @@ Fixpoint hashMap_move_elements_from_list_loop . (** [hashmap::{hashmap::HashMap}::move_elements_from_list]: - Source: 'tests/src/hashmap.rs', lines 191:4-191:72 *) + Source: 'tests/src/hashmap.rs', lines 193:4-193:72 *) Definition hashMap_move_elements_from_list (T : Type) (n : nat) (ntable : HashMap_t T) (ls : List_t T) : result (HashMap_t T) @@ -207,7 +209,7 @@ Definition hashMap_move_elements_from_list . (** [hashmap::{hashmap::HashMap}::move_elements]: loop 0: - Source: 'tests/src/hashmap.rs', lines 179:4-188:5 *) + Source: 'tests/src/hashmap.rs', lines 181:4-190:5 *) Fixpoint hashMap_move_elements_loop (T : Type) (n : nat) (ntable : HashMap_t T) (slots : alloc_vec_Vec (List_t T)) (i : usize) : @@ -233,7 +235,7 @@ Fixpoint hashMap_move_elements_loop . (** [hashmap::{hashmap::HashMap}::move_elements]: - Source: 'tests/src/hashmap.rs', lines 179:4-179:95 *) + Source: 'tests/src/hashmap.rs', lines 181:4-181:95 *) Definition hashMap_move_elements (T : Type) (n : nat) (ntable : HashMap_t T) (slots : alloc_vec_Vec (List_t T)) (i : usize) : @@ -243,7 +245,7 @@ Definition hashMap_move_elements . (** [hashmap::{hashmap::HashMap}::try_resize]: - Source: 'tests/src/hashmap.rs', lines 148:4-148:28 *) + Source: 'tests/src/hashmap.rs', lines 150:4-150:28 *) Definition hashMap_try_resize (T : Type) (n : nat) (self : HashMap_t T) : result (HashMap_t T) := max_usize <- scalar_cast U32 Usize core_u32_max; @@ -275,7 +277,7 @@ Definition hashMap_try_resize . (** [hashmap::{hashmap::HashMap}::insert]: - Source: 'tests/src/hashmap.rs', lines 137:4-137:48 *) + Source: 'tests/src/hashmap.rs', lines 139:4-139:48 *) Definition hashMap_insert (T : Type) (n : nat) (self : HashMap_t T) (key : usize) (value : T) : result (HashMap_t T) @@ -288,7 +290,7 @@ Definition hashMap_insert . (** [hashmap::{hashmap::HashMap}::contains_key_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 214:4-227:5 *) + Source: 'tests/src/hashmap.rs', lines 216:4-229:5 *) Fixpoint hashMap_contains_key_in_list_loop (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool := match n with @@ -305,14 +307,14 @@ Fixpoint hashMap_contains_key_in_list_loop . (** [hashmap::{hashmap::HashMap}::contains_key_in_list]: - Source: 'tests/src/hashmap.rs', lines 214:4-214:68 *) + Source: 'tests/src/hashmap.rs', lines 216:4-216:68 *) Definition hashMap_contains_key_in_list (T : Type) (n : nat) (key : usize) (ls : List_t T) : result bool := hashMap_contains_key_in_list_loop T n key ls . (** [hashmap::{hashmap::HashMap}::contains_key]: - Source: 'tests/src/hashmap.rs', lines 207:4-207:49 *) + Source: 'tests/src/hashmap.rs', lines 209:4-209:49 *) Definition hashMap_contains_key (T : Type) (n : nat) (self : HashMap_t T) (key : usize) : result bool := hash <- hash_key key; @@ -326,7 +328,7 @@ Definition hashMap_contains_key . (** [hashmap::{hashmap::HashMap}::get_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 232:4-245:5 *) + Source: 'tests/src/hashmap.rs', lines 234:4-247:5 *) Fixpoint hashMap_get_in_list_loop (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T := match n with @@ -341,14 +343,14 @@ Fixpoint hashMap_get_in_list_loop . (** [hashmap::{hashmap::HashMap}::get_in_list]: - Source: 'tests/src/hashmap.rs', lines 232:4-232:70 *) + Source: 'tests/src/hashmap.rs', lines 234:4-234:70 *) Definition hashMap_get_in_list (T : Type) (n : nat) (key : usize) (ls : List_t T) : result T := hashMap_get_in_list_loop T n key ls . (** [hashmap::{hashmap::HashMap}::get]: - Source: 'tests/src/hashmap.rs', lines 247:4-247:55 *) + Source: 'tests/src/hashmap.rs', lines 249:4-249:55 *) Definition hashMap_get (T : Type) (n : nat) (self : HashMap_t T) (key : usize) : result T := hash <- hash_key key; @@ -362,7 +364,7 @@ Definition hashMap_get . (** [hashmap::{hashmap::HashMap}::get_mut_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 253:4-262:5 *) + Source: 'tests/src/hashmap.rs', lines 255:4-264:5 *) Fixpoint hashMap_get_mut_in_list_loop (T : Type) (n : nat) (ls : List_t T) (key : usize) : result (T * (T -> result (List_t T))) @@ -388,7 +390,7 @@ Fixpoint hashMap_get_mut_in_list_loop . (** [hashmap::{hashmap::HashMap}::get_mut_in_list]: - Source: 'tests/src/hashmap.rs', lines 253:4-253:86 *) + Source: 'tests/src/hashmap.rs', lines 255:4-255:86 *) Definition hashMap_get_mut_in_list (T : Type) (n : nat) (ls : List_t T) (key : usize) : result (T * (T -> result (List_t T))) @@ -397,7 +399,7 @@ Definition hashMap_get_mut_in_list . (** [hashmap::{hashmap::HashMap}::get_mut]: - Source: 'tests/src/hashmap.rs', lines 265:4-265:67 *) + Source: 'tests/src/hashmap.rs', lines 267:4-267:67 *) Definition hashMap_get_mut (T : Type) (n : nat) (self : HashMap_t T) (key : usize) : result (T * (T -> result (HashMap_t T))) @@ -427,7 +429,7 @@ Definition hashMap_get_mut . (** [hashmap::{hashmap::HashMap}::remove_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 273:4-299:5 *) + Source: 'tests/src/hashmap.rs', lines 275:4-301:5 *) Fixpoint hashMap_remove_from_list_loop (T : Type) (n : nat) (key : usize) (ls : List_t T) : result ((option T) * (List_t T)) @@ -455,7 +457,7 @@ Fixpoint hashMap_remove_from_list_loop . (** [hashmap::{hashmap::HashMap}::remove_from_list]: - Source: 'tests/src/hashmap.rs', lines 273:4-273:69 *) + Source: 'tests/src/hashmap.rs', lines 275:4-275:69 *) Definition hashMap_remove_from_list (T : Type) (n : nat) (key : usize) (ls : List_t T) : result ((option T) * (List_t T)) @@ -464,7 +466,7 @@ Definition hashMap_remove_from_list . (** [hashmap::{hashmap::HashMap}::remove]: - Source: 'tests/src/hashmap.rs', lines 302:4-302:52 *) + Source: 'tests/src/hashmap.rs', lines 304:4-304:52 *) Definition hashMap_remove (T : Type) (n : nat) (self : HashMap_t T) (key : usize) : result ((option T) * (HashMap_t T)) @@ -502,8 +504,18 @@ Definition hashMap_remove end . +(** [hashmap::insert_on_disk]: + Source: 'tests/src/hashmap.rs', lines 335:0-335:43 *) +Definition insert_on_disk + (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) := + p <- hashmap_utils_deserialize st; + let (st1, hm) := p in + hm1 <- hashMap_insert u64 n hm key value; + hashmap_utils_serialize hm1 st1 +. + (** [hashmap::test1]: - Source: 'tests/src/hashmap.rs', lines 323:0-323:10 *) + Source: 'tests/src/hashmap.rs', lines 350:0-350:10 *) Definition test1 (n : nat) : result unit := hm <- hashMap_new u64 n; hm1 <- hashMap_insert u64 n hm 0%usize 42%u64; diff --git a/tests/coq/hashmap/Hashmap_FunsExternal.v b/tests/coq/hashmap/Hashmap_FunsExternal.v new file mode 100644 index 00000000..bcf12c17 --- /dev/null +++ b/tests/coq/hashmap/Hashmap_FunsExternal.v @@ -0,0 +1,21 @@ +(** [hashmap]: external functions. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Export Hashmap_Types. +Import Hashmap_Types. +Module Hashmap_FunsExternal. + +(** [hashmap::hashmap_utils::deserialize]: + Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *) +Axiom hashmap_utils_deserialize : state -> result (state * (HashMap_t u64)). + +(** [hashmap::hashmap_utils::serialize]: + Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *) +Axiom hashmap_utils_serialize : HashMap_t u64 -> state -> result (state * unit) +. + +End Hashmap_FunsExternal. diff --git a/tests/coq/hashmap/Hashmap_FunsExternal_Template.v b/tests/coq/hashmap/Hashmap_FunsExternal_Template.v new file mode 100644 index 00000000..c35b8e14 --- /dev/null +++ b/tests/coq/hashmap/Hashmap_FunsExternal_Template.v @@ -0,0 +1,23 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Import Hashmap_Types. +Include Hashmap_Types. +Module Hashmap_FunsExternal_Template. + +(** [hashmap::hashmap_utils::deserialize]: + Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *) +Axiom hashmap_utils_deserialize : state -> result (state * (HashMap_t u64)). + +(** [hashmap::hashmap_utils::serialize]: + Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *) +Axiom hashmap_utils_serialize : HashMap_t u64 -> state -> result (state * unit) +. + +End Hashmap_FunsExternal_Template. diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v index 8a8137d5..452d56f8 100644 --- a/tests/coq/hashmap/Hashmap_Types.v +++ b/tests/coq/hashmap/Hashmap_Types.v @@ -6,10 +6,12 @@ Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. +Require Import Hashmap_TypesExternal. +Include Hashmap_TypesExternal. Module Hashmap_Types. (** [hashmap::List] - Source: 'tests/src/hashmap.rs', lines 27:0-27:16 *) + Source: 'tests/src/hashmap.rs', lines 29:0-29:16 *) Inductive List_t (T : Type) := | List_Cons : usize -> T -> List_t T -> List_t T | List_Nil : List_t T @@ -19,7 +21,7 @@ Arguments List_Cons { _ }. Arguments List_Nil { _ }. (** [hashmap::HashMap] - Source: 'tests/src/hashmap.rs', lines 43:0-43:21 *) + Source: 'tests/src/hashmap.rs', lines 45:0-45:21 *) Record HashMap_t (T : Type) := mkHashMap_t { hashMap_num_entries : usize; diff --git a/tests/coq/hashmap/Hashmap_TypesExternal.v b/tests/coq/hashmap/Hashmap_TypesExternal.v new file mode 100644 index 00000000..0aa52a5d --- /dev/null +++ b/tests/coq/hashmap/Hashmap_TypesExternal.v @@ -0,0 +1,13 @@ +(** [hashmap]: external types. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module Hashmap_TypesExternal. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End Hashmap_TypesExternal. diff --git a/tests/coq/hashmap/Hashmap_TypesExternal_Template.v b/tests/coq/hashmap/Hashmap_TypesExternal_Template.v new file mode 100644 index 00000000..a8051adb --- /dev/null +++ b/tests/coq/hashmap/Hashmap_TypesExternal_Template.v @@ -0,0 +1,15 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module Hashmap_TypesExternal_Template. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End Hashmap_TypesExternal_Template. diff --git a/tests/coq/hashmap_main/HashmapMain_Funs.v b/tests/coq/hashmap_main/HashmapMain_Funs.v deleted file mode 100644 index f6467d5a..00000000 --- a/tests/coq/hashmap_main/HashmapMain_Funs.v +++ /dev/null @@ -1,589 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: function definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Require Import HashmapMain_Types. -Include HashmapMain_Types. -Require Import HashmapMain_FunsExternal. -Include HashmapMain_FunsExternal. -Module HashmapMain_Funs. - -(** [hashmap_main::hashmap::hash_key]: - Source: 'tests/src/hashmap.rs', lines 35:0-35:32 *) -Definition hashmap_hash_key (k : usize) : result usize := - Ok k. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: loop 0: - Source: 'tests/src/hashmap.rs', lines 58:4-64:5 *) -Fixpoint hashmap_HashMap_allocate_slots_loop - (T : Type) (n : nat) (slots : alloc_vec_Vec (hashmap_List_t T)) (n1 : usize) - : - result (alloc_vec_Vec (hashmap_List_t T)) - := - match n with - | O => Fail_ OutOfFuel - | S n2 => - if n1 s> 0%usize - then ( - slots1 <- alloc_vec_Vec_push (hashmap_List_t T) slots Hashmap_List_Nil; - n3 <- usize_sub n1 1%usize; - hashmap_HashMap_allocate_slots_loop T n2 slots1 n3) - else Ok slots - end -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::allocate_slots]: - Source: 'tests/src/hashmap.rs', lines 58:4-58:76 *) -Definition hashmap_HashMap_allocate_slots - (T : Type) (n : nat) (slots : alloc_vec_Vec (hashmap_List_t T)) (n1 : usize) - : - result (alloc_vec_Vec (hashmap_List_t T)) - := - hashmap_HashMap_allocate_slots_loop T n slots n1 -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new_with_capacity]: - Source: 'tests/src/hashmap.rs', lines 67:4-71:13 *) -Definition hashmap_HashMap_new_with_capacity - (T : Type) (n : nat) (capacity : usize) (max_load_dividend : usize) - (max_load_divisor : usize) : - result (hashmap_HashMap_t T) - := - slots <- - hashmap_HashMap_allocate_slots T n (alloc_vec_Vec_new (hashmap_List_t T)) - capacity; - i <- usize_mul capacity max_load_dividend; - i1 <- usize_div i max_load_divisor; - Ok - {| - hashmap_HashMap_num_entries := 0%usize; - hashmap_HashMap_max_load_factor := (max_load_dividend, max_load_divisor); - hashmap_HashMap_max_load := i1; - hashmap_HashMap_slots := slots - |} -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::new]: - Source: 'tests/src/hashmap.rs', lines 83:4-83:24 *) -Definition hashmap_HashMap_new - (T : Type) (n : nat) : result (hashmap_HashMap_t T) := - hashmap_HashMap_new_with_capacity T n 32%usize 4%usize 5%usize -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::clear]: loop 0: - Source: 'tests/src/hashmap.rs', lines 88:4-96:5 *) -Fixpoint hashmap_HashMap_clear_loop - (T : Type) (n : nat) (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : - result (alloc_vec_Vec (hashmap_List_t T)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - let i1 := alloc_vec_Vec_len (hashmap_List_t T) slots in - if i s< i1 - then ( - p <- - alloc_vec_Vec_index_mut (hashmap_List_t T) usize - (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) slots - i; - let (_, index_mut_back) := p in - i2 <- usize_add i 1%usize; - slots1 <- index_mut_back Hashmap_List_Nil; - hashmap_HashMap_clear_loop T n1 slots1 i2) - else Ok slots - end -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::clear]: - Source: 'tests/src/hashmap.rs', lines 88:4-88:27 *) -Definition hashmap_HashMap_clear - (T : Type) (n : nat) (self : hashmap_HashMap_t T) : - result (hashmap_HashMap_t T) - := - hm <- hashmap_HashMap_clear_loop T n self.(hashmap_HashMap_slots) 0%usize; - Ok - {| - hashmap_HashMap_num_entries := 0%usize; - hashmap_HashMap_max_load_factor := self.(hashmap_HashMap_max_load_factor); - hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := hm - |} -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::len]: - Source: 'tests/src/hashmap.rs', lines 98:4-98:30 *) -Definition hashmap_HashMap_len - (T : Type) (self : hashmap_HashMap_t T) : result usize := - Ok self.(hashmap_HashMap_num_entries) -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 105:4-122:5 *) -Fixpoint hashmap_HashMap_insert_in_list_loop - (T : Type) (n : nat) (key : usize) (value : T) (ls : hashmap_List_t T) : - result (bool * (hashmap_List_t T)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match ls with - | Hashmap_List_Cons ckey cvalue tl => - if ckey s= key - then Ok (false, Hashmap_List_Cons ckey value tl) - else ( - p <- hashmap_HashMap_insert_in_list_loop T n1 key value tl; - let (b, tl1) := p in - Ok (b, Hashmap_List_Cons ckey cvalue tl1)) - | Hashmap_List_Nil => - Ok (true, Hashmap_List_Cons key value Hashmap_List_Nil) - end - end -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_in_list]: - Source: 'tests/src/hashmap.rs', lines 105:4-105:71 *) -Definition hashmap_HashMap_insert_in_list - (T : Type) (n : nat) (key : usize) (value : T) (ls : hashmap_List_t T) : - result (bool * (hashmap_List_t T)) - := - hashmap_HashMap_insert_in_list_loop T n key value ls -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert_no_resize]: - Source: 'tests/src/hashmap.rs', lines 125:4-125:54 *) -Definition hashmap_HashMap_insert_no_resize - (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) : - result (hashmap_HashMap_t T) - := - hash <- hashmap_hash_key key; - let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in - hash_mod <- usize_rem hash i; - p <- - alloc_vec_Vec_index_mut (hashmap_List_t T) usize - (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) - self.(hashmap_HashMap_slots) hash_mod; - let (l, index_mut_back) := p in - p1 <- hashmap_HashMap_insert_in_list T n key value l; - let (inserted, l1) := p1 in - if inserted - then ( - i1 <- usize_add self.(hashmap_HashMap_num_entries) 1%usize; - v <- index_mut_back l1; - Ok - {| - hashmap_HashMap_num_entries := i1; - hashmap_HashMap_max_load_factor := - self.(hashmap_HashMap_max_load_factor); - hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := v - |}) - else ( - v <- index_mut_back l1; - Ok - {| - hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); - hashmap_HashMap_max_load_factor := - self.(hashmap_HashMap_max_load_factor); - hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := v - |}) -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 191:4-204:5 *) -Fixpoint hashmap_HashMap_move_elements_from_list_loop - (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) (ls : hashmap_List_t T) : - result (hashmap_HashMap_t T) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match ls with - | Hashmap_List_Cons k v tl => - ntable1 <- hashmap_HashMap_insert_no_resize T n1 ntable k v; - hashmap_HashMap_move_elements_from_list_loop T n1 ntable1 tl - | Hashmap_List_Nil => Ok ntable - end - end -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements_from_list]: - Source: 'tests/src/hashmap.rs', lines 191:4-191:72 *) -Definition hashmap_HashMap_move_elements_from_list - (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) (ls : hashmap_List_t T) : - result (hashmap_HashMap_t T) - := - hashmap_HashMap_move_elements_from_list_loop T n ntable ls -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: loop 0: - Source: 'tests/src/hashmap.rs', lines 179:4-188:5 *) -Fixpoint hashmap_HashMap_move_elements_loop - (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) - (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : - result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T))) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - let i1 := alloc_vec_Vec_len (hashmap_List_t T) slots in - if i s< i1 - then ( - p <- - alloc_vec_Vec_index_mut (hashmap_List_t T) usize - (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) slots - i; - let (l, index_mut_back) := p in - let (ls, l1) := core_mem_replace (hashmap_List_t T) l Hashmap_List_Nil in - ntable1 <- hashmap_HashMap_move_elements_from_list T n1 ntable ls; - i2 <- usize_add i 1%usize; - slots1 <- index_mut_back l1; - hashmap_HashMap_move_elements_loop T n1 ntable1 slots1 i2) - else Ok (ntable, slots) - end -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::move_elements]: - Source: 'tests/src/hashmap.rs', lines 179:4-179:95 *) -Definition hashmap_HashMap_move_elements - (T : Type) (n : nat) (ntable : hashmap_HashMap_t T) - (slots : alloc_vec_Vec (hashmap_List_t T)) (i : usize) : - result ((hashmap_HashMap_t T) * (alloc_vec_Vec (hashmap_List_t T))) - := - hashmap_HashMap_move_elements_loop T n ntable slots i -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::try_resize]: - Source: 'tests/src/hashmap.rs', lines 148:4-148:28 *) -Definition hashmap_HashMap_try_resize - (T : Type) (n : nat) (self : hashmap_HashMap_t T) : - result (hashmap_HashMap_t T) - := - max_usize <- scalar_cast U32 Usize core_u32_max; - let capacity := - alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in - n1 <- usize_div max_usize 2%usize; - let (i, i1) := self.(hashmap_HashMap_max_load_factor) in - i2 <- usize_div n1 i; - if capacity s<= i2 - then ( - i3 <- usize_mul capacity 2%usize; - ntable <- hashmap_HashMap_new_with_capacity T n i3 i i1; - p <- - hashmap_HashMap_move_elements T n ntable self.(hashmap_HashMap_slots) - 0%usize; - let (ntable1, _) := p in - Ok - {| - hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); - hashmap_HashMap_max_load_factor := (i, i1); - hashmap_HashMap_max_load := ntable1.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := ntable1.(hashmap_HashMap_slots) - |}) - else - Ok - {| - hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); - hashmap_HashMap_max_load_factor := (i, i1); - hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := self.(hashmap_HashMap_slots) - |} -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::insert]: - Source: 'tests/src/hashmap.rs', lines 137:4-137:48 *) -Definition hashmap_HashMap_insert - (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) (value : T) : - result (hashmap_HashMap_t T) - := - self1 <- hashmap_HashMap_insert_no_resize T n self key value; - i <- hashmap_HashMap_len T self1; - if i s> self1.(hashmap_HashMap_max_load) - then hashmap_HashMap_try_resize T n self1 - else Ok self1 -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 214:4-227:5 *) -Fixpoint hashmap_HashMap_contains_key_in_list_loop - (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result bool := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match ls with - | Hashmap_List_Cons ckey _ tl => - if ckey s= key - then Ok true - else hashmap_HashMap_contains_key_in_list_loop T n1 key tl - | Hashmap_List_Nil => Ok false - end - end -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key_in_list]: - Source: 'tests/src/hashmap.rs', lines 214:4-214:68 *) -Definition hashmap_HashMap_contains_key_in_list - (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result bool := - hashmap_HashMap_contains_key_in_list_loop T n key ls -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::contains_key]: - Source: 'tests/src/hashmap.rs', lines 207:4-207:49 *) -Definition hashmap_HashMap_contains_key - (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : - result bool - := - hash <- hashmap_hash_key key; - let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in - hash_mod <- usize_rem hash i; - l <- - alloc_vec_Vec_index (hashmap_List_t T) usize - (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) - self.(hashmap_HashMap_slots) hash_mod; - hashmap_HashMap_contains_key_in_list T n key l -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 232:4-245:5 *) -Fixpoint hashmap_HashMap_get_in_list_loop - (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result T := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match ls with - | Hashmap_List_Cons ckey cvalue tl => - if ckey s= key - then Ok cvalue - else hashmap_HashMap_get_in_list_loop T n1 key tl - | Hashmap_List_Nil => Fail_ Failure - end - end -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_in_list]: - Source: 'tests/src/hashmap.rs', lines 232:4-232:70 *) -Definition hashmap_HashMap_get_in_list - (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : result T := - hashmap_HashMap_get_in_list_loop T n key ls -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get]: - Source: 'tests/src/hashmap.rs', lines 247:4-247:55 *) -Definition hashmap_HashMap_get - (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : result T := - hash <- hashmap_hash_key key; - let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in - hash_mod <- usize_rem hash i; - l <- - alloc_vec_Vec_index (hashmap_List_t T) usize - (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) - self.(hashmap_HashMap_slots) hash_mod; - hashmap_HashMap_get_in_list T n key l -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 253:4-262:5 *) -Fixpoint hashmap_HashMap_get_mut_in_list_loop - (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) : - result (T * (T -> result (hashmap_List_t T))) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match ls with - | Hashmap_List_Cons ckey cvalue tl => - if ckey s= key - then - let back := fun (ret : T) => Ok (Hashmap_List_Cons ckey ret tl) in - Ok (cvalue, back) - else ( - p <- hashmap_HashMap_get_mut_in_list_loop T n1 tl key; - let (t, back) := p in - let back1 := - fun (ret : T) => - tl1 <- back ret; Ok (Hashmap_List_Cons ckey cvalue tl1) in - Ok (t, back1)) - | Hashmap_List_Nil => Fail_ Failure - end - end -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut_in_list]: - Source: 'tests/src/hashmap.rs', lines 253:4-253:86 *) -Definition hashmap_HashMap_get_mut_in_list - (T : Type) (n : nat) (ls : hashmap_List_t T) (key : usize) : - result (T * (T -> result (hashmap_List_t T))) - := - hashmap_HashMap_get_mut_in_list_loop T n ls key -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::get_mut]: - Source: 'tests/src/hashmap.rs', lines 265:4-265:67 *) -Definition hashmap_HashMap_get_mut - (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : - result (T * (T -> result (hashmap_HashMap_t T))) - := - hash <- hashmap_hash_key key; - let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in - hash_mod <- usize_rem hash i; - p <- - alloc_vec_Vec_index_mut (hashmap_List_t T) usize - (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) - self.(hashmap_HashMap_slots) hash_mod; - let (l, index_mut_back) := p in - p1 <- hashmap_HashMap_get_mut_in_list T n l key; - let (t, get_mut_in_list_back) := p1 in - let back := - fun (ret : T) => - l1 <- get_mut_in_list_back ret; - v <- index_mut_back l1; - Ok - {| - hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); - hashmap_HashMap_max_load_factor := - self.(hashmap_HashMap_max_load_factor); - hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := v - |} in - Ok (t, back) -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: loop 0: - Source: 'tests/src/hashmap.rs', lines 273:4-299:5 *) -Fixpoint hashmap_HashMap_remove_from_list_loop - (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : - result ((option T) * (hashmap_List_t T)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match ls with - | Hashmap_List_Cons ckey t tl => - if ckey s= key - then - let (mv_ls, _) := - core_mem_replace (hashmap_List_t T) (Hashmap_List_Cons ckey t tl) - Hashmap_List_Nil in - match mv_ls with - | Hashmap_List_Cons _ cvalue tl1 => Ok (Some cvalue, tl1) - | Hashmap_List_Nil => Fail_ Failure - end - else ( - p <- hashmap_HashMap_remove_from_list_loop T n1 key tl; - let (o, tl1) := p in - Ok (o, Hashmap_List_Cons ckey t tl1)) - | Hashmap_List_Nil => Ok (None, Hashmap_List_Nil) - end - end -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove_from_list]: - Source: 'tests/src/hashmap.rs', lines 273:4-273:69 *) -Definition hashmap_HashMap_remove_from_list - (T : Type) (n : nat) (key : usize) (ls : hashmap_List_t T) : - result ((option T) * (hashmap_List_t T)) - := - hashmap_HashMap_remove_from_list_loop T n key ls -. - -(** [hashmap_main::hashmap::{hashmap_main::hashmap::HashMap}::remove]: - Source: 'tests/src/hashmap.rs', lines 302:4-302:52 *) -Definition hashmap_HashMap_remove - (T : Type) (n : nat) (self : hashmap_HashMap_t T) (key : usize) : - result ((option T) * (hashmap_HashMap_t T)) - := - hash <- hashmap_hash_key key; - let i := alloc_vec_Vec_len (hashmap_List_t T) self.(hashmap_HashMap_slots) in - hash_mod <- usize_rem hash i; - p <- - alloc_vec_Vec_index_mut (hashmap_List_t T) usize - (core_slice_index_SliceIndexUsizeSliceTInst (hashmap_List_t T)) - self.(hashmap_HashMap_slots) hash_mod; - let (l, index_mut_back) := p in - p1 <- hashmap_HashMap_remove_from_list T n key l; - let (x, l1) := p1 in - match x with - | None => - v <- index_mut_back l1; - Ok (None, - {| - hashmap_HashMap_num_entries := self.(hashmap_HashMap_num_entries); - hashmap_HashMap_max_load_factor := - self.(hashmap_HashMap_max_load_factor); - hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := v - |}) - | Some x1 => - i1 <- usize_sub self.(hashmap_HashMap_num_entries) 1%usize; - v <- index_mut_back l1; - Ok (Some x1, - {| - hashmap_HashMap_num_entries := i1; - hashmap_HashMap_max_load_factor := - self.(hashmap_HashMap_max_load_factor); - hashmap_HashMap_max_load := self.(hashmap_HashMap_max_load); - hashmap_HashMap_slots := v - |}) - end -. - -(** [hashmap_main::hashmap::test1]: - Source: 'tests/src/hashmap.rs', lines 323:0-323:10 *) -Definition hashmap_test1 (n : nat) : result unit := - hm <- hashmap_HashMap_new u64 n; - hm1 <- hashmap_HashMap_insert u64 n hm 0%usize 42%u64; - hm2 <- hashmap_HashMap_insert u64 n hm1 128%usize 18%u64; - hm3 <- hashmap_HashMap_insert u64 n hm2 1024%usize 138%u64; - hm4 <- hashmap_HashMap_insert u64 n hm3 1056%usize 256%u64; - i <- hashmap_HashMap_get u64 n hm4 128%usize; - if negb (i s= 18%u64) - then Fail_ Failure - else ( - p <- hashmap_HashMap_get_mut u64 n hm4 1024%usize; - let (_, get_mut_back) := p in - hm5 <- get_mut_back 56%u64; - i1 <- hashmap_HashMap_get u64 n hm5 1024%usize; - if negb (i1 s= 56%u64) - then Fail_ Failure - else ( - p1 <- hashmap_HashMap_remove u64 n hm5 1024%usize; - let (x, hm6) := p1 in - match x with - | None => Fail_ Failure - | Some x1 => - if negb (x1 s= 56%u64) - then Fail_ Failure - else ( - i2 <- hashmap_HashMap_get u64 n hm6 0%usize; - if negb (i2 s= 42%u64) - then Fail_ Failure - else ( - i3 <- hashmap_HashMap_get u64 n hm6 128%usize; - if negb (i3 s= 18%u64) - then Fail_ Failure - else ( - i4 <- hashmap_HashMap_get u64 n hm6 1056%usize; - if negb (i4 s= 256%u64) then Fail_ Failure else Ok tt))) - end)) -. - -(** [hashmap_main::insert_on_disk]: - Source: 'tests/src/hashmap_main.rs', lines 13:0-13:43 *) -Definition insert_on_disk - (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) := - p <- hashmap_utils_deserialize st; - let (st1, hm) := p in - hm1 <- hashmap_HashMap_insert u64 n hm key value; - hashmap_utils_serialize hm1 st1 -. - -(** [hashmap_main::main]: - Source: 'tests/src/hashmap_main.rs', lines 22:0-22:13 *) -Definition main : result unit := - Ok tt. - -End HashmapMain_Funs. diff --git a/tests/coq/hashmap_main/HashmapMain_FunsExternal.v b/tests/coq/hashmap_main/HashmapMain_FunsExternal.v deleted file mode 100644 index fb5f23cd..00000000 --- a/tests/coq/hashmap_main/HashmapMain_FunsExternal.v +++ /dev/null @@ -1,24 +0,0 @@ -(** [hashmap_main]: external function declarations *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Require Export HashmapMain_Types. -Import HashmapMain_Types. -Module HashmapMain_FunsExternal. - -(** [hashmap_main::hashmap_utils::deserialize]: forward function - Source: 'src/hashmap_utils.rs', lines 10:0-10:43 *) -Axiom hashmap_utils_deserialize - : state -> result (state * (hashmap_HashMap_t u64)) -. - -(** [hashmap_main::hashmap_utils::serialize]: forward function - Source: 'src/hashmap_utils.rs', lines 5:0-5:42 *) -Axiom hashmap_utils_serialize - : hashmap_HashMap_t u64 -> state -> result (state * unit) -. - -End HashmapMain_FunsExternal. diff --git a/tests/coq/hashmap_main/HashmapMain_FunsExternal_Template.v b/tests/coq/hashmap_main/HashmapMain_FunsExternal_Template.v deleted file mode 100644 index 66835e8c..00000000 --- a/tests/coq/hashmap_main/HashmapMain_FunsExternal_Template.v +++ /dev/null @@ -1,26 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: external functions. --- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Require Import HashmapMain_Types. -Include HashmapMain_Types. -Module HashmapMain_FunsExternal_Template. - -(** [hashmap_main::hashmap_utils::deserialize]: - Source: 'tests/src/hashmap_utils.rs', lines 11:0-11:43 *) -Axiom hashmap_utils_deserialize - : state -> result (state * (hashmap_HashMap_t u64)) -. - -(** [hashmap_main::hashmap_utils::serialize]: - Source: 'tests/src/hashmap_utils.rs', lines 6:0-6:42 *) -Axiom hashmap_utils_serialize - : hashmap_HashMap_t u64 -> state -> result (state * unit) -. - -End HashmapMain_FunsExternal_Template. diff --git a/tests/coq/hashmap_main/HashmapMain_Types.v b/tests/coq/hashmap_main/HashmapMain_Types.v deleted file mode 100644 index 5656bd9c..00000000 --- a/tests/coq/hashmap_main/HashmapMain_Types.v +++ /dev/null @@ -1,40 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: type definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Require Import HashmapMain_TypesExternal. -Include HashmapMain_TypesExternal. -Module HashmapMain_Types. - -(** [hashmap_main::hashmap::List] - Source: 'tests/src/hashmap.rs', lines 27:0-27:16 *) -Inductive hashmap_List_t (T : Type) := -| Hashmap_List_Cons : usize -> T -> hashmap_List_t T -> hashmap_List_t T -| Hashmap_List_Nil : hashmap_List_t T -. - -Arguments Hashmap_List_Cons { _ }. -Arguments Hashmap_List_Nil { _ }. - -(** [hashmap_main::hashmap::HashMap] - Source: 'tests/src/hashmap.rs', lines 43:0-43:21 *) -Record hashmap_HashMap_t (T : Type) := -mkhashmap_HashMap_t { - hashmap_HashMap_num_entries : usize; - hashmap_HashMap_max_load_factor : (usize * usize); - hashmap_HashMap_max_load : usize; - hashmap_HashMap_slots : alloc_vec_Vec (hashmap_List_t T); -} -. - -Arguments mkhashmap_HashMap_t { _ }. -Arguments hashmap_HashMap_num_entries { _ }. -Arguments hashmap_HashMap_max_load_factor { _ }. -Arguments hashmap_HashMap_max_load { _ }. -Arguments hashmap_HashMap_slots { _ }. - -End HashmapMain_Types. diff --git a/tests/coq/hashmap_main/HashmapMain_TypesExternal.v b/tests/coq/hashmap_main/HashmapMain_TypesExternal.v deleted file mode 100644 index 28651c14..00000000 --- a/tests/coq/hashmap_main/HashmapMain_TypesExternal.v +++ /dev/null @@ -1,14 +0,0 @@ -(** [hashmap_main]: external types. --- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Module HashmapMain_TypesExternal. - -(** The state type used in the state-error monad *) -Axiom state : Type. - -End HashmapMain_TypesExternal. diff --git a/tests/coq/hashmap_main/HashmapMain_TypesExternal_Template.v b/tests/coq/hashmap_main/HashmapMain_TypesExternal_Template.v deleted file mode 100644 index 391b2775..00000000 --- a/tests/coq/hashmap_main/HashmapMain_TypesExternal_Template.v +++ /dev/null @@ -1,15 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: external types. --- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Module HashmapMain_TypesExternal_Template. - -(** The state type used in the state-error monad *) -Axiom state : Type. - -End HashmapMain_TypesExternal_Template. diff --git a/tests/coq/hashmap_main/Makefile b/tests/coq/hashmap_main/Makefile deleted file mode 100644 index 1a5aee4a..00000000 --- a/tests/coq/hashmap_main/Makefile +++ /dev/null @@ -1,23 +0,0 @@ -# This file was automatically generated - modify ../Makefile.template instead -# Makefile originally taken from coq-club - -%: Makefile.coq phony - +make -f Makefile.coq $@ - -all: Makefile.coq - +make -f Makefile.coq all - -clean: Makefile.coq - +make -f Makefile.coq clean - rm -f Makefile.coq - -Makefile.coq: _CoqProject Makefile - coq_makefile -f _CoqProject | sed 's/$$(COQCHK) $$(COQCHKFLAGS) $$(COQLIBS)/$$(COQCHK) $$(COQCHKFLAGS) $$(subst -Q,-R,$$(COQLIBS))/' > Makefile.coq - -_CoqProject: ; - -Makefile: ; - -phony: ; - -.PHONY: all clean phony diff --git a/tests/coq/hashmap_main/Primitives.v b/tests/coq/hashmap_main/Primitives.v deleted file mode 100644 index b29fce43..00000000 --- a/tests/coq/hashmap_main/Primitives.v +++ /dev/null @@ -1,981 +0,0 @@ -Require Import Lia. -Require Coq.Strings.Ascii. -Require Coq.Strings.String. -Require Import Coq.Program.Equality. -Require Import Coq.ZArith.ZArith. -Require Import Coq.ZArith.Znat. -Require Import List. -Import ListNotations. - -Module Primitives. - - (* TODO: use more *) -Declare Scope Primitives_scope. - -(*** Result *) - -Inductive error := - | Failure - | OutOfFuel. - -Inductive result A := - | Ok : A -> result A - | Fail_ : error -> result A. - -Arguments Ok {_} a. -Arguments Fail_ {_}. - -Definition bind {A B} (m: result A) (f: A -> result B) : result B := - match m with - | Fail_ e => Fail_ e - | Ok x => f x - end. - -Definition return_ {A: Type} (x: A) : result A := Ok x. -Definition fail_ {A: Type} (e: error) : result A := Fail_ e. - -Notation "x <- c1 ; c2" := (bind c1 (fun x => c2)) - (at level 61, c1 at next level, right associativity). - -(** Monadic assert *) -Definition massert (b: bool) : result unit := - if b then Ok tt else Fail_ Failure. - -(** Normalize and unwrap a successful result (used for globals) *) -Definition eval_result_refl {A} {x} (a: result A) (p: a = Ok x) : A := - match a as r return (r = Ok x -> A) with - | Ok a' => fun _ => a' - | Fail_ e => fun p' => - False_rect _ (eq_ind (Fail_ e) - (fun e : result A => - match e with - | Ok _ => False - | Fail_ e => True - end) - I (Ok x) p') - end p. - -Notation "x %global" := (eval_result_refl x eq_refl) (at level 40). -Notation "x %return" := (eval_result_refl x eq_refl) (at level 40). - -(* Sanity check *) -Check (if true then Ok (1 + 2) else Fail_ Failure)%global = 3. - -(*** Misc *) - -Definition string := Coq.Strings.String.string. -Definition char := Coq.Strings.Ascii.ascii. -Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte. - -Definition core_mem_replace (a : Type) (x : a) (y : a) : a * a := (x, x) . - -Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }. -Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }. - -(*** Scalars *) - -Definition i8_min : Z := -128%Z. -Definition i8_max : Z := 127%Z. -Definition i16_min : Z := -32768%Z. -Definition i16_max : Z := 32767%Z. -Definition i32_min : Z := -2147483648%Z. -Definition i32_max : Z := 2147483647%Z. -Definition i64_min : Z := -9223372036854775808%Z. -Definition i64_max : Z := 9223372036854775807%Z. -Definition i128_min : Z := -170141183460469231731687303715884105728%Z. -Definition i128_max : Z := 170141183460469231731687303715884105727%Z. -Definition u8_min : Z := 0%Z. -Definition u8_max : Z := 255%Z. -Definition u16_min : Z := 0%Z. -Definition u16_max : Z := 65535%Z. -Definition u32_min : Z := 0%Z. -Definition u32_max : Z := 4294967295%Z. -Definition u64_min : Z := 0%Z. -Definition u64_max : Z := 18446744073709551615%Z. -Definition u128_min : Z := 0%Z. -Definition u128_max : Z := 340282366920938463463374607431768211455%Z. - -(** The bounds of [isize] and [usize] vary with the architecture. *) -Axiom isize_min : Z. -Axiom isize_max : Z. -Definition usize_min : Z := 0%Z. -Axiom usize_max : Z. - -Open Scope Z_scope. - -(** We provide those lemmas to reason about the bounds of [isize] and [usize] *) -Axiom isize_min_bound : isize_min <= i32_min. -Axiom isize_max_bound : i32_max <= isize_max. -Axiom usize_max_bound : u32_max <= usize_max. - -Inductive scalar_ty := - | Isize - | I8 - | I16 - | I32 - | I64 - | I128 - | Usize - | U8 - | U16 - | U32 - | U64 - | U128 -. - -Definition scalar_min (ty: scalar_ty) : Z := - match ty with - | Isize => isize_min - | I8 => i8_min - | I16 => i16_min - | I32 => i32_min - | I64 => i64_min - | I128 => i128_min - | Usize => usize_min - | U8 => u8_min - | U16 => u16_min - | U32 => u32_min - | U64 => u64_min - | U128 => u128_min -end. - -Definition scalar_max (ty: scalar_ty) : Z := - match ty with - | Isize => isize_max - | I8 => i8_max - | I16 => i16_max - | I32 => i32_max - | I64 => i64_max - | I128 => i128_max - | Usize => usize_max - | U8 => u8_max - | U16 => u16_max - | U32 => u32_max - | U64 => u64_max - | U128 => u128_max -end. - -(** We use the following conservative bounds to make sure we can compute bound - checks in most situations *) -Definition scalar_min_cons (ty: scalar_ty) : Z := - match ty with - | Isize => i32_min - | Usize => u32_min - | _ => scalar_min ty -end. - -Definition scalar_max_cons (ty: scalar_ty) : Z := - match ty with - | Isize => i32_max - | Usize => u32_max - | _ => scalar_max ty -end. - -Lemma scalar_min_cons_valid : forall ty, scalar_min ty <= scalar_min_cons ty . -Proof. - destruct ty; unfold scalar_min_cons, scalar_min; try lia. - - pose isize_min_bound; lia. - - apply Z.le_refl. -Qed. - -Lemma scalar_max_cons_valid : forall ty, scalar_max ty >= scalar_max_cons ty . -Proof. - destruct ty; unfold scalar_max_cons, scalar_max; try lia. - - pose isize_max_bound; lia. - - pose usize_max_bound. lia. -Qed. - -Definition scalar (ty: scalar_ty) : Type := - { x: Z | scalar_min ty <= x <= scalar_max ty }. - -Definition to_Z {ty} (x: scalar ty) : Z := proj1_sig x. - -(** Bounds checks: we start by using the conservative bounds, to make sure we - can compute in most situations, then we use the real bounds (for [isize] - and [usize]). *) -Definition scalar_ge_min (ty: scalar_ty) (x: Z) : bool := - Z.leb (scalar_min_cons ty) x || Z.leb (scalar_min ty) x. - -Definition scalar_le_max (ty: scalar_ty) (x: Z) : bool := - Z.leb x (scalar_max_cons ty) || Z.leb x (scalar_max ty). - -Lemma scalar_ge_min_valid (ty: scalar_ty) (x: Z) : - scalar_ge_min ty x = true -> scalar_min ty <= x . -Proof. - unfold scalar_ge_min. - pose (scalar_min_cons_valid ty). - lia. -Qed. - -Lemma scalar_le_max_valid (ty: scalar_ty) (x: Z) : - scalar_le_max ty x = true -> x <= scalar_max ty . -Proof. - unfold scalar_le_max. - pose (scalar_max_cons_valid ty). - lia. -Qed. - -Definition scalar_in_bounds (ty: scalar_ty) (x: Z) : bool := - scalar_ge_min ty x && scalar_le_max ty x . - -Lemma scalar_in_bounds_valid (ty: scalar_ty) (x: Z) : - scalar_in_bounds ty x = true -> scalar_min ty <= x <= scalar_max ty . -Proof. - unfold scalar_in_bounds. - intros H. - destruct (scalar_ge_min ty x) eqn:Hmin. - - destruct (scalar_le_max ty x) eqn:Hmax. - + pose (scalar_ge_min_valid ty x Hmin). - pose (scalar_le_max_valid ty x Hmax). - lia. - + inversion H. - - inversion H. -Qed. - -Import Sumbool. - -Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) := - match sumbool_of_bool (scalar_in_bounds ty x) with - | left H => Ok (exist _ x (scalar_in_bounds_valid _ _ H)) - | right _ => Fail_ Failure - end. - -Definition scalar_add {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x + to_Z y). - -Definition scalar_sub {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x - to_Z y). - -Definition scalar_mul {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x * to_Z y). - -Definition scalar_div {ty} (x y: scalar ty) : result (scalar ty) := - if to_Z y =? 0 then Fail_ Failure else - mk_scalar ty (to_Z x / to_Z y). - -Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (Z.rem (to_Z x) (to_Z y)). - -Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)). - -Axiom scalar_xor : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *) -Axiom scalar_or : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *) -Axiom scalar_and : forall ty, scalar ty -> scalar ty -> scalar ty. (* TODO *) -Axiom scalar_shl : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *) -Axiom scalar_shr : forall ty0 ty1, scalar ty0 -> scalar ty1 -> result (scalar ty0). (* TODO *) - -(** Cast an integer from a [src_ty] to a [tgt_ty] *) -(* TODO: check the semantics of casts in Rust *) -Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) := - mk_scalar tgt_ty (to_Z x). - -(* This can't fail, but for now we make all casts faillible (easier for the translation) *) -Definition scalar_cast_bool (tgt_ty : scalar_ty) (x : bool) : result (scalar tgt_ty) := - mk_scalar tgt_ty (if x then 1 else 0). - -(** Comparisons *) -Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.leb (to_Z x) (to_Z y) . - -Definition scalar_ltb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.ltb (to_Z x) (to_Z y) . - -Definition scalar_geb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.geb (to_Z x) (to_Z y) . - -Definition scalar_gtb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.gtb (to_Z x) (to_Z y) . - -Definition scalar_eqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - Z.eqb (to_Z x) (to_Z y) . - -Definition scalar_neqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := - negb (Z.eqb (to_Z x) (to_Z y)) . - - -(** The scalar types *) -Definition isize := scalar Isize. -Definition i8 := scalar I8. -Definition i16 := scalar I16. -Definition i32 := scalar I32. -Definition i64 := scalar I64. -Definition i128 := scalar I128. -Definition usize := scalar Usize. -Definition u8 := scalar U8. -Definition u16 := scalar U16. -Definition u32 := scalar U32. -Definition u64 := scalar U64. -Definition u128 := scalar U128. - -(** Negaion *) -Definition isize_neg := @scalar_neg Isize. -Definition i8_neg := @scalar_neg I8. -Definition i16_neg := @scalar_neg I16. -Definition i32_neg := @scalar_neg I32. -Definition i64_neg := @scalar_neg I64. -Definition i128_neg := @scalar_neg I128. - -(** Division *) -Definition isize_div := @scalar_div Isize. -Definition i8_div := @scalar_div I8. -Definition i16_div := @scalar_div I16. -Definition i32_div := @scalar_div I32. -Definition i64_div := @scalar_div I64. -Definition i128_div := @scalar_div I128. -Definition usize_div := @scalar_div Usize. -Definition u8_div := @scalar_div U8. -Definition u16_div := @scalar_div U16. -Definition u32_div := @scalar_div U32. -Definition u64_div := @scalar_div U64. -Definition u128_div := @scalar_div U128. - -(** Remainder *) -Definition isize_rem := @scalar_rem Isize. -Definition i8_rem := @scalar_rem I8. -Definition i16_rem := @scalar_rem I16. -Definition i32_rem := @scalar_rem I32. -Definition i64_rem := @scalar_rem I64. -Definition i128_rem := @scalar_rem I128. -Definition usize_rem := @scalar_rem Usize. -Definition u8_rem := @scalar_rem U8. -Definition u16_rem := @scalar_rem U16. -Definition u32_rem := @scalar_rem U32. -Definition u64_rem := @scalar_rem U64. -Definition u128_rem := @scalar_rem U128. - -(** Addition *) -Definition isize_add := @scalar_add Isize. -Definition i8_add := @scalar_add I8. -Definition i16_add := @scalar_add I16. -Definition i32_add := @scalar_add I32. -Definition i64_add := @scalar_add I64. -Definition i128_add := @scalar_add I128. -Definition usize_add := @scalar_add Usize. -Definition u8_add := @scalar_add U8. -Definition u16_add := @scalar_add U16. -Definition u32_add := @scalar_add U32. -Definition u64_add := @scalar_add U64. -Definition u128_add := @scalar_add U128. - -(** Substraction *) -Definition isize_sub := @scalar_sub Isize. -Definition i8_sub := @scalar_sub I8. -Definition i16_sub := @scalar_sub I16. -Definition i32_sub := @scalar_sub I32. -Definition i64_sub := @scalar_sub I64. -Definition i128_sub := @scalar_sub I128. -Definition usize_sub := @scalar_sub Usize. -Definition u8_sub := @scalar_sub U8. -Definition u16_sub := @scalar_sub U16. -Definition u32_sub := @scalar_sub U32. -Definition u64_sub := @scalar_sub U64. -Definition u128_sub := @scalar_sub U128. - -(** Multiplication *) -Definition isize_mul := @scalar_mul Isize. -Definition i8_mul := @scalar_mul I8. -Definition i16_mul := @scalar_mul I16. -Definition i32_mul := @scalar_mul I32. -Definition i64_mul := @scalar_mul I64. -Definition i128_mul := @scalar_mul I128. -Definition usize_mul := @scalar_mul Usize. -Definition u8_mul := @scalar_mul U8. -Definition u16_mul := @scalar_mul U16. -Definition u32_mul := @scalar_mul U32. -Definition u64_mul := @scalar_mul U64. -Definition u128_mul := @scalar_mul U128. - -(** Xor *) -Definition u8_xor := @scalar_xor U8. -Definition u16_xor := @scalar_xor U16. -Definition u32_xor := @scalar_xor U32. -Definition u64_xor := @scalar_xor U64. -Definition u128_xor := @scalar_xor U128. -Definition usize_xor := @scalar_xor Usize. -Definition i8_xor := @scalar_xor I8. -Definition i16_xor := @scalar_xor I16. -Definition i32_xor := @scalar_xor I32. -Definition i64_xor := @scalar_xor I64. -Definition i128_xor := @scalar_xor I128. -Definition isize_xor := @scalar_xor Isize. - -(** Or *) -Definition u8_or := @scalar_or U8. -Definition u16_or := @scalar_or U16. -Definition u32_or := @scalar_or U32. -Definition u64_or := @scalar_or U64. -Definition u128_or := @scalar_or U128. -Definition usize_or := @scalar_or Usize. -Definition i8_or := @scalar_or I8. -Definition i16_or := @scalar_or I16. -Definition i32_or := @scalar_or I32. -Definition i64_or := @scalar_or I64. -Definition i128_or := @scalar_or I128. -Definition isize_or := @scalar_or Isize. - -(** And *) -Definition u8_and := @scalar_and U8. -Definition u16_and := @scalar_and U16. -Definition u32_and := @scalar_and U32. -Definition u64_and := @scalar_and U64. -Definition u128_and := @scalar_and U128. -Definition usize_and := @scalar_and Usize. -Definition i8_and := @scalar_and I8. -Definition i16_and := @scalar_and I16. -Definition i32_and := @scalar_and I32. -Definition i64_and := @scalar_and I64. -Definition i128_and := @scalar_and I128. -Definition isize_and := @scalar_and Isize. - -(** Shift left *) -Definition u8_shl {ty} := @scalar_shl U8 ty. -Definition u16_shl {ty} := @scalar_shl U16 ty. -Definition u32_shl {ty} := @scalar_shl U32 ty. -Definition u64_shl {ty} := @scalar_shl U64 ty. -Definition u128_shl {ty} := @scalar_shl U128 ty. -Definition usize_shl {ty} := @scalar_shl Usize ty. -Definition i8_shl {ty} := @scalar_shl I8 ty. -Definition i16_shl {ty} := @scalar_shl I16 ty. -Definition i32_shl {ty} := @scalar_shl I32 ty. -Definition i64_shl {ty} := @scalar_shl I64 ty. -Definition i128_shl {ty} := @scalar_shl I128 ty. -Definition isize_shl {ty} := @scalar_shl Isize ty. - -(** Shift right *) -Definition u8_shr {ty} := @scalar_shr U8 ty. -Definition u16_shr {ty} := @scalar_shr U16 ty. -Definition u32_shr {ty} := @scalar_shr U32 ty. -Definition u64_shr {ty} := @scalar_shr U64 ty. -Definition u128_shr {ty} := @scalar_shr U128 ty. -Definition usize_shr {ty} := @scalar_shr Usize ty. -Definition i8_shr {ty} := @scalar_shr I8 ty. -Definition i16_shr {ty} := @scalar_shr I16 ty. -Definition i32_shr {ty} := @scalar_shr I32 ty. -Definition i64_shr {ty} := @scalar_shr I64 ty. -Definition i128_shr {ty} := @scalar_shr I128 ty. -Definition isize_shr {ty} := @scalar_shr Isize ty. - -(** Small utility *) -Definition usize_to_nat (x: usize) : nat := Z.to_nat (to_Z x). - -(** Notations *) -Notation "x %isize" := ((mk_scalar Isize x)%return) (at level 9). -Notation "x %i8" := ((mk_scalar I8 x)%return) (at level 9). -Notation "x %i16" := ((mk_scalar I16 x)%return) (at level 9). -Notation "x %i32" := ((mk_scalar I32 x)%return) (at level 9). -Notation "x %i64" := ((mk_scalar I64 x)%return) (at level 9). -Notation "x %i128" := ((mk_scalar I128 x)%return) (at level 9). -Notation "x %usize" := ((mk_scalar Usize x)%return) (at level 9). -Notation "x %u8" := ((mk_scalar U8 x)%return) (at level 9). -Notation "x %u16" := ((mk_scalar U16 x)%return) (at level 9). -Notation "x %u32" := ((mk_scalar U32 x)%return) (at level 9). -Notation "x %u64" := ((mk_scalar U64 x)%return) (at level 9). -Notation "x %u128" := ((mk_scalar U128 x)%return) (at level 9). - -Notation "x s= y" := (scalar_eqb x y) (at level 80) : Primitives_scope. -Notation "x s<> y" := (scalar_neqb x y) (at level 80) : Primitives_scope. -Notation "x s<= y" := (scalar_leb x y) (at level 80) : Primitives_scope. -Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope. -Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope. -Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope. - -(** Constants *) -Definition core_u8_max := u8_max %u32. -Definition core_u16_max := u16_max %u32. -Definition core_u32_max := u32_max %u32. -Definition core_u64_max := u64_max %u64. -Definition core_u128_max := u64_max %u128. -Axiom core_usize_max : usize. (** TODO *) -Definition core_i8_max := i8_max %i32. -Definition core_i16_max := i16_max %i32. -Definition core_i32_max := i32_max %i32. -Definition core_i64_max := i64_max %i64. -Definition core_i128_max := i64_max %i128. -Axiom core_isize_max : isize. (** TODO *) - -(*** core *) - -(** Trait declaration: [core::clone::Clone] *) -Record core_clone_Clone (self : Type) := { - clone : self -> result self -}. - -Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b. - -Definition core_clone_CloneBool : core_clone_Clone bool := {| - clone := fun b => Ok (core_clone_impls_CloneBool_clone b) -|}. - -Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x. -Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x. -Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x. -Definition core_clone_impls_CloneU32_clone (x : u32) : u32 := x. -Definition core_clone_impls_CloneU64_clone (x : u64) : u64 := x. -Definition core_clone_impls_CloneU128_clone (x : u128) : u128 := x. - -Definition core_clone_impls_CloneIsize_clone (x : isize) : isize := x. -Definition core_clone_impls_CloneI8_clone (x : i8) : i8 := x. -Definition core_clone_impls_CloneI16_clone (x : i16) : i16 := x. -Definition core_clone_impls_CloneI32_clone (x : i32) : i32 := x. -Definition core_clone_impls_CloneI64_clone (x : i64) : i64 := x. -Definition core_clone_impls_CloneI128_clone (x : i128) : i128 := x. - -Definition core_clone_CloneUsize : core_clone_Clone usize := {| - clone := fun x => Ok (core_clone_impls_CloneUsize_clone x) -|}. - -Definition core_clone_CloneU8 : core_clone_Clone u8 := {| - clone := fun x => Ok (core_clone_impls_CloneU8_clone x) -|}. - -Definition core_clone_CloneU16 : core_clone_Clone u16 := {| - clone := fun x => Ok (core_clone_impls_CloneU16_clone x) -|}. - -Definition core_clone_CloneU32 : core_clone_Clone u32 := {| - clone := fun x => Ok (core_clone_impls_CloneU32_clone x) -|}. - -Definition core_clone_CloneU64 : core_clone_Clone u64 := {| - clone := fun x => Ok (core_clone_impls_CloneU64_clone x) -|}. - -Definition core_clone_CloneU128 : core_clone_Clone u128 := {| - clone := fun x => Ok (core_clone_impls_CloneU128_clone x) -|}. - -Definition core_clone_CloneIsize : core_clone_Clone isize := {| - clone := fun x => Ok (core_clone_impls_CloneIsize_clone x) -|}. - -Definition core_clone_CloneI8 : core_clone_Clone i8 := {| - clone := fun x => Ok (core_clone_impls_CloneI8_clone x) -|}. - -Definition core_clone_CloneI16 : core_clone_Clone i16 := {| - clone := fun x => Ok (core_clone_impls_CloneI16_clone x) -|}. - -Definition core_clone_CloneI32 : core_clone_Clone i32 := {| - clone := fun x => Ok (core_clone_impls_CloneI32_clone x) -|}. - -Definition core_clone_CloneI64 : core_clone_Clone i64 := {| - clone := fun x => Ok (core_clone_impls_CloneI64_clone x) -|}. - -Definition core_clone_CloneI128 : core_clone_Clone i128 := {| - clone := fun x => Ok (core_clone_impls_CloneI128_clone x) -|}. - -(** [core::option::{core::option::Option}::unwrap] *) -Definition core_option_Option_unwrap (T : Type) (x : option T) : result T := - match x with - | None => Fail_ Failure - | Some x => Ok x - end. - -(*** core::ops *) - -(* Trait declaration: [core::ops::index::Index] *) -Record core_ops_index_Index (Self Idx : Type) := mk_core_ops_index_Index { - core_ops_index_Index_Output : Type; - core_ops_index_Index_index : Self -> Idx -> result core_ops_index_Index_Output; -}. -Arguments mk_core_ops_index_Index {_ _}. -Arguments core_ops_index_Index_Output {_ _}. -Arguments core_ops_index_Index_index {_ _}. - -(* Trait declaration: [core::ops::index::IndexMut] *) -Record core_ops_index_IndexMut (Self Idx : Type) := mk_core_ops_index_IndexMut { - core_ops_index_IndexMut_indexInst : core_ops_index_Index Self Idx; - core_ops_index_IndexMut_index_mut : - Self -> - Idx -> - result (core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output) * - (core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output) -> result Self)); -}. -Arguments mk_core_ops_index_IndexMut {_ _}. -Arguments core_ops_index_IndexMut_indexInst {_ _}. -Arguments core_ops_index_IndexMut_index_mut {_ _}. - -(* Trait declaration [core::ops::deref::Deref] *) -Record core_ops_deref_Deref (Self : Type) := mk_core_ops_deref_Deref { - core_ops_deref_Deref_target : Type; - core_ops_deref_Deref_deref : Self -> result core_ops_deref_Deref_target; -}. -Arguments mk_core_ops_deref_Deref {_}. -Arguments core_ops_deref_Deref_target {_}. -Arguments core_ops_deref_Deref_deref {_}. - -(* Trait declaration [core::ops::deref::DerefMut] *) -Record core_ops_deref_DerefMut (Self : Type) := mk_core_ops_deref_DerefMut { - core_ops_deref_DerefMut_derefInst : core_ops_deref_Deref Self; - core_ops_deref_DerefMut_deref_mut : - Self -> - result (core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target) * - (core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target) -> result Self)); -}. -Arguments mk_core_ops_deref_DerefMut {_}. -Arguments core_ops_deref_DerefMut_derefInst {_}. -Arguments core_ops_deref_DerefMut_deref_mut {_}. - -Record core_ops_range_Range (T : Type) := mk_core_ops_range_Range { - core_ops_range_Range_start : T; - core_ops_range_Range_end_ : T; -}. -Arguments mk_core_ops_range_Range {_}. -Arguments core_ops_range_Range_start {_}. -Arguments core_ops_range_Range_end_ {_}. - -(*** [alloc] *) - -Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Ok x. -Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result (T * (T -> result T)) := - Ok (x, fun x => Ok x). - -(* Trait instance *) -Definition alloc_boxed_Box_coreopsDerefInst (Self : Type) : core_ops_deref_Deref Self := {| - core_ops_deref_Deref_target := Self; - core_ops_deref_Deref_deref := alloc_boxed_Box_deref Self; -|}. - -(* Trait instance *) -Definition alloc_boxed_Box_coreopsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {| - core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreopsDerefInst Self; - core_ops_deref_DerefMut_deref_mut := alloc_boxed_Box_deref_mut Self; -|}. - - -(*** Arrays *) -Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}. - -Lemma le_0_usize_max : 0 <= usize_max. -Proof. - pose (H := usize_max_bound). - unfold u32_max in H. - lia. -Qed. - -Lemma eqb_imp_eq (x y : Z) : Z.eqb x y = true -> x = y. -Proof. - lia. -Qed. - -(* TODO: finish the definitions *) -Axiom mk_array : forall (T : Type) (n : usize) (l : list T), array T n. - -(* For initialization *) -Axiom array_repeat : forall (T : Type) (n : usize) (x : T), array T n. - -Axiom array_index_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. -Axiom array_update_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n). - -Definition array_index_mut_usize (T : Type) (n : usize) (a : array T n) (i : usize) : - result (T * (T -> result (array T n))) := - match array_index_usize T n a i with - | Fail_ e => Fail_ e - | Ok x => Ok (x, array_update_usize T n a i) - end. - -(*** Slice *) -Definition slice T := { l: list T | Z.of_nat (length l) <= usize_max}. - -Axiom slice_len : forall (T : Type) (s : slice T), usize. -Axiom slice_index_usize : forall (T : Type) (x : slice T) (i : usize), result T. -Axiom slice_update_usize : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T). - -Definition slice_index_mut_usize (T : Type) (s : slice T) (i : usize) : - result (T * (T -> result (slice T))) := - match slice_index_usize T s i with - | Fail_ e => Fail_ e - | Ok x => Ok (x, slice_update_usize T s i) - end. - -(*** Subslices *) - -Axiom array_to_slice : forall (T : Type) (n : usize) (x : array T n), result (slice T). -Axiom array_from_slice : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n). - -Definition array_to_slice_mut (T : Type) (n : usize) (a : array T n) : - result (slice T * (slice T -> result (array T n))) := - match array_to_slice T n a with - | Fail_ e => Fail_ e - | Ok x => Ok (x, array_from_slice T n a) - end. - -Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T). -Axiom array_update_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize) (ns : slice T), result (array T n). - -Axiom slice_subslice: forall (T : Type) (x : slice T) (r : core_ops_range_Range usize), result (slice T). -Axiom slice_update_subslice: forall (T : Type) (x : slice T) (r : core_ops_range_Range usize) (ns : slice T), result (slice T). - -(*** Vectors *) - -Definition alloc_vec_Vec T := { l: list T | Z.of_nat (length l) <= usize_max }. - -Definition alloc_vec_Vec_to_list {T: Type} (v: alloc_vec_Vec T) : list T := proj1_sig v. - -Definition alloc_vec_Vec_length {T: Type} (v: alloc_vec_Vec T) : Z := Z.of_nat (length (alloc_vec_Vec_to_list v)). - -Definition alloc_vec_Vec_new (T: Type) : alloc_vec_Vec T := (exist _ [] le_0_usize_max). - -Lemma alloc_vec_Vec_len_in_usize {T} (v: alloc_vec_Vec T) : usize_min <= alloc_vec_Vec_length v <= usize_max. -Proof. - unfold alloc_vec_Vec_length, usize_min. - split. - - lia. - - apply (proj2_sig v). -Qed. - -Definition alloc_vec_Vec_len (T: Type) (v: alloc_vec_Vec T) : usize := - exist _ (alloc_vec_Vec_length v) (alloc_vec_Vec_len_in_usize v). - -Fixpoint list_update {A} (l: list A) (n: nat) (a: A) - : list A := - match l with - | [] => [] - | x :: t => match n with - | 0%nat => a :: t - | S m => x :: (list_update t m a) -end end. - -Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) := - l <- f (alloc_vec_Vec_to_list v) ; - match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with - | left H => Ok (exist _ l (scalar_le_max_valid _ _ H)) - | right _ => Fail_ Failure - end. - -Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) := - alloc_vec_Vec_bind v (fun l => Ok (l ++ [x])). - -Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) := - alloc_vec_Vec_bind v (fun l => - if to_Z i result (alloc_vec_Vec T))) := - match alloc_vec_Vec_index_usize v i with - | Ok x => - Ok (x, alloc_vec_Vec_update_usize v i) - | Fail_ e => Fail_ e - end. - -(* Trait declaration: [core::slice::index::private_slice_index::Sealed] *) -Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit. - -(* Trait declaration: [core::slice::index::SliceIndex] *) -Record core_slice_index_SliceIndex (Self T : Type) := mk_core_slice_index_SliceIndex { - core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self; - core_slice_index_SliceIndex_Output : Type; - core_slice_index_SliceIndex_get : Self -> T -> result (option core_slice_index_SliceIndex_Output); - core_slice_index_SliceIndex_get_mut : - Self -> T -> result (option core_slice_index_SliceIndex_Output * (option core_slice_index_SliceIndex_Output -> result T)); - core_slice_index_SliceIndex_get_unchecked : Self -> const_raw_ptr T -> result (const_raw_ptr core_slice_index_SliceIndex_Output); - core_slice_index_SliceIndex_get_unchecked_mut : Self -> mut_raw_ptr T -> result (mut_raw_ptr core_slice_index_SliceIndex_Output); - core_slice_index_SliceIndex_index : Self -> T -> result core_slice_index_SliceIndex_Output; - core_slice_index_SliceIndex_index_mut : - Self -> T -> result (core_slice_index_SliceIndex_Output * (core_slice_index_SliceIndex_Output -> result T)); -}. -Arguments mk_core_slice_index_SliceIndex {_ _}. -Arguments core_slice_index_SliceIndex_sealedInst {_ _}. -Arguments core_slice_index_SliceIndex_Output {_ _}. -Arguments core_slice_index_SliceIndex_get {_ _}. -Arguments core_slice_index_SliceIndex_get_mut {_ _}. -Arguments core_slice_index_SliceIndex_get_unchecked {_ _}. -Arguments core_slice_index_SliceIndex_get_unchecked_mut {_ _}. -Arguments core_slice_index_SliceIndex_index {_ _}. -Arguments core_slice_index_SliceIndex_index_mut {_ _}. - -(* [core::slice::index::[T]::index]: forward function *) -Definition core_slice_index_Slice_index - (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) - (s : slice T) (i : Idx) : result inst.(core_slice_index_SliceIndex_Output) := - x <- inst.(core_slice_index_SliceIndex_get) i s; - match x with - | None => Fail_ Failure - | Some x => Ok x - end. - -(* [core::slice::index::Range:::get]: forward function *) -Axiom core_slice_index_RangeUsize_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)). - -(* [core::slice::index::Range::get_mut]: forward function *) -Axiom core_slice_index_RangeUsize_get_mut : - forall (T : Type), - core_ops_range_Range usize -> slice T -> - result (option (slice T) * (option (slice T) -> result (slice T))). - -(* [core::slice::index::Range::get_unchecked]: forward function *) -Definition core_slice_index_RangeUsize_get_unchecked - (T : Type) : - core_ops_range_Range usize -> const_raw_ptr (slice T) -> result (const_raw_ptr (slice T)) := - (* Don't know what the model should be - for now we always fail to make - sure code which uses it fails *) - fun _ _ => Fail_ Failure. - -(* [core::slice::index::Range::get_unchecked_mut]: forward function *) -Definition core_slice_index_RangeUsize_get_unchecked_mut - (T : Type) : - core_ops_range_Range usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr (slice T)) := - (* Don't know what the model should be - for now we always fail to make - sure code which uses it fails *) - fun _ _ => Fail_ Failure. - -(* [core::slice::index::Range::index]: forward function *) -Axiom core_slice_index_RangeUsize_index : - forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T). - -(* [core::slice::index::Range::index_mut]: forward function *) -Axiom core_slice_index_RangeUsize_index_mut : - forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T * (slice T -> result (slice T))). - -(* [core::slice::index::[T]::index_mut]: forward function *) -Axiom core_slice_index_Slice_index_mut : - forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)), - slice T -> Idx -> - result (inst.(core_slice_index_SliceIndex_Output) * - (inst.(core_slice_index_SliceIndex_Output) -> result (slice T))). - -(* [core::array::[T; N]::index]: forward function *) -Axiom core_array_Array_index : - forall (T Idx : Type) (N : usize) (inst : core_ops_index_Index (slice T) Idx) - (a : array T N) (i : Idx), result inst.(core_ops_index_Index_Output). - -(* [core::array::[T; N]::index_mut]: forward function *) -Axiom core_array_Array_index_mut : - forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx) - (a : array T N) (i : Idx), - result (inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output) * - (inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output) -> result (array T N))). - -(* Trait implementation: [core::slice::index::private_slice_index::Range] *) -Definition core_slice_index_private_slice_index_SealedRangeUsizeInst - : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt. - -(* Trait implementation: [core::slice::index::Range] *) -Definition core_slice_index_SliceIndexRangeUsizeSliceTInst (T : Type) : - core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) := {| - core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedRangeUsizeInst; - core_slice_index_SliceIndex_Output := slice T; - core_slice_index_SliceIndex_get := core_slice_index_RangeUsize_get T; - core_slice_index_SliceIndex_get_mut := core_slice_index_RangeUsize_get_mut T; - core_slice_index_SliceIndex_get_unchecked := core_slice_index_RangeUsize_get_unchecked T; - core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_RangeUsize_get_unchecked_mut T; - core_slice_index_SliceIndex_index := core_slice_index_RangeUsize_index T; - core_slice_index_SliceIndex_index_mut := core_slice_index_RangeUsize_index_mut T; -|}. - -(* Trait implementation: [core::slice::index::[T]] *) -Definition core_ops_index_IndexSliceTIInst (T Idx : Type) - (inst : core_slice_index_SliceIndex Idx (slice T)) : - core_ops_index_Index (slice T) Idx := {| - core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output); - core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst; -|}. - -(* Trait implementation: [core::slice::index::[T]] *) -Definition core_ops_index_IndexMutSliceTIInst (T Idx : Type) - (inst : core_slice_index_SliceIndex Idx (slice T)) : - core_ops_index_IndexMut (slice T) Idx := {| - core_ops_index_IndexMut_indexInst := core_ops_index_IndexSliceTIInst T Idx inst; - core_ops_index_IndexMut_index_mut := core_slice_index_Slice_index_mut T Idx inst; -|}. - -(* Trait implementation: [core::array::[T; N]] *) -Definition core_ops_index_IndexArrayInst (T Idx : Type) (N : usize) - (inst : core_ops_index_Index (slice T) Idx) : - core_ops_index_Index (array T N) Idx := {| - core_ops_index_Index_Output := inst.(core_ops_index_Index_Output); - core_ops_index_Index_index := core_array_Array_index T Idx N inst; -|}. - -(* Trait implementation: [core::array::[T; N]] *) -Definition core_ops_index_IndexMutArrayInst (T Idx : Type) (N : usize) - (inst : core_ops_index_IndexMut (slice T) Idx) : - core_ops_index_IndexMut (array T N) Idx := {| - core_ops_index_IndexMut_indexInst := core_ops_index_IndexArrayInst T Idx N inst.(core_ops_index_IndexMut_indexInst); - core_ops_index_IndexMut_index_mut := core_array_Array_index_mut T Idx N inst; -|}. - -(* [core::slice::index::usize::get]: forward function *) -Axiom core_slice_index_usize_get : forall (T : Type), usize -> slice T -> result (option T). - -(* [core::slice::index::usize::get_mut]: forward function *) -Axiom core_slice_index_usize_get_mut : - forall (T : Type), usize -> slice T -> result (option T * (option T -> result (slice T))). - -(* [core::slice::index::usize::get_unchecked]: forward function *) -Axiom core_slice_index_usize_get_unchecked : - forall (T : Type), usize -> const_raw_ptr (slice T) -> result (const_raw_ptr T). - -(* [core::slice::index::usize::get_unchecked_mut]: forward function *) -Axiom core_slice_index_usize_get_unchecked_mut : - forall (T : Type), usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr T). - -(* [core::slice::index::usize::index]: forward function *) -Axiom core_slice_index_usize_index : forall (T : Type), usize -> slice T -> result T. - -(* [core::slice::index::usize::index_mut]: forward function *) -Axiom core_slice_index_usize_index_mut : - forall (T : Type), usize -> slice T -> result (T * (T -> result (slice T))). - -(* Trait implementation: [core::slice::index::private_slice_index::usize] *) -Definition core_slice_index_private_slice_index_SealedUsizeInst - : core_slice_index_private_slice_index_Sealed usize := tt. - -(* Trait implementation: [core::slice::index::usize] *) -Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) : - core_slice_index_SliceIndex usize (slice T) := {| - core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst; - core_slice_index_SliceIndex_Output := T; - core_slice_index_SliceIndex_get := core_slice_index_usize_get T; - core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut T; - core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked T; - core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_usize_get_unchecked_mut T; - core_slice_index_SliceIndex_index := core_slice_index_usize_index T; - core_slice_index_SliceIndex_index_mut := core_slice_index_usize_index_mut T; -|}. - -(* [alloc::vec::Vec::index]: forward function *) -Axiom alloc_vec_Vec_index : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) - (Self : alloc_vec_Vec T) (i : Idx), result inst.(core_slice_index_SliceIndex_Output). - -(* [alloc::vec::Vec::index_mut]: forward function *) -Axiom alloc_vec_Vec_index_mut : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) - (Self : alloc_vec_Vec T) (i : Idx), - result (inst.(core_slice_index_SliceIndex_Output) * - (inst.(core_slice_index_SliceIndex_Output) -> result (alloc_vec_Vec T))). - -(* Trait implementation: [alloc::vec::Vec] *) -Definition alloc_vec_Vec_coreopsindexIndexInst (T Idx : Type) - (inst : core_slice_index_SliceIndex Idx (slice T)) : - core_ops_index_Index (alloc_vec_Vec T) Idx := {| - core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output); - core_ops_index_Index_index := alloc_vec_Vec_index T Idx inst; -|}. - -(* Trait implementation: [alloc::vec::Vec] *) -Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type) - (inst : core_slice_index_SliceIndex Idx (slice T)) : - core_ops_index_IndexMut (alloc_vec_Vec T) Idx := {| - core_ops_index_IndexMut_indexInst := alloc_vec_Vec_coreopsindexIndexInst T Idx inst; - core_ops_index_IndexMut_index_mut := alloc_vec_Vec_index_mut T Idx inst; -|}. - -(*** Theorems *) - -Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a), - alloc_vec_Vec_index a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i = - alloc_vec_Vec_index_usize v i. - -Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a), - alloc_vec_Vec_index_mut a usize (core_slice_index_SliceIndexUsizeSliceTInst a) v i = - alloc_vec_Vec_index_mut_usize v i. - -End Primitives. diff --git a/tests/coq/hashmap_main/_CoqProject b/tests/coq/hashmap_main/_CoqProject deleted file mode 100644 index d73541d9..00000000 --- a/tests/coq/hashmap_main/_CoqProject +++ /dev/null @@ -1,12 +0,0 @@ -# This file was automatically generated - see ../Makefile --R . Lib --arg -w --arg all - -HashmapMain_Types.v -HashmapMain_FunsExternal_Template.v -Primitives.v -HashmapMain_Funs.v -HashmapMain_TypesExternal.v -HashmapMain_FunsExternal.v -HashmapMain_TypesExternal_Template.v -- cgit v1.2.3 From f77e3f9cbe2ea7abeb4be815bdbf33d0c98076c2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 13:28:28 +0200 Subject: tests: Rename betree_main -> betree --- tests/coq/betree/BetreeMain_Funs.v | 837 --------------------- tests/coq/betree/BetreeMain_FunsExternal.v | 39 - .../coq/betree/BetreeMain_FunsExternal_Template.v | 40 - tests/coq/betree/BetreeMain_Types.v | 118 --- tests/coq/betree/BetreeMain_TypesExternal.v | 14 - .../coq/betree/BetreeMain_TypesExternal_Template.v | 15 - tests/coq/betree/Betree_Funs.v | 837 +++++++++++++++++++++ tests/coq/betree/Betree_FunsExternal.v | 39 + tests/coq/betree/Betree_FunsExternal_Template.v | 40 + tests/coq/betree/Betree_Types.v | 118 +++ tests/coq/betree/Betree_TypesExternal.v | 14 + tests/coq/betree/Betree_TypesExternal_Template.v | 15 + tests/coq/betree/_CoqProject | 12 +- 13 files changed, 1069 insertions(+), 1069 deletions(-) delete mode 100644 tests/coq/betree/BetreeMain_Funs.v delete mode 100644 tests/coq/betree/BetreeMain_FunsExternal.v delete mode 100644 tests/coq/betree/BetreeMain_FunsExternal_Template.v delete mode 100644 tests/coq/betree/BetreeMain_Types.v delete mode 100644 tests/coq/betree/BetreeMain_TypesExternal.v delete mode 100644 tests/coq/betree/BetreeMain_TypesExternal_Template.v create mode 100644 tests/coq/betree/Betree_Funs.v create mode 100644 tests/coq/betree/Betree_FunsExternal.v create mode 100644 tests/coq/betree/Betree_FunsExternal_Template.v create mode 100644 tests/coq/betree/Betree_Types.v create mode 100644 tests/coq/betree/Betree_TypesExternal.v create mode 100644 tests/coq/betree/Betree_TypesExternal_Template.v (limited to 'tests/coq') diff --git a/tests/coq/betree/BetreeMain_Funs.v b/tests/coq/betree/BetreeMain_Funs.v deleted file mode 100644 index e0a1d8a2..00000000 --- a/tests/coq/betree/BetreeMain_Funs.v +++ /dev/null @@ -1,837 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: function definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Require Import BetreeMain_Types. -Include BetreeMain_Types. -Require Import BetreeMain_FunsExternal. -Include BetreeMain_FunsExternal. -Module BetreeMain_Funs. - -(** [betree_main::betree::load_internal_node]: - Source: 'src/betree.rs', lines 36:0-36:52 *) -Definition betree_load_internal_node - (id : u64) (st : state) : - result (state * (betree_List_t (u64 * betree_Message_t))) - := - betree_utils_load_internal_node id st -. - -(** [betree_main::betree::store_internal_node]: - Source: 'src/betree.rs', lines 41:0-41:60 *) -Definition betree_store_internal_node - (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) : - result (state * unit) - := - betree_utils_store_internal_node id content st -. - -(** [betree_main::betree::load_leaf_node]: - Source: 'src/betree.rs', lines 46:0-46:44 *) -Definition betree_load_leaf_node - (id : u64) (st : state) : result (state * (betree_List_t (u64 * u64))) := - betree_utils_load_leaf_node id st -. - -(** [betree_main::betree::store_leaf_node]: - Source: 'src/betree.rs', lines 51:0-51:52 *) -Definition betree_store_leaf_node - (id : u64) (content : betree_List_t (u64 * u64)) (st : state) : - result (state * unit) - := - betree_utils_store_leaf_node id content st -. - -(** [betree_main::betree::fresh_node_id]: - Source: 'src/betree.rs', lines 55:0-55:48 *) -Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) := - counter1 <- u64_add counter 1%u64; Ok (counter, counter1) -. - -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: - Source: 'src/betree.rs', lines 206:4-206:20 *) -Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t := - Ok {| betree_NodeIdCounter_next_node_id := 0%u64 |} -. - -(** [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: - Source: 'src/betree.rs', lines 210:4-210:36 *) -Definition betree_NodeIdCounter_fresh_id - (self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) := - i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64; - Ok (self.(betree_NodeIdCounter_next_node_id), - {| betree_NodeIdCounter_next_node_id := i |}) -. - -(** [betree_main::betree::upsert_update]: - Source: 'src/betree.rs', lines 234:0-234:70 *) -Definition betree_upsert_update - (prev : option u64) (st : betree_UpsertFunState_t) : result u64 := - match prev with - | None => - match st with - | Betree_UpsertFunState_Add v => Ok v - | Betree_UpsertFunState_Sub _ => Ok 0%u64 - end - | Some prev1 => - match st with - | Betree_UpsertFunState_Add v => - margin <- u64_sub core_u64_max prev1; - if margin s>= v then u64_add prev1 v else Ok core_u64_max - | Betree_UpsertFunState_Sub v => - if prev1 s>= v then u64_sub prev1 v else Ok 0%u64 - end - end -. - -(** [betree_main::betree::{betree_main::betree::List#1}::len]: - Source: 'src/betree.rs', lines 276:4-276:24 *) -Fixpoint betree_List_len - (T : Type) (n : nat) (self : betree_List_t T) : result u64 := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match self with - | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i - | Betree_List_Nil => Ok 0%u64 - end - end -. - -(** [betree_main::betree::{betree_main::betree::List#1}::split_at]: - Source: 'src/betree.rs', lines 284:4-284:51 *) -Fixpoint betree_List_split_at - (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) : - result ((betree_List_t T) * (betree_List_t T)) - := - match n with - | O => Fail_ OutOfFuel - | S n2 => - if n1 s= 0%u64 - then Ok (Betree_List_Nil, self) - else - match self with - | Betree_List_Cons hd tl => - i <- u64_sub n1 1%u64; - p <- betree_List_split_at T n2 tl i; - let (ls0, ls1) := p in - Ok (Betree_List_Cons hd ls0, ls1) - | Betree_List_Nil => Fail_ Failure - end - end -. - -(** [betree_main::betree::{betree_main::betree::List#1}::push_front]: - Source: 'src/betree.rs', lines 299:4-299:34 *) -Definition betree_List_push_front - (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) := - let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in - Ok (Betree_List_Cons x tl) -. - -(** [betree_main::betree::{betree_main::betree::List#1}::pop_front]: - Source: 'src/betree.rs', lines 306:4-306:32 *) -Definition betree_List_pop_front - (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) := - let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in - match ls with - | Betree_List_Cons x tl => Ok (x, tl) - | Betree_List_Nil => Fail_ Failure - end -. - -(** [betree_main::betree::{betree_main::betree::List#1}::hd]: - Source: 'src/betree.rs', lines 318:4-318:22 *) -Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := - match self with - | Betree_List_Cons hd _ => Ok hd - | Betree_List_Nil => Fail_ Failure - end -. - -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: - Source: 'src/betree.rs', lines 327:4-327:44 *) -Definition betree_ListPairU64T_head_has_key - (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool := - match self with - | Betree_List_Cons hd _ => let (i, _) := hd in Ok (i s= key) - | Betree_List_Nil => Ok false - end -. - -(** [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: - Source: 'src/betree.rs', lines 339:4-339:73 *) -Fixpoint betree_ListPairU64T_partition_at_pivot - (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) : - result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T))) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match self with - | Betree_List_Cons hd tl => - let (i, t) := hd in - if i s>= pivot - then Ok (Betree_List_Nil, Betree_List_Cons (i, t) tl) - else ( - p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot; - let (ls0, ls1) := p in - Ok (Betree_List_Cons (i, t) ls0, ls1)) - | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil) - end - end -. - -(** [betree_main::betree::{betree_main::betree::Leaf#3}::split]: - Source: 'src/betree.rs', lines 359:4-364:17 *) -Definition betree_Leaf_split - (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64)) - (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) - (st : state) : - result (state * (betree_Internal_t * betree_NodeIdCounter_t)) - := - p <- - betree_List_split_at (u64 * u64) n content - params.(betree_Params_split_size); - let (content0, content1) := p in - p1 <- betree_List_hd (u64 * u64) content1; - let (pivot, _) := p1 in - p2 <- betree_NodeIdCounter_fresh_id node_id_cnt; - let (id0, node_id_cnt1) := p2 in - p3 <- betree_NodeIdCounter_fresh_id node_id_cnt1; - let (id1, node_id_cnt2) := p3 in - p4 <- betree_store_leaf_node id0 content0 st; - let (st1, _) := p4 in - p5 <- betree_store_leaf_node id1 content1 st1; - let (st2, _) := p5 in - let n1 := Betree_Node_Leaf - {| - betree_Leaf_id := id0; - betree_Leaf_size := params.(betree_Params_split_size) - |} in - let n2 := Betree_Node_Leaf - {| - betree_Leaf_id := id1; - betree_Leaf_size := params.(betree_Params_split_size) - |} in - Ok (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, - node_id_cnt2)) -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: - Source: 'src/betree.rs', lines 789:4-792:34 *) -Fixpoint betree_Node_lookup_first_message_for_key - (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : - result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 * - betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t)))) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match msgs with - | Betree_List_Cons x next_msgs => - let (i, m) := x in - if i s>= key - then Ok (Betree_List_Cons (i, m) next_msgs, Ok) - else ( - p <- betree_Node_lookup_first_message_for_key n1 key next_msgs; - let (l, lookup_first_message_for_key_back) := p in - let back := - fun (ret : betree_List_t (u64 * betree_Message_t)) => - next_msgs1 <- lookup_first_message_for_key_back ret; - Ok (Betree_List_Cons (i, m) next_msgs1) in - Ok (l, back)) - | Betree_List_Nil => Ok (Betree_List_Nil, Ok) - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: - Source: 'src/betree.rs', lines 636:4-636:80 *) -Fixpoint betree_Node_lookup_in_bindings - (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : - result (option u64) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match bindings with - | Betree_List_Cons hd tl => - let (i, i1) := hd in - if i s= key - then Ok (Some i1) - else - if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl - | Betree_List_Nil => Ok None - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: - Source: 'src/betree.rs', lines 819:4-819:90 *) -Fixpoint betree_Node_apply_upserts - (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) - (key : u64) : - result (u64 * (betree_List_t (u64 * betree_Message_t))) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - b <- betree_ListPairU64T_head_has_key betree_Message_t msgs key; - if b - then ( - p <- betree_List_pop_front (u64 * betree_Message_t) msgs; - let (msg, msgs1) := p in - let (_, m) := msg in - match m with - | Betree_Message_Insert _ => Fail_ Failure - | Betree_Message_Delete => Fail_ Failure - | Betree_Message_Upsert s => - v <- betree_upsert_update prev s; - betree_Node_apply_upserts n1 msgs1 (Some v) key - end) - else ( - v <- core_option_Option_unwrap u64 prev; - msgs1 <- - betree_List_push_front (u64 * betree_Message_t) msgs (key, - Betree_Message_Insert v); - Ok (v, msgs1)) - end -. - -(** [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: - Source: 'src/betree.rs', lines 395:4-395:63 *) -Fixpoint betree_Internal_lookup_in_children - (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : - result (state * ((option u64) * betree_Internal_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - if key s< self.(betree_Internal_pivot) - then ( - p <- betree_Node_lookup n1 self.(betree_Internal_left) key st; - let (st1, p1) := p in - let (o, n2) := p1 in - Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id) - self.(betree_Internal_pivot) n2 self.(betree_Internal_right)))) - else ( - p <- betree_Node_lookup n1 self.(betree_Internal_right) key st; - let (st1, p1) := p in - let (o, n2) := p1 in - Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id) - self.(betree_Internal_pivot) self.(betree_Internal_left) n2))) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup]: - Source: 'src/betree.rs', lines 709:4-709:58 *) -with betree_Node_lookup - (n : nat) (self : betree_Node_t) (key : u64) (st : state) : - result (state * ((option u64) * betree_Node_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match self with - | Betree_Node_Internal node => - p <- betree_load_internal_node node.(betree_Internal_id) st; - let (st1, msgs) := p in - p1 <- betree_Node_lookup_first_message_for_key n1 key msgs; - let (pending, lookup_first_message_for_key_back) := p1 in - match pending with - | Betree_List_Cons p2 l => - let (k, msg) := p2 in - if k s<> key - then ( - p3 <- betree_Internal_lookup_in_children n1 node key st1; - let (st2, p4) := p3 in - let (o, node1) := p4 in - _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l); - Ok (st2, (o, Betree_Node_Internal node1))) - else - match msg with - | Betree_Message_Insert v => - _ <- - lookup_first_message_for_key_back (Betree_List_Cons (k, - Betree_Message_Insert v) l); - Ok (st1, (Some v, Betree_Node_Internal node)) - | Betree_Message_Delete => - _ <- - lookup_first_message_for_key_back (Betree_List_Cons (k, - Betree_Message_Delete) l); - Ok (st1, (None, Betree_Node_Internal node)) - | Betree_Message_Upsert ufs => - p3 <- betree_Internal_lookup_in_children n1 node key st1; - let (st2, p4) := p3 in - let (v, node1) := p4 in - p5 <- - betree_Node_apply_upserts n1 (Betree_List_Cons (k, - Betree_Message_Upsert ufs) l) v key; - let (v1, pending1) := p5 in - msgs1 <- lookup_first_message_for_key_back pending1; - p6 <- - betree_store_internal_node node1.(betree_Internal_id) msgs1 st2; - let (st3, _) := p6 in - Ok (st3, (Some v1, Betree_Node_Internal node1)) - end - | Betree_List_Nil => - p2 <- betree_Internal_lookup_in_children n1 node key st1; - let (st2, p3) := p2 in - let (o, node1) := p3 in - _ <- lookup_first_message_for_key_back Betree_List_Nil; - Ok (st2, (o, Betree_Node_Internal node1)) - end - | Betree_Node_Leaf node => - p <- betree_load_leaf_node node.(betree_Leaf_id) st; - let (st1, bindings) := p in - o <- betree_Node_lookup_in_bindings n1 key bindings; - Ok (st1, (o, Betree_Node_Leaf node)) - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: - Source: 'src/betree.rs', lines 674:4-674:77 *) -Fixpoint betree_Node_filter_messages_for_key - (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : - result (betree_List_t (u64 * betree_Message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match msgs with - | Betree_List_Cons p l => - let (k, m) := p in - if k s= key - then ( - p1 <- - betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k, - m) l); - let (_, msgs1) := p1 in - betree_Node_filter_messages_for_key n1 key msgs1) - else Ok (Betree_List_Cons (k, m) l) - | Betree_List_Nil => Ok Betree_List_Nil - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: - Source: 'src/betree.rs', lines 689:4-692:34 *) -Fixpoint betree_Node_lookup_first_message_after_key - (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : - result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 * - betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t)))) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match msgs with - | Betree_List_Cons p next_msgs => - let (k, m) := p in - if k s= key - then ( - p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs; - let (l, lookup_first_message_after_key_back) := p1 in - let back := - fun (ret : betree_List_t (u64 * betree_Message_t)) => - next_msgs1 <- lookup_first_message_after_key_back ret; - Ok (Betree_List_Cons (k, m) next_msgs1) in - Ok (l, back)) - else Ok (Betree_List_Cons (k, m) next_msgs, Ok) - | Betree_List_Nil => Ok (Betree_List_Nil, Ok) - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: - Source: 'src/betree.rs', lines 521:4-521:89 *) -Definition betree_Node_apply_to_internal - (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64) - (new_msg : betree_Message_t) : - result (betree_List_t (u64 * betree_Message_t)) - := - p <- betree_Node_lookup_first_message_for_key n key msgs; - let (msgs1, lookup_first_message_for_key_back) := p in - b <- betree_ListPairU64T_head_has_key betree_Message_t msgs1 key; - if b - then - match new_msg with - | Betree_Message_Insert i => - msgs2 <- betree_Node_filter_messages_for_key n key msgs1; - msgs3 <- - betree_List_push_front (u64 * betree_Message_t) msgs2 (key, - Betree_Message_Insert i); - lookup_first_message_for_key_back msgs3 - | Betree_Message_Delete => - msgs2 <- betree_Node_filter_messages_for_key n key msgs1; - msgs3 <- - betree_List_push_front (u64 * betree_Message_t) msgs2 (key, - Betree_Message_Delete); - lookup_first_message_for_key_back msgs3 - | Betree_Message_Upsert s => - p1 <- betree_List_hd (u64 * betree_Message_t) msgs1; - let (_, m) := p1 in - match m with - | Betree_Message_Insert prev => - v <- betree_upsert_update (Some prev) s; - p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; - let (_, msgs2) := p2 in - msgs3 <- - betree_List_push_front (u64 * betree_Message_t) msgs2 (key, - Betree_Message_Insert v); - lookup_first_message_for_key_back msgs3 - | Betree_Message_Delete => - p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; - let (_, msgs2) := p2 in - v <- betree_upsert_update None s; - msgs3 <- - betree_List_push_front (u64 * betree_Message_t) msgs2 (key, - Betree_Message_Insert v); - lookup_first_message_for_key_back msgs3 - | Betree_Message_Upsert _ => - p2 <- betree_Node_lookup_first_message_after_key n key msgs1; - let (msgs2, lookup_first_message_after_key_back) := p2 in - msgs3 <- - betree_List_push_front (u64 * betree_Message_t) msgs2 (key, - Betree_Message_Upsert s); - msgs4 <- lookup_first_message_after_key_back msgs3; - lookup_first_message_for_key_back msgs4 - end - end - else ( - msgs2 <- - betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg); - lookup_first_message_for_key_back msgs2) -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: - Source: 'src/betree.rs', lines 502:4-505:5 *) -Fixpoint betree_Node_apply_messages_to_internal - (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) - (new_msgs : betree_List_t (u64 * betree_Message_t)) : - result (betree_List_t (u64 * betree_Message_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match new_msgs with - | Betree_List_Cons new_msg new_msgs_tl => - let (i, m) := new_msg in - msgs1 <- betree_Node_apply_to_internal n1 msgs i m; - betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl - | Betree_List_Nil => Ok msgs - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: - Source: 'src/betree.rs', lines 653:4-656:32 *) -Fixpoint betree_Node_lookup_mut_in_bindings - (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : - result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result - (betree_List_t (u64 * u64)))) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match bindings with - | Betree_List_Cons hd tl => - let (i, i1) := hd in - if i s>= key - then Ok (Betree_List_Cons (i, i1) tl, Ok) - else ( - p <- betree_Node_lookup_mut_in_bindings n1 key tl; - let (l, lookup_mut_in_bindings_back) := p in - let back := - fun (ret : betree_List_t (u64 * u64)) => - tl1 <- lookup_mut_in_bindings_back ret; - Ok (Betree_List_Cons (i, i1) tl1) in - Ok (l, back)) - | Betree_List_Nil => Ok (Betree_List_Nil, Ok) - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: - Source: 'src/betree.rs', lines 460:4-460:87 *) -Definition betree_Node_apply_to_leaf - (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64) - (new_msg : betree_Message_t) : - result (betree_List_t (u64 * u64)) - := - p <- betree_Node_lookup_mut_in_bindings n key bindings; - let (bindings1, lookup_mut_in_bindings_back) := p in - b <- betree_ListPairU64T_head_has_key u64 bindings1 key; - if b - then ( - p1 <- betree_List_pop_front (u64 * u64) bindings1; - let (hd, bindings2) := p1 in - match new_msg with - | Betree_Message_Insert v => - bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v); - lookup_mut_in_bindings_back bindings3 - | Betree_Message_Delete => lookup_mut_in_bindings_back bindings2 - | Betree_Message_Upsert s => - let (_, i) := hd in - v <- betree_upsert_update (Some i) s; - bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v); - lookup_mut_in_bindings_back bindings3 - end) - else - match new_msg with - | Betree_Message_Insert v => - bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); - lookup_mut_in_bindings_back bindings2 - | Betree_Message_Delete => lookup_mut_in_bindings_back bindings1 - | Betree_Message_Upsert s => - v <- betree_upsert_update None s; - bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); - lookup_mut_in_bindings_back bindings2 - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: - Source: 'src/betree.rs', lines 444:4-447:5 *) -Fixpoint betree_Node_apply_messages_to_leaf - (n : nat) (bindings : betree_List_t (u64 * u64)) - (new_msgs : betree_List_t (u64 * betree_Message_t)) : - result (betree_List_t (u64 * u64)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match new_msgs with - | Betree_List_Cons new_msg new_msgs_tl => - let (i, m) := new_msg in - bindings1 <- betree_Node_apply_to_leaf n1 bindings i m; - betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl - | Betree_List_Nil => Ok bindings - end - end -. - -(** [betree_main::betree::{betree_main::betree::Internal#4}::flush]: - Source: 'src/betree.rs', lines 410:4-415:26 *) -Fixpoint betree_Internal_flush - (n : nat) (self : betree_Internal_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) - (content : betree_List_t (u64 * betree_Message_t)) (st : state) : - result (state * ((betree_List_t (u64 * betree_Message_t)) * - (betree_Internal_t * betree_NodeIdCounter_t))) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - p <- - betree_ListPairU64T_partition_at_pivot betree_Message_t n1 content - self.(betree_Internal_pivot); - let (msgs_left, msgs_right) := p in - len_left <- betree_List_len (u64 * betree_Message_t) n1 msgs_left; - if len_left s>= params.(betree_Params_min_flush_size) - then ( - p1 <- - betree_Node_apply_messages n1 self.(betree_Internal_left) params - node_id_cnt msgs_left st; - let (st1, p2) := p1 in - let (n2, node_id_cnt1) := p2 in - len_right <- betree_List_len (u64 * betree_Message_t) n1 msgs_right; - if len_right s>= params.(betree_Params_min_flush_size) - then ( - p3 <- - betree_Node_apply_messages n1 self.(betree_Internal_right) params - node_id_cnt1 msgs_right st1; - let (st2, p4) := p3 in - let (n3, node_id_cnt2) := p4 in - Ok (st2, (Betree_List_Nil, (mkbetree_Internal_t - self.(betree_Internal_id) self.(betree_Internal_pivot) n2 n3, - node_id_cnt2)))) - else - Ok (st1, (msgs_right, (mkbetree_Internal_t self.(betree_Internal_id) - self.(betree_Internal_pivot) n2 self.(betree_Internal_right), - node_id_cnt1)))) - else ( - p1 <- - betree_Node_apply_messages n1 self.(betree_Internal_right) params - node_id_cnt msgs_right st; - let (st1, p2) := p1 in - let (n2, node_id_cnt1) := p2 in - Ok (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id) - self.(betree_Internal_pivot) self.(betree_Internal_left) n2, - node_id_cnt1)))) - end - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: - Source: 'src/betree.rs', lines 588:4-593:5 *) -with betree_Node_apply_messages - (n : nat) (self : betree_Node_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) - (msgs : betree_List_t (u64 * betree_Message_t)) (st : state) : - result (state * (betree_Node_t * betree_NodeIdCounter_t)) - := - match n with - | O => Fail_ OutOfFuel - | S n1 => - match self with - | Betree_Node_Internal node => - p <- betree_load_internal_node node.(betree_Internal_id) st; - let (st1, content) := p in - content1 <- betree_Node_apply_messages_to_internal n1 content msgs; - num_msgs <- betree_List_len (u64 * betree_Message_t) n1 content1; - if num_msgs s>= params.(betree_Params_min_flush_size) - then ( - p1 <- betree_Internal_flush n1 node params node_id_cnt content1 st1; - let (st2, p2) := p1 in - let (content2, p3) := p2 in - let (node1, node_id_cnt1) := p3 in - p4 <- - betree_store_internal_node node1.(betree_Internal_id) content2 st2; - let (st3, _) := p4 in - Ok (st3, (Betree_Node_Internal node1, node_id_cnt1))) - else ( - p1 <- - betree_store_internal_node node.(betree_Internal_id) content1 st1; - let (st2, _) := p1 in - Ok (st2, (Betree_Node_Internal node, node_id_cnt))) - | Betree_Node_Leaf node => - p <- betree_load_leaf_node node.(betree_Leaf_id) st; - let (st1, content) := p in - content1 <- betree_Node_apply_messages_to_leaf n1 content msgs; - len <- betree_List_len (u64 * u64) n1 content1; - i <- u64_mul 2%u64 params.(betree_Params_split_size); - if len s>= i - then ( - p1 <- betree_Leaf_split n1 node content1 params node_id_cnt st1; - let (st2, p2) := p1 in - let (new_node, node_id_cnt1) := p2 in - p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2; - let (st3, _) := p3 in - Ok (st3, (Betree_Node_Internal new_node, node_id_cnt1))) - else ( - p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1; - let (st2, _) := p1 in - Ok (st2, (Betree_Node_Leaf - {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len - |}, node_id_cnt))) - end - end -. - -(** [betree_main::betree::{betree_main::betree::Node#5}::apply]: - Source: 'src/betree.rs', lines 576:4-582:5 *) -Definition betree_Node_apply - (n : nat) (self : betree_Node_t) (params : betree_Params_t) - (node_id_cnt : betree_NodeIdCounter_t) (key : u64) - (new_msg : betree_Message_t) (st : state) : - result (state * (betree_Node_t * betree_NodeIdCounter_t)) - := - p <- - betree_Node_apply_messages n self params node_id_cnt (Betree_List_Cons - (key, new_msg) Betree_List_Nil) st; - let (st1, p1) := p in - let (self1, node_id_cnt1) := p1 in - Ok (st1, (self1, node_id_cnt1)) -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::new]: - Source: 'src/betree.rs', lines 849:4-849:60 *) -Definition betree_BeTree_new - (min_flush_size : u64) (split_size : u64) (st : state) : - result (state * betree_BeTree_t) - := - node_id_cnt <- betree_NodeIdCounter_new; - p <- betree_NodeIdCounter_fresh_id node_id_cnt; - let (id, node_id_cnt1) := p in - p1 <- betree_store_leaf_node id Betree_List_Nil st; - let (st1, _) := p1 in - Ok (st1, - {| - betree_BeTree_params := - {| - betree_Params_min_flush_size := min_flush_size; - betree_Params_split_size := split_size - |}; - betree_BeTree_node_id_cnt := node_id_cnt1; - betree_BeTree_root := - (Betree_Node_Leaf - {| betree_Leaf_id := id; betree_Leaf_size := 0%u64 |}) - |}) -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: - Source: 'src/betree.rs', lines 868:4-868:47 *) -Definition betree_BeTree_apply - (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) - (st : state) : - result (state * betree_BeTree_t) - := - p <- - betree_Node_apply n self.(betree_BeTree_root) self.(betree_BeTree_params) - self.(betree_BeTree_node_id_cnt) key msg st; - let (st1, p1) := p in - let (n1, nic) := p1 in - Ok (st1, - {| - betree_BeTree_params := self.(betree_BeTree_params); - betree_BeTree_node_id_cnt := nic; - betree_BeTree_root := n1 - |}) -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: - Source: 'src/betree.rs', lines 874:4-874:52 *) -Definition betree_BeTree_insert - (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : - result (state * betree_BeTree_t) - := - betree_BeTree_apply n self key (Betree_Message_Insert value) st -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: - Source: 'src/betree.rs', lines 880:4-880:38 *) -Definition betree_BeTree_delete - (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : - result (state * betree_BeTree_t) - := - betree_BeTree_apply n self key Betree_Message_Delete st -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: - Source: 'src/betree.rs', lines 886:4-886:59 *) -Definition betree_BeTree_upsert - (n : nat) (self : betree_BeTree_t) (key : u64) - (upd : betree_UpsertFunState_t) (st : state) : - result (state * betree_BeTree_t) - := - betree_BeTree_apply n self key (Betree_Message_Upsert upd) st -. - -(** [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: - Source: 'src/betree.rs', lines 895:4-895:62 *) -Definition betree_BeTree_lookup - (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : - result (state * ((option u64) * betree_BeTree_t)) - := - p <- betree_Node_lookup n self.(betree_BeTree_root) key st; - let (st1, p1) := p in - let (o, n1) := p1 in - Ok (st1, (o, - {| - betree_BeTree_params := self.(betree_BeTree_params); - betree_BeTree_node_id_cnt := self.(betree_BeTree_node_id_cnt); - betree_BeTree_root := n1 - |})) -. - -(** [betree_main::main]: - Source: 'src/main.rs', lines 4:0-4:9 *) -Definition main : result unit := - Ok tt. - -(** Unit test for [betree_main::main] *) -Check (main )%return. - -End BetreeMain_Funs. diff --git a/tests/coq/betree/BetreeMain_FunsExternal.v b/tests/coq/betree/BetreeMain_FunsExternal.v deleted file mode 100644 index 099a2e8f..00000000 --- a/tests/coq/betree/BetreeMain_FunsExternal.v +++ /dev/null @@ -1,39 +0,0 @@ -(** [betree_main]: external functions. --- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Require Export BetreeMain_Types. -Import BetreeMain_Types. -Module BetreeMain_FunsExternal. - -(** [betree_main::betree_utils::load_internal_node]: forward function - Source: 'src/betree_utils.rs', lines 98:0-98:63 *) -Axiom betree_utils_load_internal_node - : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t))) -. - -(** [betree_main::betree_utils::store_internal_node]: forward function - Source: 'src/betree_utils.rs', lines 115:0-115:71 *) -Axiom betree_utils_store_internal_node - : - u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state * - unit) -. - -(** [betree_main::betree_utils::load_leaf_node]: forward function - Source: 'src/betree_utils.rs', lines 132:0-132:55 *) -Axiom betree_utils_load_leaf_node - : u64 -> state -> result (state * (betree_List_t (u64 * u64))) -. - -(** [betree_main::betree_utils::store_leaf_node]: forward function - Source: 'src/betree_utils.rs', lines 145:0-145:63 *) -Axiom betree_utils_store_leaf_node - : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) -. - -End BetreeMain_FunsExternal. diff --git a/tests/coq/betree/BetreeMain_FunsExternal_Template.v b/tests/coq/betree/BetreeMain_FunsExternal_Template.v deleted file mode 100644 index 58be2733..00000000 --- a/tests/coq/betree/BetreeMain_FunsExternal_Template.v +++ /dev/null @@ -1,40 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external functions. --- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Require Import BetreeMain_Types. -Include BetreeMain_Types. -Module BetreeMain_FunsExternal_Template. - -(** [betree_main::betree_utils::load_internal_node]: - Source: 'src/betree_utils.rs', lines 98:0-98:63 *) -Axiom betree_utils_load_internal_node - : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t))) -. - -(** [betree_main::betree_utils::store_internal_node]: - Source: 'src/betree_utils.rs', lines 115:0-115:71 *) -Axiom betree_utils_store_internal_node - : - u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state * - unit) -. - -(** [betree_main::betree_utils::load_leaf_node]: - Source: 'src/betree_utils.rs', lines 132:0-132:55 *) -Axiom betree_utils_load_leaf_node - : u64 -> state -> result (state * (betree_List_t (u64 * u64))) -. - -(** [betree_main::betree_utils::store_leaf_node]: - Source: 'src/betree_utils.rs', lines 145:0-145:63 *) -Axiom betree_utils_store_leaf_node - : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) -. - -End BetreeMain_FunsExternal_Template. diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v deleted file mode 100644 index acbc2085..00000000 --- a/tests/coq/betree/BetreeMain_Types.v +++ /dev/null @@ -1,118 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: type definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Require Import BetreeMain_TypesExternal. -Include BetreeMain_TypesExternal. -Module BetreeMain_Types. - -(** [betree_main::betree::List] - Source: 'src/betree.rs', lines 17:0-17:23 *) -Inductive betree_List_t (T : Type) := -| Betree_List_Cons : T -> betree_List_t T -> betree_List_t T -| Betree_List_Nil : betree_List_t T -. - -Arguments Betree_List_Cons { _ }. -Arguments Betree_List_Nil { _ }. - -(** [betree_main::betree::UpsertFunState] - Source: 'src/betree.rs', lines 63:0-63:23 *) -Inductive betree_UpsertFunState_t := -| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t -| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t -. - -(** [betree_main::betree::Message] - Source: 'src/betree.rs', lines 69:0-69:23 *) -Inductive betree_Message_t := -| Betree_Message_Insert : u64 -> betree_Message_t -| Betree_Message_Delete : betree_Message_t -| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t -. - -(** [betree_main::betree::Leaf] - Source: 'src/betree.rs', lines 167:0-167:11 *) -Record betree_Leaf_t := -mkbetree_Leaf_t { - betree_Leaf_id : u64; betree_Leaf_size : u64; -} -. - -(** [betree_main::betree::Internal] - Source: 'src/betree.rs', lines 156:0-156:15 *) -Inductive betree_Internal_t := -| mkbetree_Internal_t : - u64 -> - u64 -> - betree_Node_t -> - betree_Node_t -> - betree_Internal_t - -(** [betree_main::betree::Node] - Source: 'src/betree.rs', lines 179:0-179:9 *) -with betree_Node_t := -| Betree_Node_Internal : betree_Internal_t -> betree_Node_t -| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t -. - -Definition betree_Internal_id (x : betree_Internal_t) := - match x with | mkbetree_Internal_t x1 _ _ _ => x1 end -. - -Notation "x2 .(betree_Internal_id)" := (betree_Internal_id x2) (at level 9). - -Definition betree_Internal_pivot (x : betree_Internal_t) := - match x with | mkbetree_Internal_t _ x1 _ _ => x1 end -. - -Notation "x2 .(betree_Internal_pivot)" := (betree_Internal_pivot x2) - (at level 9) -. - -Definition betree_Internal_left (x : betree_Internal_t) := - match x with | mkbetree_Internal_t _ _ x1 _ => x1 end -. - -Notation "x2 .(betree_Internal_left)" := (betree_Internal_left x2) (at level 9) -. - -Definition betree_Internal_right (x : betree_Internal_t) := - match x with | mkbetree_Internal_t _ _ _ x1 => x1 end -. - -Notation "x2 .(betree_Internal_right)" := (betree_Internal_right x2) - (at level 9) -. - -(** [betree_main::betree::Params] - Source: 'src/betree.rs', lines 187:0-187:13 *) -Record betree_Params_t := -mkbetree_Params_t { - betree_Params_min_flush_size : u64; betree_Params_split_size : u64; -} -. - -(** [betree_main::betree::NodeIdCounter] - Source: 'src/betree.rs', lines 201:0-201:20 *) -Record betree_NodeIdCounter_t := -mkbetree_NodeIdCounter_t { - betree_NodeIdCounter_next_node_id : u64; -} -. - -(** [betree_main::betree::BeTree] - Source: 'src/betree.rs', lines 218:0-218:17 *) -Record betree_BeTree_t := -mkbetree_BeTree_t { - betree_BeTree_params : betree_Params_t; - betree_BeTree_node_id_cnt : betree_NodeIdCounter_t; - betree_BeTree_root : betree_Node_t; -} -. - -End BetreeMain_Types. diff --git a/tests/coq/betree/BetreeMain_TypesExternal.v b/tests/coq/betree/BetreeMain_TypesExternal.v deleted file mode 100644 index 870d2601..00000000 --- a/tests/coq/betree/BetreeMain_TypesExternal.v +++ /dev/null @@ -1,14 +0,0 @@ -(** [betree_main]: external types. --- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Module BetreeMain_TypesExternal. - -(** The state type used in the state-error monad *) -Axiom state : Type. - -End BetreeMain_TypesExternal. diff --git a/tests/coq/betree/BetreeMain_TypesExternal_Template.v b/tests/coq/betree/BetreeMain_TypesExternal_Template.v deleted file mode 100644 index 651de2b7..00000000 --- a/tests/coq/betree/BetreeMain_TypesExternal_Template.v +++ /dev/null @@ -1,15 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external types. --- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Module BetreeMain_TypesExternal_Template. - -(** The state type used in the state-error monad *) -Axiom state : Type. - -End BetreeMain_TypesExternal_Template. diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v new file mode 100644 index 00000000..b965d423 --- /dev/null +++ b/tests/coq/betree/Betree_Funs.v @@ -0,0 +1,837 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree]: function definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Import Betree_Types. +Include Betree_Types. +Require Import Betree_FunsExternal. +Include Betree_FunsExternal. +Module Betree_Funs. + +(** [betree::betree::load_internal_node]: + Source: 'src/betree.rs', lines 36:0-36:52 *) +Definition betree_load_internal_node + (id : u64) (st : state) : + result (state * (betree_List_t (u64 * betree_Message_t))) + := + betree_utils_load_internal_node id st +. + +(** [betree::betree::store_internal_node]: + Source: 'src/betree.rs', lines 41:0-41:60 *) +Definition betree_store_internal_node + (id : u64) (content : betree_List_t (u64 * betree_Message_t)) (st : state) : + result (state * unit) + := + betree_utils_store_internal_node id content st +. + +(** [betree::betree::load_leaf_node]: + Source: 'src/betree.rs', lines 46:0-46:44 *) +Definition betree_load_leaf_node + (id : u64) (st : state) : result (state * (betree_List_t (u64 * u64))) := + betree_utils_load_leaf_node id st +. + +(** [betree::betree::store_leaf_node]: + Source: 'src/betree.rs', lines 51:0-51:52 *) +Definition betree_store_leaf_node + (id : u64) (content : betree_List_t (u64 * u64)) (st : state) : + result (state * unit) + := + betree_utils_store_leaf_node id content st +. + +(** [betree::betree::fresh_node_id]: + Source: 'src/betree.rs', lines 55:0-55:48 *) +Definition betree_fresh_node_id (counter : u64) : result (u64 * u64) := + counter1 <- u64_add counter 1%u64; Ok (counter, counter1) +. + +(** [betree::betree::{betree::betree::NodeIdCounter}::new]: + Source: 'src/betree.rs', lines 206:4-206:20 *) +Definition betree_NodeIdCounter_new : result betree_NodeIdCounter_t := + Ok {| betree_NodeIdCounter_next_node_id := 0%u64 |} +. + +(** [betree::betree::{betree::betree::NodeIdCounter}::fresh_id]: + Source: 'src/betree.rs', lines 210:4-210:36 *) +Definition betree_NodeIdCounter_fresh_id + (self : betree_NodeIdCounter_t) : result (u64 * betree_NodeIdCounter_t) := + i <- u64_add self.(betree_NodeIdCounter_next_node_id) 1%u64; + Ok (self.(betree_NodeIdCounter_next_node_id), + {| betree_NodeIdCounter_next_node_id := i |}) +. + +(** [betree::betree::upsert_update]: + Source: 'src/betree.rs', lines 234:0-234:70 *) +Definition betree_upsert_update + (prev : option u64) (st : betree_UpsertFunState_t) : result u64 := + match prev with + | None => + match st with + | Betree_UpsertFunState_Add v => Ok v + | Betree_UpsertFunState_Sub _ => Ok 0%u64 + end + | Some prev1 => + match st with + | Betree_UpsertFunState_Add v => + margin <- u64_sub core_u64_max prev1; + if margin s>= v then u64_add prev1 v else Ok core_u64_max + | Betree_UpsertFunState_Sub v => + if prev1 s>= v then u64_sub prev1 v else Ok 0%u64 + end + end +. + +(** [betree::betree::{betree::betree::List#1}::len]: + Source: 'src/betree.rs', lines 276:4-276:24 *) +Fixpoint betree_List_len + (T : Type) (n : nat) (self : betree_List_t T) : result u64 := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match self with + | Betree_List_Cons _ tl => i <- betree_List_len T n1 tl; u64_add 1%u64 i + | Betree_List_Nil => Ok 0%u64 + end + end +. + +(** [betree::betree::{betree::betree::List#1}::split_at]: + Source: 'src/betree.rs', lines 284:4-284:51 *) +Fixpoint betree_List_split_at + (T : Type) (n : nat) (self : betree_List_t T) (n1 : u64) : + result ((betree_List_t T) * (betree_List_t T)) + := + match n with + | O => Fail_ OutOfFuel + | S n2 => + if n1 s= 0%u64 + then Ok (Betree_List_Nil, self) + else + match self with + | Betree_List_Cons hd tl => + i <- u64_sub n1 1%u64; + p <- betree_List_split_at T n2 tl i; + let (ls0, ls1) := p in + Ok (Betree_List_Cons hd ls0, ls1) + | Betree_List_Nil => Fail_ Failure + end + end +. + +(** [betree::betree::{betree::betree::List#1}::push_front]: + Source: 'src/betree.rs', lines 299:4-299:34 *) +Definition betree_List_push_front + (T : Type) (self : betree_List_t T) (x : T) : result (betree_List_t T) := + let (tl, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in + Ok (Betree_List_Cons x tl) +. + +(** [betree::betree::{betree::betree::List#1}::pop_front]: + Source: 'src/betree.rs', lines 306:4-306:32 *) +Definition betree_List_pop_front + (T : Type) (self : betree_List_t T) : result (T * (betree_List_t T)) := + let (ls, _) := core_mem_replace (betree_List_t T) self Betree_List_Nil in + match ls with + | Betree_List_Cons x tl => Ok (x, tl) + | Betree_List_Nil => Fail_ Failure + end +. + +(** [betree::betree::{betree::betree::List#1}::hd]: + Source: 'src/betree.rs', lines 318:4-318:22 *) +Definition betree_List_hd (T : Type) (self : betree_List_t T) : result T := + match self with + | Betree_List_Cons hd _ => Ok hd + | Betree_List_Nil => Fail_ Failure + end +. + +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::head_has_key]: + Source: 'src/betree.rs', lines 327:4-327:44 *) +Definition betree_ListPairU64T_head_has_key + (T : Type) (self : betree_List_t (u64 * T)) (key : u64) : result bool := + match self with + | Betree_List_Cons hd _ => let (i, _) := hd in Ok (i s= key) + | Betree_List_Nil => Ok false + end +. + +(** [betree::betree::{betree::betree::List<(u64, T)>#2}::partition_at_pivot]: + Source: 'src/betree.rs', lines 339:4-339:73 *) +Fixpoint betree_ListPairU64T_partition_at_pivot + (T : Type) (n : nat) (self : betree_List_t (u64 * T)) (pivot : u64) : + result ((betree_List_t (u64 * T)) * (betree_List_t (u64 * T))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match self with + | Betree_List_Cons hd tl => + let (i, t) := hd in + if i s>= pivot + then Ok (Betree_List_Nil, Betree_List_Cons (i, t) tl) + else ( + p <- betree_ListPairU64T_partition_at_pivot T n1 tl pivot; + let (ls0, ls1) := p in + Ok (Betree_List_Cons (i, t) ls0, ls1)) + | Betree_List_Nil => Ok (Betree_List_Nil, Betree_List_Nil) + end + end +. + +(** [betree::betree::{betree::betree::Leaf#3}::split]: + Source: 'src/betree.rs', lines 359:4-364:17 *) +Definition betree_Leaf_split + (n : nat) (self : betree_Leaf_t) (content : betree_List_t (u64 * u64)) + (params : betree_Params_t) (node_id_cnt : betree_NodeIdCounter_t) + (st : state) : + result (state * (betree_Internal_t * betree_NodeIdCounter_t)) + := + p <- + betree_List_split_at (u64 * u64) n content + params.(betree_Params_split_size); + let (content0, content1) := p in + p1 <- betree_List_hd (u64 * u64) content1; + let (pivot, _) := p1 in + p2 <- betree_NodeIdCounter_fresh_id node_id_cnt; + let (id0, node_id_cnt1) := p2 in + p3 <- betree_NodeIdCounter_fresh_id node_id_cnt1; + let (id1, node_id_cnt2) := p3 in + p4 <- betree_store_leaf_node id0 content0 st; + let (st1, _) := p4 in + p5 <- betree_store_leaf_node id1 content1 st1; + let (st2, _) := p5 in + let n1 := Betree_Node_Leaf + {| + betree_Leaf_id := id0; + betree_Leaf_size := params.(betree_Params_split_size) + |} in + let n2 := Betree_Node_Leaf + {| + betree_Leaf_id := id1; + betree_Leaf_size := params.(betree_Params_split_size) + |} in + Ok (st2, (mkbetree_Internal_t self.(betree_Leaf_id) pivot n1 n2, + node_id_cnt2)) +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_for_key]: + Source: 'src/betree.rs', lines 789:4-792:34 *) +Fixpoint betree_Node_lookup_first_message_for_key + (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : + result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 * + betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t)))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match msgs with + | Betree_List_Cons x next_msgs => + let (i, m) := x in + if i s>= key + then Ok (Betree_List_Cons (i, m) next_msgs, Ok) + else ( + p <- betree_Node_lookup_first_message_for_key n1 key next_msgs; + let (l, lookup_first_message_for_key_back) := p in + let back := + fun (ret : betree_List_t (u64 * betree_Message_t)) => + next_msgs1 <- lookup_first_message_for_key_back ret; + Ok (Betree_List_Cons (i, m) next_msgs1) in + Ok (l, back)) + | Betree_List_Nil => Ok (Betree_List_Nil, Ok) + end + end +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_in_bindings]: + Source: 'src/betree.rs', lines 636:4-636:80 *) +Fixpoint betree_Node_lookup_in_bindings + (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : + result (option u64) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match bindings with + | Betree_List_Cons hd tl => + let (i, i1) := hd in + if i s= key + then Ok (Some i1) + else + if i s> key then Ok None else betree_Node_lookup_in_bindings n1 key tl + | Betree_List_Nil => Ok None + end + end +. + +(** [betree::betree::{betree::betree::Node#5}::apply_upserts]: + Source: 'src/betree.rs', lines 819:4-819:90 *) +Fixpoint betree_Node_apply_upserts + (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (prev : option u64) + (key : u64) : + result (u64 * (betree_List_t (u64 * betree_Message_t))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + b <- betree_ListPairU64T_head_has_key betree_Message_t msgs key; + if b + then ( + p <- betree_List_pop_front (u64 * betree_Message_t) msgs; + let (msg, msgs1) := p in + let (_, m) := msg in + match m with + | Betree_Message_Insert _ => Fail_ Failure + | Betree_Message_Delete => Fail_ Failure + | Betree_Message_Upsert s => + v <- betree_upsert_update prev s; + betree_Node_apply_upserts n1 msgs1 (Some v) key + end) + else ( + v <- core_option_Option_unwrap u64 prev; + msgs1 <- + betree_List_push_front (u64 * betree_Message_t) msgs (key, + Betree_Message_Insert v); + Ok (v, msgs1)) + end +. + +(** [betree::betree::{betree::betree::Internal#4}::lookup_in_children]: + Source: 'src/betree.rs', lines 395:4-395:63 *) +Fixpoint betree_Internal_lookup_in_children + (n : nat) (self : betree_Internal_t) (key : u64) (st : state) : + result (state * ((option u64) * betree_Internal_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + if key s< self.(betree_Internal_pivot) + then ( + p <- betree_Node_lookup n1 self.(betree_Internal_left) key st; + let (st1, p1) := p in + let (o, n2) := p1 in + Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id) + self.(betree_Internal_pivot) n2 self.(betree_Internal_right)))) + else ( + p <- betree_Node_lookup n1 self.(betree_Internal_right) key st; + let (st1, p1) := p in + let (o, n2) := p1 in + Ok (st1, (o, mkbetree_Internal_t self.(betree_Internal_id) + self.(betree_Internal_pivot) self.(betree_Internal_left) n2))) + end + +(** [betree::betree::{betree::betree::Node#5}::lookup]: + Source: 'src/betree.rs', lines 709:4-709:58 *) +with betree_Node_lookup + (n : nat) (self : betree_Node_t) (key : u64) (st : state) : + result (state * ((option u64) * betree_Node_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match self with + | Betree_Node_Internal node => + p <- betree_load_internal_node node.(betree_Internal_id) st; + let (st1, msgs) := p in + p1 <- betree_Node_lookup_first_message_for_key n1 key msgs; + let (pending, lookup_first_message_for_key_back) := p1 in + match pending with + | Betree_List_Cons p2 l => + let (k, msg) := p2 in + if k s<> key + then ( + p3 <- betree_Internal_lookup_in_children n1 node key st1; + let (st2, p4) := p3 in + let (o, node1) := p4 in + _ <- lookup_first_message_for_key_back (Betree_List_Cons (k, msg) l); + Ok (st2, (o, Betree_Node_Internal node1))) + else + match msg with + | Betree_Message_Insert v => + _ <- + lookup_first_message_for_key_back (Betree_List_Cons (k, + Betree_Message_Insert v) l); + Ok (st1, (Some v, Betree_Node_Internal node)) + | Betree_Message_Delete => + _ <- + lookup_first_message_for_key_back (Betree_List_Cons (k, + Betree_Message_Delete) l); + Ok (st1, (None, Betree_Node_Internal node)) + | Betree_Message_Upsert ufs => + p3 <- betree_Internal_lookup_in_children n1 node key st1; + let (st2, p4) := p3 in + let (v, node1) := p4 in + p5 <- + betree_Node_apply_upserts n1 (Betree_List_Cons (k, + Betree_Message_Upsert ufs) l) v key; + let (v1, pending1) := p5 in + msgs1 <- lookup_first_message_for_key_back pending1; + p6 <- + betree_store_internal_node node1.(betree_Internal_id) msgs1 st2; + let (st3, _) := p6 in + Ok (st3, (Some v1, Betree_Node_Internal node1)) + end + | Betree_List_Nil => + p2 <- betree_Internal_lookup_in_children n1 node key st1; + let (st2, p3) := p2 in + let (o, node1) := p3 in + _ <- lookup_first_message_for_key_back Betree_List_Nil; + Ok (st2, (o, Betree_Node_Internal node1)) + end + | Betree_Node_Leaf node => + p <- betree_load_leaf_node node.(betree_Leaf_id) st; + let (st1, bindings) := p in + o <- betree_Node_lookup_in_bindings n1 key bindings; + Ok (st1, (o, Betree_Node_Leaf node)) + end + end +. + +(** [betree::betree::{betree::betree::Node#5}::filter_messages_for_key]: + Source: 'src/betree.rs', lines 674:4-674:77 *) +Fixpoint betree_Node_filter_messages_for_key + (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : + result (betree_List_t (u64 * betree_Message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match msgs with + | Betree_List_Cons p l => + let (k, m) := p in + if k s= key + then ( + p1 <- + betree_List_pop_front (u64 * betree_Message_t) (Betree_List_Cons (k, + m) l); + let (_, msgs1) := p1 in + betree_Node_filter_messages_for_key n1 key msgs1) + else Ok (Betree_List_Cons (k, m) l) + | Betree_List_Nil => Ok Betree_List_Nil + end + end +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_first_message_after_key]: + Source: 'src/betree.rs', lines 689:4-692:34 *) +Fixpoint betree_Node_lookup_first_message_after_key + (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) : + result ((betree_List_t (u64 * betree_Message_t)) * (betree_List_t (u64 * + betree_Message_t) -> result (betree_List_t (u64 * betree_Message_t)))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match msgs with + | Betree_List_Cons p next_msgs => + let (k, m) := p in + if k s= key + then ( + p1 <- betree_Node_lookup_first_message_after_key n1 key next_msgs; + let (l, lookup_first_message_after_key_back) := p1 in + let back := + fun (ret : betree_List_t (u64 * betree_Message_t)) => + next_msgs1 <- lookup_first_message_after_key_back ret; + Ok (Betree_List_Cons (k, m) next_msgs1) in + Ok (l, back)) + else Ok (Betree_List_Cons (k, m) next_msgs, Ok) + | Betree_List_Nil => Ok (Betree_List_Nil, Ok) + end + end +. + +(** [betree::betree::{betree::betree::Node#5}::apply_to_internal]: + Source: 'src/betree.rs', lines 521:4-521:89 *) +Definition betree_Node_apply_to_internal + (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) (key : u64) + (new_msg : betree_Message_t) : + result (betree_List_t (u64 * betree_Message_t)) + := + p <- betree_Node_lookup_first_message_for_key n key msgs; + let (msgs1, lookup_first_message_for_key_back) := p in + b <- betree_ListPairU64T_head_has_key betree_Message_t msgs1 key; + if b + then + match new_msg with + | Betree_Message_Insert i => + msgs2 <- betree_Node_filter_messages_for_key n key msgs1; + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, + Betree_Message_Insert i); + lookup_first_message_for_key_back msgs3 + | Betree_Message_Delete => + msgs2 <- betree_Node_filter_messages_for_key n key msgs1; + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, + Betree_Message_Delete); + lookup_first_message_for_key_back msgs3 + | Betree_Message_Upsert s => + p1 <- betree_List_hd (u64 * betree_Message_t) msgs1; + let (_, m) := p1 in + match m with + | Betree_Message_Insert prev => + v <- betree_upsert_update (Some prev) s; + p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; + let (_, msgs2) := p2 in + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, + Betree_Message_Insert v); + lookup_first_message_for_key_back msgs3 + | Betree_Message_Delete => + p2 <- betree_List_pop_front (u64 * betree_Message_t) msgs1; + let (_, msgs2) := p2 in + v <- betree_upsert_update None s; + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, + Betree_Message_Insert v); + lookup_first_message_for_key_back msgs3 + | Betree_Message_Upsert _ => + p2 <- betree_Node_lookup_first_message_after_key n key msgs1; + let (msgs2, lookup_first_message_after_key_back) := p2 in + msgs3 <- + betree_List_push_front (u64 * betree_Message_t) msgs2 (key, + Betree_Message_Upsert s); + msgs4 <- lookup_first_message_after_key_back msgs3; + lookup_first_message_for_key_back msgs4 + end + end + else ( + msgs2 <- + betree_List_push_front (u64 * betree_Message_t) msgs1 (key, new_msg); + lookup_first_message_for_key_back msgs2) +. + +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_internal]: + Source: 'src/betree.rs', lines 502:4-505:5 *) +Fixpoint betree_Node_apply_messages_to_internal + (n : nat) (msgs : betree_List_t (u64 * betree_Message_t)) + (new_msgs : betree_List_t (u64 * betree_Message_t)) : + result (betree_List_t (u64 * betree_Message_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match new_msgs with + | Betree_List_Cons new_msg new_msgs_tl => + let (i, m) := new_msg in + msgs1 <- betree_Node_apply_to_internal n1 msgs i m; + betree_Node_apply_messages_to_internal n1 msgs1 new_msgs_tl + | Betree_List_Nil => Ok msgs + end + end +. + +(** [betree::betree::{betree::betree::Node#5}::lookup_mut_in_bindings]: + Source: 'src/betree.rs', lines 653:4-656:32 *) +Fixpoint betree_Node_lookup_mut_in_bindings + (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) : + result ((betree_List_t (u64 * u64)) * (betree_List_t (u64 * u64) -> result + (betree_List_t (u64 * u64)))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match bindings with + | Betree_List_Cons hd tl => + let (i, i1) := hd in + if i s>= key + then Ok (Betree_List_Cons (i, i1) tl, Ok) + else ( + p <- betree_Node_lookup_mut_in_bindings n1 key tl; + let (l, lookup_mut_in_bindings_back) := p in + let back := + fun (ret : betree_List_t (u64 * u64)) => + tl1 <- lookup_mut_in_bindings_back ret; + Ok (Betree_List_Cons (i, i1) tl1) in + Ok (l, back)) + | Betree_List_Nil => Ok (Betree_List_Nil, Ok) + end + end +. + +(** [betree::betree::{betree::betree::Node#5}::apply_to_leaf]: + Source: 'src/betree.rs', lines 460:4-460:87 *) +Definition betree_Node_apply_to_leaf + (n : nat) (bindings : betree_List_t (u64 * u64)) (key : u64) + (new_msg : betree_Message_t) : + result (betree_List_t (u64 * u64)) + := + p <- betree_Node_lookup_mut_in_bindings n key bindings; + let (bindings1, lookup_mut_in_bindings_back) := p in + b <- betree_ListPairU64T_head_has_key u64 bindings1 key; + if b + then ( + p1 <- betree_List_pop_front (u64 * u64) bindings1; + let (hd, bindings2) := p1 in + match new_msg with + | Betree_Message_Insert v => + bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v); + lookup_mut_in_bindings_back bindings3 + | Betree_Message_Delete => lookup_mut_in_bindings_back bindings2 + | Betree_Message_Upsert s => + let (_, i) := hd in + v <- betree_upsert_update (Some i) s; + bindings3 <- betree_List_push_front (u64 * u64) bindings2 (key, v); + lookup_mut_in_bindings_back bindings3 + end) + else + match new_msg with + | Betree_Message_Insert v => + bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); + lookup_mut_in_bindings_back bindings2 + | Betree_Message_Delete => lookup_mut_in_bindings_back bindings1 + | Betree_Message_Upsert s => + v <- betree_upsert_update None s; + bindings2 <- betree_List_push_front (u64 * u64) bindings1 (key, v); + lookup_mut_in_bindings_back bindings2 + end +. + +(** [betree::betree::{betree::betree::Node#5}::apply_messages_to_leaf]: + Source: 'src/betree.rs', lines 444:4-447:5 *) +Fixpoint betree_Node_apply_messages_to_leaf + (n : nat) (bindings : betree_List_t (u64 * u64)) + (new_msgs : betree_List_t (u64 * betree_Message_t)) : + result (betree_List_t (u64 * u64)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match new_msgs with + | Betree_List_Cons new_msg new_msgs_tl => + let (i, m) := new_msg in + bindings1 <- betree_Node_apply_to_leaf n1 bindings i m; + betree_Node_apply_messages_to_leaf n1 bindings1 new_msgs_tl + | Betree_List_Nil => Ok bindings + end + end +. + +(** [betree::betree::{betree::betree::Internal#4}::flush]: + Source: 'src/betree.rs', lines 410:4-415:26 *) +Fixpoint betree_Internal_flush + (n : nat) (self : betree_Internal_t) (params : betree_Params_t) + (node_id_cnt : betree_NodeIdCounter_t) + (content : betree_List_t (u64 * betree_Message_t)) (st : state) : + result (state * ((betree_List_t (u64 * betree_Message_t)) * + (betree_Internal_t * betree_NodeIdCounter_t))) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + p <- + betree_ListPairU64T_partition_at_pivot betree_Message_t n1 content + self.(betree_Internal_pivot); + let (msgs_left, msgs_right) := p in + len_left <- betree_List_len (u64 * betree_Message_t) n1 msgs_left; + if len_left s>= params.(betree_Params_min_flush_size) + then ( + p1 <- + betree_Node_apply_messages n1 self.(betree_Internal_left) params + node_id_cnt msgs_left st; + let (st1, p2) := p1 in + let (n2, node_id_cnt1) := p2 in + len_right <- betree_List_len (u64 * betree_Message_t) n1 msgs_right; + if len_right s>= params.(betree_Params_min_flush_size) + then ( + p3 <- + betree_Node_apply_messages n1 self.(betree_Internal_right) params + node_id_cnt1 msgs_right st1; + let (st2, p4) := p3 in + let (n3, node_id_cnt2) := p4 in + Ok (st2, (Betree_List_Nil, (mkbetree_Internal_t + self.(betree_Internal_id) self.(betree_Internal_pivot) n2 n3, + node_id_cnt2)))) + else + Ok (st1, (msgs_right, (mkbetree_Internal_t self.(betree_Internal_id) + self.(betree_Internal_pivot) n2 self.(betree_Internal_right), + node_id_cnt1)))) + else ( + p1 <- + betree_Node_apply_messages n1 self.(betree_Internal_right) params + node_id_cnt msgs_right st; + let (st1, p2) := p1 in + let (n2, node_id_cnt1) := p2 in + Ok (st1, (msgs_left, (mkbetree_Internal_t self.(betree_Internal_id) + self.(betree_Internal_pivot) self.(betree_Internal_left) n2, + node_id_cnt1)))) + end + +(** [betree::betree::{betree::betree::Node#5}::apply_messages]: + Source: 'src/betree.rs', lines 588:4-593:5 *) +with betree_Node_apply_messages + (n : nat) (self : betree_Node_t) (params : betree_Params_t) + (node_id_cnt : betree_NodeIdCounter_t) + (msgs : betree_List_t (u64 * betree_Message_t)) (st : state) : + result (state * (betree_Node_t * betree_NodeIdCounter_t)) + := + match n with + | O => Fail_ OutOfFuel + | S n1 => + match self with + | Betree_Node_Internal node => + p <- betree_load_internal_node node.(betree_Internal_id) st; + let (st1, content) := p in + content1 <- betree_Node_apply_messages_to_internal n1 content msgs; + num_msgs <- betree_List_len (u64 * betree_Message_t) n1 content1; + if num_msgs s>= params.(betree_Params_min_flush_size) + then ( + p1 <- betree_Internal_flush n1 node params node_id_cnt content1 st1; + let (st2, p2) := p1 in + let (content2, p3) := p2 in + let (node1, node_id_cnt1) := p3 in + p4 <- + betree_store_internal_node node1.(betree_Internal_id) content2 st2; + let (st3, _) := p4 in + Ok (st3, (Betree_Node_Internal node1, node_id_cnt1))) + else ( + p1 <- + betree_store_internal_node node.(betree_Internal_id) content1 st1; + let (st2, _) := p1 in + Ok (st2, (Betree_Node_Internal node, node_id_cnt))) + | Betree_Node_Leaf node => + p <- betree_load_leaf_node node.(betree_Leaf_id) st; + let (st1, content) := p in + content1 <- betree_Node_apply_messages_to_leaf n1 content msgs; + len <- betree_List_len (u64 * u64) n1 content1; + i <- u64_mul 2%u64 params.(betree_Params_split_size); + if len s>= i + then ( + p1 <- betree_Leaf_split n1 node content1 params node_id_cnt st1; + let (st2, p2) := p1 in + let (new_node, node_id_cnt1) := p2 in + p3 <- betree_store_leaf_node node.(betree_Leaf_id) Betree_List_Nil st2; + let (st3, _) := p3 in + Ok (st3, (Betree_Node_Internal new_node, node_id_cnt1))) + else ( + p1 <- betree_store_leaf_node node.(betree_Leaf_id) content1 st1; + let (st2, _) := p1 in + Ok (st2, (Betree_Node_Leaf + {| betree_Leaf_id := node.(betree_Leaf_id); betree_Leaf_size := len + |}, node_id_cnt))) + end + end +. + +(** [betree::betree::{betree::betree::Node#5}::apply]: + Source: 'src/betree.rs', lines 576:4-582:5 *) +Definition betree_Node_apply + (n : nat) (self : betree_Node_t) (params : betree_Params_t) + (node_id_cnt : betree_NodeIdCounter_t) (key : u64) + (new_msg : betree_Message_t) (st : state) : + result (state * (betree_Node_t * betree_NodeIdCounter_t)) + := + p <- + betree_Node_apply_messages n self params node_id_cnt (Betree_List_Cons + (key, new_msg) Betree_List_Nil) st; + let (st1, p1) := p in + let (self1, node_id_cnt1) := p1 in + Ok (st1, (self1, node_id_cnt1)) +. + +(** [betree::betree::{betree::betree::BeTree#6}::new]: + Source: 'src/betree.rs', lines 849:4-849:60 *) +Definition betree_BeTree_new + (min_flush_size : u64) (split_size : u64) (st : state) : + result (state * betree_BeTree_t) + := + node_id_cnt <- betree_NodeIdCounter_new; + p <- betree_NodeIdCounter_fresh_id node_id_cnt; + let (id, node_id_cnt1) := p in + p1 <- betree_store_leaf_node id Betree_List_Nil st; + let (st1, _) := p1 in + Ok (st1, + {| + betree_BeTree_params := + {| + betree_Params_min_flush_size := min_flush_size; + betree_Params_split_size := split_size + |}; + betree_BeTree_node_id_cnt := node_id_cnt1; + betree_BeTree_root := + (Betree_Node_Leaf + {| betree_Leaf_id := id; betree_Leaf_size := 0%u64 |}) + |}) +. + +(** [betree::betree::{betree::betree::BeTree#6}::apply]: + Source: 'src/betree.rs', lines 868:4-868:47 *) +Definition betree_BeTree_apply + (n : nat) (self : betree_BeTree_t) (key : u64) (msg : betree_Message_t) + (st : state) : + result (state * betree_BeTree_t) + := + p <- + betree_Node_apply n self.(betree_BeTree_root) self.(betree_BeTree_params) + self.(betree_BeTree_node_id_cnt) key msg st; + let (st1, p1) := p in + let (n1, nic) := p1 in + Ok (st1, + {| + betree_BeTree_params := self.(betree_BeTree_params); + betree_BeTree_node_id_cnt := nic; + betree_BeTree_root := n1 + |}) +. + +(** [betree::betree::{betree::betree::BeTree#6}::insert]: + Source: 'src/betree.rs', lines 874:4-874:52 *) +Definition betree_BeTree_insert + (n : nat) (self : betree_BeTree_t) (key : u64) (value : u64) (st : state) : + result (state * betree_BeTree_t) + := + betree_BeTree_apply n self key (Betree_Message_Insert value) st +. + +(** [betree::betree::{betree::betree::BeTree#6}::delete]: + Source: 'src/betree.rs', lines 880:4-880:38 *) +Definition betree_BeTree_delete + (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : + result (state * betree_BeTree_t) + := + betree_BeTree_apply n self key Betree_Message_Delete st +. + +(** [betree::betree::{betree::betree::BeTree#6}::upsert]: + Source: 'src/betree.rs', lines 886:4-886:59 *) +Definition betree_BeTree_upsert + (n : nat) (self : betree_BeTree_t) (key : u64) + (upd : betree_UpsertFunState_t) (st : state) : + result (state * betree_BeTree_t) + := + betree_BeTree_apply n self key (Betree_Message_Upsert upd) st +. + +(** [betree::betree::{betree::betree::BeTree#6}::lookup]: + Source: 'src/betree.rs', lines 895:4-895:62 *) +Definition betree_BeTree_lookup + (n : nat) (self : betree_BeTree_t) (key : u64) (st : state) : + result (state * ((option u64) * betree_BeTree_t)) + := + p <- betree_Node_lookup n self.(betree_BeTree_root) key st; + let (st1, p1) := p in + let (o, n1) := p1 in + Ok (st1, (o, + {| + betree_BeTree_params := self.(betree_BeTree_params); + betree_BeTree_node_id_cnt := self.(betree_BeTree_node_id_cnt); + betree_BeTree_root := n1 + |})) +. + +(** [betree::main]: + Source: 'src/main.rs', lines 4:0-4:9 *) +Definition main : result unit := + Ok tt. + +(** Unit test for [betree::main] *) +Check (main )%return. + +End Betree_Funs. diff --git a/tests/coq/betree/Betree_FunsExternal.v b/tests/coq/betree/Betree_FunsExternal.v new file mode 100644 index 00000000..0263c272 --- /dev/null +++ b/tests/coq/betree/Betree_FunsExternal.v @@ -0,0 +1,39 @@ +(** [betree_main]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Export Betree_Types. +Import Betree_Types. +Module Betree_FunsExternal. + +(** [betree_main::betree_utils::load_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 98:0-98:63 *) +Axiom betree_utils_load_internal_node + : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t))) +. + +(** [betree_main::betree_utils::store_internal_node]: forward function + Source: 'src/betree_utils.rs', lines 115:0-115:71 *) +Axiom betree_utils_store_internal_node + : + u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state * + unit) +. + +(** [betree_main::betree_utils::load_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 132:0-132:55 *) +Axiom betree_utils_load_leaf_node + : u64 -> state -> result (state * (betree_List_t (u64 * u64))) +. + +(** [betree_main::betree_utils::store_leaf_node]: forward function + Source: 'src/betree_utils.rs', lines 145:0-145:63 *) +Axiom betree_utils_store_leaf_node + : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) +. + +End Betree_FunsExternal. diff --git a/tests/coq/betree/Betree_FunsExternal_Template.v b/tests/coq/betree/Betree_FunsExternal_Template.v new file mode 100644 index 00000000..2a2fddfc --- /dev/null +++ b/tests/coq/betree/Betree_FunsExternal_Template.v @@ -0,0 +1,40 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Import Betree_Types. +Include Betree_Types. +Module Betree_FunsExternal_Template. + +(** [betree::betree_utils::load_internal_node]: + Source: 'src/betree_utils.rs', lines 98:0-98:63 *) +Axiom betree_utils_load_internal_node + : u64 -> state -> result (state * (betree_List_t (u64 * betree_Message_t))) +. + +(** [betree::betree_utils::store_internal_node]: + Source: 'src/betree_utils.rs', lines 115:0-115:71 *) +Axiom betree_utils_store_internal_node + : + u64 -> betree_List_t (u64 * betree_Message_t) -> state -> result (state * + unit) +. + +(** [betree::betree_utils::load_leaf_node]: + Source: 'src/betree_utils.rs', lines 132:0-132:55 *) +Axiom betree_utils_load_leaf_node + : u64 -> state -> result (state * (betree_List_t (u64 * u64))) +. + +(** [betree::betree_utils::store_leaf_node]: + Source: 'src/betree_utils.rs', lines 145:0-145:63 *) +Axiom betree_utils_store_leaf_node + : u64 -> betree_List_t (u64 * u64) -> state -> result (state * unit) +. + +End Betree_FunsExternal_Template. diff --git a/tests/coq/betree/Betree_Types.v b/tests/coq/betree/Betree_Types.v new file mode 100644 index 00000000..aa39d8e4 --- /dev/null +++ b/tests/coq/betree/Betree_Types.v @@ -0,0 +1,118 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree]: type definitions *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Import Betree_TypesExternal. +Include Betree_TypesExternal. +Module Betree_Types. + +(** [betree::betree::List] + Source: 'src/betree.rs', lines 17:0-17:23 *) +Inductive betree_List_t (T : Type) := +| Betree_List_Cons : T -> betree_List_t T -> betree_List_t T +| Betree_List_Nil : betree_List_t T +. + +Arguments Betree_List_Cons { _ }. +Arguments Betree_List_Nil { _ }. + +(** [betree::betree::UpsertFunState] + Source: 'src/betree.rs', lines 63:0-63:23 *) +Inductive betree_UpsertFunState_t := +| Betree_UpsertFunState_Add : u64 -> betree_UpsertFunState_t +| Betree_UpsertFunState_Sub : u64 -> betree_UpsertFunState_t +. + +(** [betree::betree::Message] + Source: 'src/betree.rs', lines 69:0-69:23 *) +Inductive betree_Message_t := +| Betree_Message_Insert : u64 -> betree_Message_t +| Betree_Message_Delete : betree_Message_t +| Betree_Message_Upsert : betree_UpsertFunState_t -> betree_Message_t +. + +(** [betree::betree::Leaf] + Source: 'src/betree.rs', lines 167:0-167:11 *) +Record betree_Leaf_t := +mkbetree_Leaf_t { + betree_Leaf_id : u64; betree_Leaf_size : u64; +} +. + +(** [betree::betree::Internal] + Source: 'src/betree.rs', lines 156:0-156:15 *) +Inductive betree_Internal_t := +| mkbetree_Internal_t : + u64 -> + u64 -> + betree_Node_t -> + betree_Node_t -> + betree_Internal_t + +(** [betree::betree::Node] + Source: 'src/betree.rs', lines 179:0-179:9 *) +with betree_Node_t := +| Betree_Node_Internal : betree_Internal_t -> betree_Node_t +| Betree_Node_Leaf : betree_Leaf_t -> betree_Node_t +. + +Definition betree_Internal_id (x : betree_Internal_t) := + match x with | mkbetree_Internal_t x1 _ _ _ => x1 end +. + +Notation "x2 .(betree_Internal_id)" := (betree_Internal_id x2) (at level 9). + +Definition betree_Internal_pivot (x : betree_Internal_t) := + match x with | mkbetree_Internal_t _ x1 _ _ => x1 end +. + +Notation "x2 .(betree_Internal_pivot)" := (betree_Internal_pivot x2) + (at level 9) +. + +Definition betree_Internal_left (x : betree_Internal_t) := + match x with | mkbetree_Internal_t _ _ x1 _ => x1 end +. + +Notation "x2 .(betree_Internal_left)" := (betree_Internal_left x2) (at level 9) +. + +Definition betree_Internal_right (x : betree_Internal_t) := + match x with | mkbetree_Internal_t _ _ _ x1 => x1 end +. + +Notation "x2 .(betree_Internal_right)" := (betree_Internal_right x2) + (at level 9) +. + +(** [betree::betree::Params] + Source: 'src/betree.rs', lines 187:0-187:13 *) +Record betree_Params_t := +mkbetree_Params_t { + betree_Params_min_flush_size : u64; betree_Params_split_size : u64; +} +. + +(** [betree::betree::NodeIdCounter] + Source: 'src/betree.rs', lines 201:0-201:20 *) +Record betree_NodeIdCounter_t := +mkbetree_NodeIdCounter_t { + betree_NodeIdCounter_next_node_id : u64; +} +. + +(** [betree::betree::BeTree] + Source: 'src/betree.rs', lines 218:0-218:17 *) +Record betree_BeTree_t := +mkbetree_BeTree_t { + betree_BeTree_params : betree_Params_t; + betree_BeTree_node_id_cnt : betree_NodeIdCounter_t; + betree_BeTree_root : betree_Node_t; +} +. + +End Betree_Types. diff --git a/tests/coq/betree/Betree_TypesExternal.v b/tests/coq/betree/Betree_TypesExternal.v new file mode 100644 index 00000000..37487d6d --- /dev/null +++ b/tests/coq/betree/Betree_TypesExternal.v @@ -0,0 +1,14 @@ +(** [betree_main]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module Betree_TypesExternal. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End Betree_TypesExternal. diff --git a/tests/coq/betree/Betree_TypesExternal_Template.v b/tests/coq/betree/Betree_TypesExternal_Template.v new file mode 100644 index 00000000..a40811cb --- /dev/null +++ b/tests/coq/betree/Betree_TypesExternal_Template.v @@ -0,0 +1,15 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree]: external types. +-- This is a template file: rename it to "TypesExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module Betree_TypesExternal_Template. + +(** The state type used in the state-error monad *) +Axiom state : Type. + +End Betree_TypesExternal_Template. diff --git a/tests/coq/betree/_CoqProject b/tests/coq/betree/_CoqProject index b14bed66..9fb7fe64 100644 --- a/tests/coq/betree/_CoqProject +++ b/tests/coq/betree/_CoqProject @@ -3,10 +3,10 @@ -arg -w -arg all -BetreeMain_TypesExternal_Template.v -BetreeMain_Types.v +Betree_TypesExternal_Template.v +Betree_Types.v Primitives.v -BetreeMain_FunsExternal_Template.v -BetreeMain_Funs.v -BetreeMain_TypesExternal.v -BetreeMain_FunsExternal.v +Betree_FunsExternal_Template.v +Betree_Funs.v +Betree_TypesExternal.v +Betree_FunsExternal.v -- cgit v1.2.3 From c81c96f20b1dbf428a9ed42e83b910e798e1a225 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 May 2024 17:33:56 +0200 Subject: Add some tests --- tests/coq/misc/Issue194RecursiveStructProjector.v | 54 +++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 tests/coq/misc/Issue194RecursiveStructProjector.v (limited to 'tests/coq') diff --git a/tests/coq/misc/Issue194RecursiveStructProjector.v b/tests/coq/misc/Issue194RecursiveStructProjector.v new file mode 100644 index 00000000..d1a07449 --- /dev/null +++ b/tests/coq/misc/Issue194RecursiveStructProjector.v @@ -0,0 +1,54 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [issue_194_recursive_struct_projector] *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module Issue194RecursiveStructProjector. + +(** [issue_194_recursive_struct_projector::AVLNode] + Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 2:0-2:17 *) +Inductive AVLNode_t (T : Type) := +| mkAVLNode_t : + T -> + option (AVLNode_t T) -> + option (AVLNode_t T) -> + AVLNode_t T +. + +Arguments mkAVLNode_t { _ }. + +Definition aVLNode_value {T : Type} (x : AVLNode_t T) := + match x with | mkAVLNode_t x1 _ _ => x1 end +. + +Notation "x2 .(aVLNode_value)" := (aVLNode_value x2) (at level 9). + +Definition aVLNode_left {T : Type} (x : AVLNode_t T) := + match x with | mkAVLNode_t _ x1 _ => x1 end +. + +Notation "x2 .(aVLNode_left)" := (aVLNode_left x2) (at level 9). + +Definition aVLNode_right {T : Type} (x : AVLNode_t T) := + match x with | mkAVLNode_t _ _ x1 => x1 end +. + +Notation "x2 .(aVLNode_right)" := (aVLNode_right x2) (at level 9). + +(** [issue_194_recursive_struct_projector::get_val]: + Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 10:0-10:33 *) +Definition get_val (T : Type) (x : AVLNode_t T) : result T := + Ok x.(aVLNode_value) +. + +(** [issue_194_recursive_struct_projector::get_left]: + Source: 'tests/src/issue-194-recursive-struct-projector.rs', lines 14:0-14:43 *) +Definition get_left + (T : Type) (x : AVLNode_t T) : result (option (AVLNode_t T)) := + Ok x.(aVLNode_left) +. + +End Issue194RecursiveStructProjector. -- cgit v1.2.3 From c4d2af051c18c4c81b1e57a45210c37c89c8330f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 May 2024 11:18:35 +0200 Subject: tests: Rename hashmap_utils -> utils --- tests/coq/hashmap/Hashmap_Funs.v | 4 ++-- tests/coq/hashmap/Hashmap_FunsExternal.v | 8 ++++---- tests/coq/hashmap/Hashmap_FunsExternal_Template.v | 9 ++++----- 3 files changed, 10 insertions(+), 11 deletions(-) (limited to 'tests/coq') diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v index 89f90210..04df873a 100644 --- a/tests/coq/hashmap/Hashmap_Funs.v +++ b/tests/coq/hashmap/Hashmap_Funs.v @@ -508,10 +508,10 @@ Definition hashMap_remove Source: 'tests/src/hashmap.rs', lines 335:0-335:43 *) Definition insert_on_disk (n : nat) (key : usize) (value : u64) (st : state) : result (state * unit) := - p <- hashmap_utils_deserialize st; + p <- utils_deserialize st; let (st1, hm) := p in hm1 <- hashMap_insert u64 n hm key value; - hashmap_utils_serialize hm1 st1 + utils_serialize hm1 st1 . (** [hashmap::test1]: diff --git a/tests/coq/hashmap/Hashmap_FunsExternal.v b/tests/coq/hashmap/Hashmap_FunsExternal.v index bcf12c17..3bc6c98a 100644 --- a/tests/coq/hashmap/Hashmap_FunsExternal.v +++ b/tests/coq/hashmap/Hashmap_FunsExternal.v @@ -9,13 +9,13 @@ Require Export Hashmap_Types. Import Hashmap_Types. Module Hashmap_FunsExternal. -(** [hashmap::hashmap_utils::deserialize]: +(** [hashmap::utils::deserialize]: Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *) -Axiom hashmap_utils_deserialize : state -> result (state * (HashMap_t u64)). +Axiom utils_deserialize : state -> result (state * (HashMap_t u64)). -(** [hashmap::hashmap_utils::serialize]: +(** [hashmap::utils::serialize]: Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *) -Axiom hashmap_utils_serialize : HashMap_t u64 -> state -> result (state * unit) +Axiom utils_serialize : HashMap_t u64 -> state -> result (state * unit) . End Hashmap_FunsExternal. diff --git a/tests/coq/hashmap/Hashmap_FunsExternal_Template.v b/tests/coq/hashmap/Hashmap_FunsExternal_Template.v index c35b8e14..c58b021d 100644 --- a/tests/coq/hashmap/Hashmap_FunsExternal_Template.v +++ b/tests/coq/hashmap/Hashmap_FunsExternal_Template.v @@ -11,13 +11,12 @@ Require Import Hashmap_Types. Include Hashmap_Types. Module Hashmap_FunsExternal_Template. -(** [hashmap::hashmap_utils::deserialize]: +(** [hashmap::utils::deserialize]: Source: 'tests/src/hashmap.rs', lines 330:4-330:47 *) -Axiom hashmap_utils_deserialize : state -> result (state * (HashMap_t u64)). +Axiom utils_deserialize : state -> result (state * (HashMap_t u64)). -(** [hashmap::hashmap_utils::serialize]: +(** [hashmap::utils::serialize]: Source: 'tests/src/hashmap.rs', lines 325:4-325:46 *) -Axiom hashmap_utils_serialize : HashMap_t u64 -> state -> result (state * unit) -. +Axiom utils_serialize : HashMap_t u64 -> state -> result (state * unit). End Hashmap_FunsExternal_Template. -- cgit v1.2.3