From b7baf31b09e13557a7f10ffb95d8a7ba6ed97c02 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Fri, 11 Oct 2024 10:53:27 -0500 Subject: [PATCH 1/6] Checkpoint changing string literals to list w8 --- new/golang/defn/typing.v | 10 ++++----- src/Helpers/ByteString.v | 20 +++++++++++------ src/goose_lang/ffi/grove_ffi/impl.v | 4 ++-- src/goose_lang/interpreter/pretty_types.v | 5 +++-- src/goose_lang/lang.v | 27 ++++++++++++----------- src/goose_lang/notation.v | 1 + 6 files changed, 38 insertions(+), 29 deletions(-) diff --git a/new/golang/defn/typing.v b/new/golang/defn/typing.v index e1568990c..5626c71cc 100644 --- a/new/golang/defn/typing.v +++ b/new/golang/defn/typing.v @@ -33,7 +33,7 @@ Section val_types. | stringT | arrayT (n : nat) (elem : go_type) | sliceT (elem : go_type) - | structT (decls : list (string * go_type)) (* What if this were a gmap? *) + | structT (decls : list (byte_string * go_type)) (* What if this were a gmap? *) | ptrT (* Untyped pointer; convenient to support recursion in structs *) | funcT | interfaceT @@ -102,19 +102,19 @@ Reserved Notation "l +ₗ[ t ] z" (at level 50, left associativity, format "l + Notation "l +ₗ[ t ] z" := (l +ₗ go_type_size t * z) : stdpp_scope . Notation "e1 +ₗ[ t ] e2" := (BinOp (OffsetOp (go_type_size t)) e1%E e2%E) : expr_scope . -Fixpoint assocl_lookup {A} (f : string) (field_vals: list (string * A)) : option A := +Fixpoint assocl_lookup {A} (f : byte_string) (field_vals: list (byte_string * A)) : option A := match field_vals with | [] => None - | (f', v)::fs => if String.eqb f' f then Some v else assocl_lookup f fs + | (f', v)::fs => if ByteString.eqb f' f then Some v else assocl_lookup f fs end. Module struct. - Definition descriptor := list (string * go_type). + Definition descriptor := list (byte_string * go_type). Section goose_lang. Context `{ffi_syntax}. - Definition fields_val_def (m : list (string* val)) : val := + Definition fields_val_def (m : list (byte_string* val)) : val := list.val (fmap (λ '(a,b), (#(str a), b)%V) m). Program Definition fields_val := unseal (_:seal (@fields_val_def)). Obligation 1. by eexists. Qed. Definition fields_val_unseal : fields_val = _ := seal_eq _. diff --git a/src/Helpers/ByteString.v b/src/Helpers/ByteString.v index d84c7a917..09eb781ed 100644 --- a/src/Helpers/ByteString.v +++ b/src/Helpers/ByteString.v @@ -1,4 +1,4 @@ -From stdpp Require Import base. +From stdpp Require Import base decidable. From Perennial.Helpers Require Import Integers bytes. From Coq Require Import ZArith Strings.Byte. @@ -25,25 +25,31 @@ Definition w8_to_byte (w: w8) : byte := Notation byte_string := (@list w8) (only parsing). -Definition parse_string (s: list Byte.byte) : byte_string := +#[local] Definition parse_string (s: list Byte.byte) : byte_string := byte_to_w8 <$> s. -Definition print_string (b: byte_string) : list Byte.byte := +#[local] Definition print_string (b: byte_string) : list Byte.byte := w8_to_byte <$> b. -String Notation byte_string parse_string print_string : string_scope. +Declare Scope byte_string_scope. +Bind Scope byte_string_scope with byte_string. +String Notation byte_string parse_string print_string : byte_string_scope. + +(* TODO: replace with more computationally efficient version *) +#[local] Definition eqb (s1 s2: byte_string) : bool := + bool_decide (s1 = s2). (* These theorems are not actually required, but they are a sanity check that the code above is implemented correctly. *) -Lemma byte_to_w8_to_byte b : +#[local] Lemma byte_to_w8_to_byte b : w8_to_byte (byte_to_w8 b) = b. Proof. destruct b; auto. Qed. -Lemma w8_to_byte_to_w8 w : +#[local] Lemma w8_to_byte_to_w8 w : byte_to_w8 (w8_to_byte w) = w. Proof. byte_cases w; reflexivity. Qed. -Lemma parse_print_inverse s : +#[local] Lemma parse_print_inverse s : print_string (parse_string s) = s. Proof. rewrite /print_string /parse_string. diff --git a/src/goose_lang/ffi/grove_ffi/impl.v b/src/goose_lang/ffi/grove_ffi/impl.v index 20aa4a9a1..581fec788 100644 --- a/src/goose_lang/ffi/grove_ffi/impl.v +++ b/src/goose_lang/ffi/grove_ffi/impl.v @@ -3,7 +3,7 @@ From stdpp Require Import gmap vector fin_maps. From RecordUpdate Require Import RecordSet. -From Perennial.Helpers Require Import CountableTactics Transitions Integers. +From Perennial.Helpers Require Import CountableTactics Transitions Integers ByteString. From Perennial.goose_lang Require Import lang notation lib.control.impl. Set Default Proof Using "Type". @@ -95,7 +95,7 @@ Global Instance grove_global_state_inhabited : Inhabited grove_global_state := (** The per-node state *) Record grove_node_state : Type := { grove_node_tsc : u64; - grove_node_files: gmap string (list byte); + grove_node_files: gmap byte_string (list byte); }. Global Instance grove_node_state_settable : Settable _ := diff --git a/src/goose_lang/interpreter/pretty_types.v b/src/goose_lang/interpreter/pretty_types.v index f84ce9a3b..814ddcba9 100644 --- a/src/goose_lang/interpreter/pretty_types.v +++ b/src/goose_lang/interpreter/pretty_types.v @@ -1,7 +1,7 @@ From stdpp Require Import strings. From stdpp Require Export pretty. From Perennial.program_logic Require Import language ectx_language ectxi_language. -From Perennial.Helpers Require Import Integers Transitions. +From Perennial.Helpers Require Import Integers Transitions ByteString. From Perennial.goose_lang Require Import locations lang. Set Default Proof Using "Type". @@ -18,7 +18,8 @@ Instance pretty_u32 : Pretty Integers.u32 := Instance pretty_loc : Pretty loc := fun x => pretty x.(loc_car). -Definition quoted (s:string) : string := ("""" ++ s ++ """")%string. +Definition quoted (s:byte_string) : string := + ("""" ++ String.string_of_list_byte (ByteString.print_string s) ++ """")%string. #[global] Instance pretty_lit : Pretty base_lit := diff --git a/src/goose_lang/lang.v b/src/goose_lang/lang.v index b85a4a101..381cce608 100644 --- a/src/goose_lang/lang.v +++ b/src/goose_lang/lang.v @@ -1,14 +1,16 @@ From Coq.Program Require Import Equality. From RecordUpdate Require Import RecordSet. -From stdpp Require Export binders strings. +From stdpp Require Export binders. From stdpp Require Import gmap. From iris.algebra Require Export ofe. From Perennial.program_logic Require Export language ectx_language ectxi_language. From Perennial.Helpers Require Import CountableTactics. From Perennial.Helpers Require Import Transitions. +From Perennial.Helpers Require Import ByteString. From Perennial.program_logic Require Export crash_lang. From Perennial.goose_lang Require Export locations. From Perennial Require Export Helpers.Integers. + Set Default Proof Using "Type". Open Scope Z_scope. @@ -64,10 +66,9 @@ behavior. So we erase to the poison value instead, making sure that no legal comparisons could be affected. *) Inductive base_lit : Type := | LitInt (n : u64) | LitInt32 (n : u32) | LitBool (b : bool) | LitByte (n : u8) - | LitString (s : string) | LitUnit | LitPoison + | LitString (s : byte_string) | LitUnit | LitPoison | LitLoc (l : loc) | LitProphecy (p: proph_id). Inductive un_op : Set := - (* TODO: operation to take length of string *) | NegOp | MinusUnOp | UToW64Op | UToW32Op | UToW8Op | SToW64Op | SToW32Op | SToW8Op @@ -82,7 +83,7 @@ Inductive bin_op : Set := | StringGetOp . -Inductive prim_op0 : Set := +Inductive prim_op0 : Type := (* a stuck expression, to represent undefined behavior *) | PanicOp (s: string) (* non-deterministically pick an integer *) @@ -107,7 +108,7 @@ Inductive prim_op2 : Set := . Inductive arity : Set := args0 | args1 | args2. -Definition prim_op (ar:arity) : Set := +Definition prim_op (ar:arity) : Type := match ar with | args0 => prim_op0 | args1 => prim_op1 @@ -539,7 +540,7 @@ Proof. solve_countable prim_op1_rec 7%nat. Qed. Instance prim_op2_countable : Countable prim_op2. Proof. solve_countable prim_op2_rec 4%nat. Qed. -Definition prim_op' : Set := prim_op0 + prim_op1 + prim_op2. +Definition prim_op' : Type := prim_op0 + prim_op1 + prim_op2. Definition a_prim_op {ar} (op: prim_op ar) : prim_op'. rewrite /prim_op'. @@ -774,7 +775,7 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr := end. (** Substitution *) -Fixpoint subst (x : string) (v : val) (e : expr) : expr := +Fixpoint subst (x : String.string) (v : val) (e : expr) : expr := match e with | Val _ => e | Var y => if decide (x = y) then Val v else Var y @@ -831,9 +832,9 @@ Definition un_op_eval (op : un_op) (v : val) : option val := | SToW8Op, LitV (LitInt v) => Some $ LitV $ LitByte (W8 (sint.Z v)) | SToW8Op, LitV (LitInt32 v) => Some $ LitV $ LitByte (W8 (sint.Z v)) | SToW8Op, LitV (LitByte v) => Some $ LitV $ LitByte (W8 (sint.Z v)) - | ToStringOp, LitV (LitByte v) => Some $ LitV $ LitString (u8_to_string v) - | StringLenOp, LitV (LitString v) => Some $ LitV $ LitInt (W64 (String.length v)) - | IsNoStringOverflowOp, LitV (LitString v) => Some $ LitV $ LitBool (bool_decide ((String.length v) < 2^64)) + | ToStringOp, LitV (LitByte v) => Some $ LitV $ LitString [v] + | StringLenOp, LitV (LitString v) => Some $ LitV $ LitInt (W64 (Z.of_nat (length v))) + | IsNoStringOverflowOp, LitV (LitString v) => Some $ LitV $ LitBool (bool_decide (Z.of_nat (length v) < 2^64)) | _, _ => None end. @@ -878,7 +879,7 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit := | _ => None end. -Definition bin_op_eval_string (op : bin_op) (s1 s2 : string) : option base_lit := +Definition bin_op_eval_string (op : bin_op) (s1 s2 : byte_string) : option base_lit := match op with | PlusOp => Some $ LitString (s1 ++ s2) | _ => None @@ -887,11 +888,11 @@ Definition bin_op_eval_string (op : bin_op) (s1 s2 : string) : option base_lit : Definition string_to_bytes (s:string): list u8 := (λ x, W8 $ Ascii.nat_of_ascii x) <$> String.list_ascii_of_string s. -Definition bin_op_eval_string_word (op : bin_op) (s1 : string) {width} {word: Interface.word width} (w2 : word): option base_lit := +Definition bin_op_eval_string_word (op : bin_op) (s1 : byte_string) {width} {word: Interface.word width} (w2 : word): option base_lit := match op with | StringGetOp => mbind (M:=option) (λ (x:u8), Some $ LitByte x) - ((string_to_bytes s1) !! (uint.nat w2)) + (s1 !! (uint.nat w2)) | _ => None end. diff --git a/src/goose_lang/notation.v b/src/goose_lang/notation.v index c3453a694..c1f6ba57d 100644 --- a/src/goose_lang/notation.v +++ b/src/goose_lang/notation.v @@ -1,5 +1,6 @@ From Perennial.program_logic Require Import language. From Perennial.goose_lang Require Export lang. +From Perennial.Helpers Require Export ByteString. Set Default Proof Using "Type". Delimit Scope expr_scope with E. From e05dfe0927fad7ca81495ca9b8274f7f66492c14 Mon Sep 17 00:00:00 2001 From: Tej Chajed Date: Fri, 11 Oct 2024 12:08:46 -0500 Subject: [PATCH 2/6] Get proof_prelude to compile --- src/goose_lang/lib/into_val.v | 10 +++++----- src/goose_lang/lib/string/string.v | 16 +++++++--------- 2 files changed, 12 insertions(+), 14 deletions(-) diff --git a/src/goose_lang/lib/into_val.v b/src/goose_lang/lib/into_val.v index f993a88ee..05a131f2d 100644 --- a/src/goose_lang/lib/into_val.v +++ b/src/goose_lang/lib/into_val.v @@ -228,15 +228,15 @@ Section instances. by injection H. Qed. - Global Instance string_IntoVal : IntoVal string. + Global Instance byte_string_IntoVal : IntoVal byte_string. Proof. - refine {| into_val.to_val := λ (x: string), #(str x); + refine {| into_val.to_val := λ (x: byte_string), #(str x); from_val := λ v, match v with #(LitString x) => Some x | _ => None end; - IntoVal_def := ""; |}; done. + IntoVal_def := []; |}; done. Defined. - Global Instance string_IntoVal_boolT : IntoValForType string stringT. + Global Instance byte_string_IntoVal_boolT : IntoValForType byte_string stringT. Proof. constructor; auto. Qed. - Global Instance string_IntoValComparable : IntoValComparable string. + Global Instance byte_string_IntoValComparable : IntoValComparable byte_string. Proof. constructor; try done. intros. simpl in *. diff --git a/src/goose_lang/lib/string/string.v b/src/goose_lang/lib/string/string.v index 61c5ca089..29d08376f 100644 --- a/src/goose_lang/lib/string/string.v +++ b/src/goose_lang/lib/string/string.v @@ -115,14 +115,14 @@ Proof. rewrite bytes_to_string_to_bytes //. Qed. -Lemma wp_stringToBytes (i:u64) (s:string) : +Lemma wp_stringToBytes (i:u64) (s:byte_string) : {{{ - ⌜uint.nat i <= String.length s⌝ + ⌜uint.nat i <= length s⌝ }}} stringToBytes #i #(str s) {{{ (sl:Slice.t), RET (slice_val sl); own_slice sl byteT (DfracOwn 1) - (take (uint.nat i) (string_to_bytes s)) + (take (uint.nat i) s) }}} . Proof. @@ -140,11 +140,10 @@ Proof. wp_pures. destruct (decide (i = 0)). { subst. by exfalso. } - assert (uint.nat (word.sub i 1%Z) < String.length s)%nat as Hlookup. + assert (uint.nat (word.sub i 1%Z) < length s)%nat as Hlookup. { enough (uint.nat i ≠ 0%nat) by word. intros ?. apply n. word. } pose proof Hlookup as Hineq2. - rewrite string_bytes_length in Hlookup. apply List.list_lookup_lt in Hlookup as [? Hlookup]. wp_pure. { by rewrite /bin_op_eval /= Hlookup. } @@ -165,13 +164,13 @@ Proof. iFrame. Qed. -Lemma wp_StringToBytes (s:string) : +Lemma wp_StringToBytes (s:byte_string) : {{{ True }}} StringToBytes #(str s) {{{ - (sl:Slice.t), RET (slice_val sl); own_slice sl byteT (DfracOwn 1) (string_to_bytes s) + (sl:Slice.t), RET (slice_val sl); own_slice sl byteT (DfracOwn 1) s }}} . Proof. @@ -185,7 +184,6 @@ Proof. iDestruct (own_slice_sz with "[$]") as %Hsz. rewrite take_ge. { iFrame. } - rewrite -string_bytes_length. word. Qed. @@ -195,7 +193,7 @@ Lemma wp_StringFromBytes sl q (l:list u8) : }}} StringFromBytes (slice_val sl) {{{ - RET #(str bytes_to_string l); own_slice_small sl byteT q l + RET #(str l); own_slice_small sl byteT q l }}} . Proof. From ced6aed7670fa335e28890ef3539f022d2bd1717 Mon Sep 17 00:00:00 2001 From: Upamanyu Sharma Date: Thu, 19 Dec 2024 00:05:20 -0500 Subject: [PATCH 3/6] Remove `Hint Immediate` for `finite_countable` --- src/Helpers/CountableTactics.v | 5 ++++- src/goose_lang/ffi/grove_ffi/adequacy.v | 10 ++++------ src/program_proof/kv/interface.v | 4 ---- src/program_proof/rsm/distx/base.v | 4 ++-- 4 files changed, 10 insertions(+), 13 deletions(-) diff --git a/src/Helpers/CountableTactics.v b/src/Helpers/CountableTactics.v index 4ed10bf08..c2b0db131 100644 --- a/src/Helpers/CountableTactics.v +++ b/src/Helpers/CountableTactics.v @@ -1,4 +1,7 @@ -From stdpp Require Import countable. +From stdpp Require Import countable finite. + +(* FIXME: https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/424 *) +Global Remove Hints finite_countable : typeclass_instances. Local Ltac count t_rec := let rec go num f := diff --git a/src/goose_lang/ffi/grove_ffi/adequacy.v b/src/goose_lang/ffi/grove_ffi/adequacy.v index b4630ea6f..3dcecd1b7 100644 --- a/src/goose_lang/ffi/grove_ffi/adequacy.v +++ b/src/goose_lang/ffi/grove_ffi/adequacy.v @@ -47,14 +47,12 @@ Theorem grove_ffi_dist_adequacy_failstop Σ `{hPre: !gooseGpreS Σ} (∀ HG : gooseGlobalGS Σ, ⊢@{iPropI Σ} ([∗ map] e↦ms ∈ g.(global_world).(grove_net), e c↦ ms) ={⊤}=∗ - (([∗ list] ρ ∈ ebσs, - (* FIXME: the following doesn't work because of https://github.com/coq/coq/issues/16893 *) - (* (([∗ list] '(e, σ) ∈ ebσs, *) + (([∗ list] '(e, σ) ∈ ebσs, (* We reason about node running e with an arbitrary generation *) ∀ HL : gooseLocalGS Σ, - ([∗ map] f ↦ c ∈ ρ.2.(world).(grove_node_files), f f↦ c) -∗ - own_globals (DfracOwn 1) ρ.2.(globals) - ={⊤}=∗ ∃ Φ, wp NotStuck ⊤ ρ.1 Φ + ([∗ map] f ↦ c ∈ σ.(world).(grove_node_files), f f↦ c) -∗ + own_globals (DfracOwn 1) σ.(globals) + ={⊤}=∗ ∃ Φ, wp NotStuck ⊤ e Φ ) ∗ (∀ g', ffi_global_ctx goose_ffiGlobalGS g'.(global_world) ={⊤,∅}=∗ ⌜ φinv g' ⌝) )) → dist_adequate_failstop (ffi_sem:=grove_semantics) ebσs g (λ g, φinv g). diff --git a/src/program_proof/kv/interface.v b/src/program_proof/kv/interface.v index ca1bd0f2d..3b530fc6b 100644 --- a/src/program_proof/kv/interface.v +++ b/src/program_proof/kv/interface.v @@ -80,7 +80,3 @@ Definition is_Kv_Get_hocap2 P E (Get_fn:val) : iProp Σ := . End hocap_definitions. - -Check "a"%go. -(* [{| Naive.unsigned := 97; Naive._unsigned_in_range := eq_refl |}] - : list Naive.rep *) diff --git a/src/program_proof/rsm/distx/base.v b/src/program_proof/rsm/distx/base.v index fc49b68cf..3da3f90e7 100644 --- a/src/program_proof/rsm/distx/base.v +++ b/src/program_proof/rsm/distx/base.v @@ -73,7 +73,7 @@ Instance fstring_finite : Admitted. (* Definition keys_all : gset string := fin_to_set fstring. *) -Definition keys_all : gset string. +Definition keys_all : gset byte_string. Admitted. (** Transaction status on group/replica. *) @@ -129,7 +129,7 @@ Definition ptgroups (keys : gset dbkey) : gset groupid := Definition wrs_group gid (wrs : dbmap) := filter (λ t, key_to_group t.1 = gid) wrs. -Definition tpls_group gid (tpls : gmap dbkey dbtpl (H:=list_countable)) := +Definition tpls_group gid (tpls : gmap dbkey dbtpl) := filter (λ t, key_to_group t.1 = gid) tpls. Definition keys_group gid (keys : gset dbkey) := From 1e7e75adf3c4b6a4b7a69d3e8cd5413a3e6b1acc Mon Sep 17 00:00:00 2001 From: Upamanyu Sharma Date: Thu, 19 Dec 2024 18:10:54 -0500 Subject: [PATCH 4/6] Checkpoint migration to byte_string --- src/program_proof/append_log_refinement.v | 2 +- src/program_proof/bank/bank_proof.v | 63 ++++++----- src/program_proof/cachekv/proof.v | 25 ++--- src/program_proof/ctrexample/server.v | 2 +- src/program_proof/lockservice/aof_proof.v | 2 +- src/program_proof/lockservice/grove_ffi.v | 8 +- src/program_proof/lockservice/kv_proof.v | 8 +- src/program_proof/lockservice/rpc_proof.v | 12 +- src/program_proof/mvcc/mvcc_prelude.v | 4 +- src/program_proof/mvcc/strnum.v | 4 +- src/program_proof/mvcc/tuple_append_version.v | 4 +- src/program_proof/mvcc/tuple_kill_version.v | 2 +- src/program_proof/mvcc/tuple_mk.v | 2 +- src/program_proof/mvcc/tuple_prelude.v | 6 +- src/program_proof/mvcc/tuple_read_version.v | 8 +- .../mvcc/tuple_remove_versions.v | 2 +- src/program_proof/mvcc/txn_read.v | 4 +- src/program_proof/mvcc/wrbuf_prelude.v | 8 +- src/program_proof/mvcc/wrbuf_proof.v | 8 +- src/program_proof/pav/serde.v | 4 +- src/program_proof/rsm/distx/program/index.v | 2 +- src/program_proof/rsm/distx/program/replica.v | 4 +- .../rsm/distx/program/replica_group.v | 2 +- src/program_proof/rsm/distx/program/tuple.v | 16 +-- src/program_proof/rsm/distx/program/txn.v | 8 +- src/program_proof/rsm/distx/program/txnlog.v | 2 +- src/program_proof/rsm/fpaxos_inv.v | 6 +- src/program_proof/rsm/fpaxos_top.v | 12 +- src/program_proof/rsm/spaxos_examples.v | 4 +- src/program_proof/rsm/spaxos_ghost.v | 8 +- src/program_proof/rsm/spaxos_inv.v | 2 +- src/program_proof/rsm/spaxos_propose.v | 46 ++++---- src/program_proof/rsm/spaxos_top.v | 6 +- src/program_proof/tulip/base.v | 17 +-- src/program_proof/tulip/encode.v | 72 +----------- src/program_proof/tulip/inv.v | 2 +- src/program_proof/tulip/inv_txnlog.v | 6 +- src/program_proof/tulip/msg.v | 16 +-- src/program_proof/tulip/paxos/base.v | 16 +-- src/program_proof/tulip/paxos/inv.v | 14 +-- src/program_proof/tulip/paxos/msg.v | 16 +-- .../paxos/program/encode_accept_request.v | 2 +- .../paxos/program/encode_prepare_response.v | 2 +- .../tulip/paxos/program/mk_paxos.v | 2 +- .../tulip/paxos/program/paxos_accept.v | 4 +- .../tulip/paxos/program/paxos_collect.v | 4 +- .../tulip/paxos/program/paxos_commit.v | 2 +- .../tulip/paxos/program/paxos_forward.v | 2 +- .../tulip/paxos/program/paxos_getlsnc.v | 2 +- .../tulip/paxos/program/paxos_learn.v | 2 +- .../tulip/paxos/program/paxos_log.v | 12 +- .../tulip/paxos/program/paxos_lookup.v | 2 +- .../tulip/paxos/program/paxos_obtain.v | 2 +- .../tulip/paxos/program/paxos_prepare.v | 2 +- .../tulip/paxos/program/paxos_submit.v | 2 +- src/program_proof/tulip/paxos/program/repr.v | 16 +-- .../tulip/paxos/program/resume.v | 2 +- src/program_proof/tulip/paxos/program/start.v | 4 +- src/program_proof/tulip/paxos/res.v | 32 +++--- .../tulip/program/gcoord/encode.v | 4 +- .../tulip/program/util/decode_string.v | 1 - .../tulip/program/util/encode_strings.v | 2 +- src/program_proof/tulip/res_txnsys.v | 6 +- .../tutorial/kvservice/full_proof.v | 103 ++++++++---------- src/program_proof/tutorial/kvservice/proof.v | 43 ++++---- .../txn/twophase_sub_logical_reln_defs.v | 2 +- src/program_proof/vrsm/apps/vkv/kv_proof.v | 8 +- .../vrsm/apps/vkv/kv_vsm_proof.v | 30 ++--- src/program_proof/vrsm/paxos/start_proof.v | 4 +- src/program_proof/vrsm/storage/proof.v | 2 +- src/program_proof/wp_auto/experiments.v | 2 +- 71 files changed, 337 insertions(+), 421 deletions(-) diff --git a/src/program_proof/append_log_refinement.v b/src/program_proof/append_log_refinement.v index 2aa4c34d6..364c9d43f 100644 --- a/src/program_proof/append_log_refinement.v +++ b/src/program_proof/append_log_refinement.v @@ -137,7 +137,7 @@ Definition append_op_trans (op: log_spec_ext.(@spec_ffi_op_field).(@external)) : end. Inductive append_trans : @val log_op -> @val disk_op -> Prop := -| AppendTrans (x: string) op: +| AppendTrans (x: byte_string) op: append_trans (λ: x, ExternalOp op (Var x)) (append_op_trans op). diff --git a/src/program_proof/bank/bank_proof.v b/src/program_proof/bank/bank_proof.v index b68350eb4..3874d398a 100644 --- a/src/program_proof/bank/bank_proof.v +++ b/src/program_proof/bank/bank_proof.v @@ -4,11 +4,11 @@ From Perennial.program_proof.lock Require Import lock_proof. From Goose.github_com.mit_pdos.gokv Require Import lockservice bank. Class bankG Σ := { - #[global] bank_mapG :: mapG Σ string u64 ; + #[global] bank_mapG :: mapG Σ byte_string u64 ; }. Definition bankΣ := - #[mapΣ string u64]. + #[mapΣ byte_string u64]. Global Instance subG_pbΣ {Σ} : subG (bankΣ) Σ → (bankG Σ). Proof. solve_inG. Qed. @@ -18,23 +18,23 @@ Context `{!invGS Σ, !bankG Σ}. Record bank_names := BankNames { bank_ls_names: (lock_names (Σ:=Σ)) ; (* Logical balances of accounts; must match the physical balance by the time you give up the lock *) - bank_kvptsto : string → string → iProp Σ ; (* Logical balances of accounts; must match the physical balance by the time you give up the lock *) + bank_kvptsto : byte_string → byte_string → iProp Σ ; (* Logical balances of accounts; must match the physical balance by the time you give up the lock *) bank_logBalGN : gname ; (* Logical balances of accounts; must match the physical balance by the time you give up the lock *) }. Definition log_gn γ := γ.(bank_logBalGN). Definition lock_gn γ := γ.(bank_ls_names). -Definition bankPs γ := λ k, (∃ v, bank_kvptsto γ k (bytes_to_string $ u64_le v) ∗ k [[log_gn γ]]↦v)%I. +Definition bankPs γ := λ k, (∃ v, bank_kvptsto γ k (u64_le v) ∗ k [[log_gn γ]]↦v)%I. Definition bankN := nroot .@ "grove_bank_of_boston". Definition lockN : namespace := nroot.@"grove_bank_of_boston_vault". Definition bal_total : u64 := 1000. -Context (init_flag: string). (* Account names for bank *) +Context (init_flag: byte_string). (* Account names for bank *) -Definition map_total (m : gmap string u64) : u64 := +Definition map_total (m : gmap byte_string u64) : u64 := map_fold (λ k v tot, word.add tot v) 0 m. Lemma map_total_insert m k v : @@ -72,7 +72,7 @@ Proof. Qed. Lemma map_total_zero m : - map_Forall (λ (_:string) (x : u64), x = 0) m -> + map_Forall (λ (_:byte_string) (x : u64), x = 0) m -> map_total m = 0. Proof. induction m using map_ind. @@ -108,22 +108,22 @@ Proof. done. Qed. -Definition bank_inv γ (accts : gset string) : iProp Σ := - ∃ (m:gmap string u64), +Definition bank_inv γ (accts : gset byte_string) : iProp Σ := + ∃ (m:gmap byte_string u64), "HlogBalCtx" ∷ map_ctx (log_gn γ) 1 m ∗ "%" ∷ ⌜map_total m = bal_total⌝ ∗ "%" ∷ ⌜dom m = accts⌝ . -Definition init_lock_inv γlk kvptsto (accts:gset string) : iProp Σ := +Definition init_lock_inv γlk kvptsto (accts:gset byte_string) : iProp Σ := (* Uninit case *) - (kvptsto init_flag "" ∗ - [∗ set] acc ∈ accts, kvptsto acc "" ∗ kvptsto_lock γlk acc "" + (kvptsto init_flag ""%go ∗ + [∗ set] acc ∈ accts, kvptsto acc ""%go ∗ kvptsto_lock γlk acc ""%go ) ∨ (* Already init case *) (∃ γlog, let γ := (BankNames γlk kvptsto γlog) in - bank_kvptsto γ init_flag "1" ∗ inv bankN (bank_inv γ accts) ∗ + bank_kvptsto γ init_flag "1"%go ∗ inv bankN (bank_inv γ accts) ∗ [∗ set] acc ∈ accts, is_lock lockN (lock_gn γ) acc (bankPs γ acc)). Definition is_bank γlk kvptsto accs : iProp Σ := @@ -135,10 +135,10 @@ End bank_defs. Section bank_proof. Context `{!heapGS Σ (ext:=grove_op) (ffi:=grove_model), !bankG Σ}. -Context (init_flag: string). (* Account names for bank *) +Context (init_flag: byte_string). (* Account names for bank *) -Definition own_bank_clerk (bank_ck:loc) (accts : gset string) : iProp Σ := - ∃ (lck kck : loc) (accts_s : Slice.t) (accts_l : list string) γ E, +Definition own_bank_clerk (bank_ck:loc) (accts : gset byte_string) : iProp Σ := + ∃ (lck kck : loc) (accts_s : Slice.t) (accts_l : list byte_string) γ E, "%" ∷ ⌜Permutation (elements accts) (accts_l)⌝ ∗ "#Hlck_is" ∷ is_LockClerk lockN lck (lock_gn γ) ∗ "#Hkck_is" ∷ is_Kv kck (bank_kvptsto γ) E ∗ @@ -153,7 +153,7 @@ Definition own_bank_clerk (bank_ck:loc) (accts : gset string) : iProp Σ := "#Haccts_is_lock" ∷ [∗ list] acc ∈ accts_l, is_lock lockN (lock_gn γ) acc (bankPs γ acc) . -Lemma acquire_two_spec (lck :loc) (ln1 ln2:string) γ: +Lemma acquire_two_spec (lck :loc) (ln1 ln2:byte_string) γ: {{{ is_LockClerk lockN lck γ.(bank_ls_names) ∗ is_lock lockN γ.(bank_ls_names) ln1 (bankPs γ ln1) ∗ @@ -178,7 +178,7 @@ Proof. iApply "Hpost". by iFrame. Qed. -Lemma release_two_spec (lck :loc) (ln1 ln2:string) γ: +Lemma release_two_spec (lck :loc) (ln1 ln2:byte_string) γ: {{{ is_LockClerk lockN lck γ.(bank_ls_names) ∗ is_lock lockN γ.(bank_ls_names) ln1 (bankPs γ ln1) ∗ @@ -205,7 +205,7 @@ Lemma wp_decodeInt (x:u64) : {{{ True }}} - decodeInt #(str bytes_to_string (u64_le x)) + decodeInt #(str (u64_le x)) {{{ RET #x; True }}} @@ -217,7 +217,6 @@ Proof. wp_apply wp_StringToBytes. iIntros (?) "Hsl". iDestruct (own_slice_to_small with "Hsl") as "Hsl". - rewrite bytes_to_string_to_bytes. wp_apply (wp_ReadInt with "[$]"). iIntros. wp_pures. iModIntro. by iApply "HΦ". Qed. @@ -228,7 +227,7 @@ Lemma wp_encodeInt (x:u64) : }}} encodeInt #x {{{ - RET #(str bytes_to_string (u64_le x)); True + RET #(str (u64_le x)); True }}} . Proof. @@ -245,7 +244,7 @@ Proof. simpl. by iApply "HΦ". Qed. -Lemma Bank__transfer_internal_spec (bck:loc) (src dst:string) (amount:u64) accts : +Lemma Bank__transfer_internal_spec (bck:loc) (src dst:byte_string) (amount:u64) accts : {{{ own_bank_clerk bck accts ∗ ⌜ src ∈ accts ⌝ ∗ @@ -461,7 +460,7 @@ Proof. "%Hlocked_dom" ∷ ⌜Permutation (elements (dom locked)) done⌝ ∗ "Hml" ∷ [∗ map] acc ↦ bal ∈ locked, is_lock lockN γ.(bank_ls_names) acc (bankPs γ acc) ∗ - (bank_kvptsto γ acc (bytes_to_string $ u64_le $ bal) ∗ acc [[log_gn γ]]↦ bal))%I + (bank_kvptsto γ acc (u64_le $ bal) ∗ acc [[log_gn γ]]↦ bal))%I with "[] [$Haccts_slice Hsum $Hlck $Hkck]"). 2: { iExists ∅. rewrite map_total_empty. iFrame. @@ -540,7 +539,7 @@ Proof. iNamed "HbankInv". iDestruct (big_sepM_sep with "Hml") as "[#Hml_islock Hmlkv]". - iDestruct (big_sepM_mono_wand _ (λ k v, ⌜m !! k = Some v⌝ ∗ bank_kvptsto γ k (bytes_to_string $ u64_le v) ∗ k [[log_gn γ]]↦ v)%I _ (map_ctx (log_gn γ) 1 m)%I with "[] [$HlogBalCtx $Hmlkv]") as "[HlogBalCtx Hmlkv]". + iDestruct (big_sepM_mono_wand _ (λ k v, ⌜m !! k = Some v⌝ ∗ bank_kvptsto γ k (u64_le v) ∗ k [[log_gn γ]]↦ v)%I _ (map_ctx (log_gn γ) 1 m)%I with "[] [$HlogBalCtx $Hmlkv]") as "[HlogBalCtx Hmlkv]". { iModIntro. iIntros (??) "%Hsome [HlogBalCtx HbankPs]". @@ -578,7 +577,7 @@ Proof. "Hlck" ∷ bck ↦[BankClerk :: "lck"] #lck ∗ "%Hdom" ∷ ⌜Permutation (elements (dom mtodo)) todo⌝ ∗ "Hml" ∷ [∗ map] k↦x ∈ mtodo, is_lock lockN γ.(bank_ls_names) k (bankPs γ k) ∗ - (bank_kvptsto γ k (bytes_to_string $ u64_le x) ∗ k [[log_gn γ]]↦ x))%I + (bank_kvptsto γ k (u64_le x) ∗ k [[log_gn γ]]↦ x))%I with "[] [$Haccts_slice $Hlck Hml]"). { iIntros (?? ??) "%Hx". @@ -638,7 +637,7 @@ Proof. iModIntro. iLeft. iFrame. eauto. Qed. -Lemma wp_MakeBankClerkSlice (lck kck : loc) γlk kvptsto E accts (accts_s : Slice.t) acc0 (accts_l : list string) : +Lemma wp_MakeBankClerkSlice (lck kck : loc) γlk kvptsto E accts (accts_s : Slice.t) acc0 (accts_l : list byte_string) : {{{ is_LockClerk lockN lck γlk ∗ is_Kv kck kvptsto E ∗ @@ -706,15 +705,15 @@ Proof. rewrite skipn_cons. replace (drop 0 accts_l) with (accts_l) by reflexivity. wp_apply (wp_forSlicePrefix - (λ done todo, ∃ (sdone: gset string), + (λ done todo, ∃ (sdone: gset byte_string), "kvck" ∷ l ↦[BankClerk :: "kvck"] #kck ∗ "Htodo" ∷ ([∗ list] acc ∈ todo, - "Hkv2" ∷ kvptsto_lock γlk acc "" ∗ - "Hkv1" ∷ kvptsto acc "") ∗ + "Hkv2" ∷ kvptsto_lock γlk acc ""%go ∗ + "Hkv1" ∷ kvptsto acc ""%go) ∗ "%Hdone_dom" ∷ ⌜Permutation (elements sdone) done⌝ ∗ "Hdone" ∷ [∗ map] acc ↦ bal ∈ (gset_to_gmap (W64 0) sdone), - kvptsto_lock γlk acc "" ∗ - kvptsto acc (bytes_to_string $ u64_le bal) + kvptsto_lock γlk acc ""%go ∗ + kvptsto acc (u64_le bal) )%I with "[] [$Haccts_slice $kvck Haccs]"). { iIntros (????) "%Hx". @@ -868,7 +867,7 @@ Proof. iDestruct (big_sepS_elements with "H") as "He". rewrite Hperm. iFrame "He". Qed. -Lemma wp_MakeBankClerk (lck kck : loc) γlk kvptsto (acc0 acc1 : string ) E : +Lemma wp_MakeBankClerk (lck kck : loc) γlk kvptsto (acc0 acc1 : byte_string ) E : {{{ is_LockClerk lockN lck γlk ∗ is_Kv kck kvptsto E ∗ diff --git a/src/program_proof/cachekv/proof.v b/src/program_proof/cachekv/proof.v index c698e9a6c..bfc2956df 100644 --- a/src/program_proof/cachekv/proof.v +++ b/src/program_proof/cachekv/proof.v @@ -7,7 +7,7 @@ From iris.base_logic.lib Require Import ghost_map. Module cacheValueC. Record t := mk { - v : string ; + v : byte_string ; l : u64 ; }. @@ -31,11 +31,11 @@ End cacheValueC. Section proof. Context `{!heapGS Σ}. -Context `{!ghost_mapG Σ string string}. +Context `{!ghost_mapG Σ byte_string byte_string}. Context `{!renewable_leaseG Σ}. -Definition encode_cacheValue (v:string) (lease:u64) : string := - (bytes_to_string $ u64_le lease) ++ v. +Definition encode_cacheValue (v:byte_string) (lease:u64) : byte_string := + (u64_le lease) ++ v. Lemma encode_cacheValue_inj v l v' l' : encode_cacheValue v l = encode_cacheValue v' l' → @@ -44,15 +44,11 @@ Lemma encode_cacheValue_inj v l v' l' : Proof. intros H. rewrite /encode_cacheValue in H. - apply (f_equal string_to_bytes) in H. - repeat rewrite string_to_bytes_app bytes_to_string_to_bytes in H. apply app_inj_1 in H. 2:{ done. } destruct H as [H1 H2]. split. - { - apply (f_equal bytes_to_string) in H2. repeat rewrite string_to_bytes_to_string in H2. done. - } + { done. } apply (f_equal le_to_u64) in H1. repeat rewrite u64_le_to_word in H1. done. @@ -72,7 +68,7 @@ Definition kvptsto γ key value : iProp Σ := . (* KV points-to for the internal kv service *) -Implicit Types kvptsto_int: string → string → iProp Σ. +Implicit Types kvptsto_int: byte_string → byte_string → iProp Σ. Definition is_cachekv_inv kvptsto_int γ : iProp Σ := inv invN (∃ kvs, @@ -88,7 +84,7 @@ Definition is_cachekv_inv kvptsto_int γ : iProp Σ := . Definition own_CacheKv (k:loc) γ : iProp Σ := - ∃ (cache_ptr:loc) (cache:gmap string cacheValueC.t), + ∃ (cache_ptr:loc) (cache:gmap byte_string cacheValueC.t), "Hcache_ptr" ∷ k ↦[CacheKv :: "cache"] #cache_ptr ∗ "Hcache" ∷ own_map cache_ptr (DfracOwn 1) cache ∗ "#Hleases" ∷ ([∗ map] k ↦ cv ∈ cache, @@ -124,18 +120,18 @@ Proof. iIntros (?) "Hptr". wp_pures. wp_load. - rewrite /encode_cacheValue string_to_bytes_app bytes_to_string_to_bytes. + rewrite /encode_cacheValue. iDestruct (own_slice_to_small with "Hsl") as "Hsl". wp_apply (wp_ReadInt with "[$Hsl]"). iIntros (?) "Hsl". wp_pures. wp_apply (wp_StringFromBytes with "[$]"). - iIntros "_". rewrite string_to_bytes_to_string. + iIntros "_". wp_pures. iModIntro. by iApply "HΦ". Qed. -Lemma wp_EncodeValue (v:string) (l:u64) : +Lemma wp_EncodeValue (v:byte_string) (l:u64) : {{{ True }}} EncodeValue (to_val (cacheValueC.mk v l)) {{{ RET #(str encode_cacheValue v l); True }}}. @@ -166,7 +162,6 @@ Proof. iIntros "_". Opaque u64_le. simpl. rewrite replicate_0 /=. - rewrite bytes_to_string_app string_to_bytes_to_string. by iApply "HΦ". Qed. diff --git a/src/program_proof/ctrexample/server.v b/src/program_proof/ctrexample/server.v index a67360c2d..d0d974afb 100644 --- a/src/program_proof/ctrexample/server.v +++ b/src/program_proof/ctrexample/server.v @@ -15,7 +15,7 @@ Context `{!heapGS Σ}. Context `{!inG Σ mono_natUR}. Context `{stagedG Σ}. -Definition ctrname := "ctr". +Definition ctrname := "ctr"%go. Definition own_CtrServer_durable (c:u64) : iProp Σ := ∃ l, ctrname f↦ l ∗ diff --git a/src/program_proof/lockservice/aof_proof.v b/src/program_proof/lockservice/aof_proof.v index 54cd061fc..7d1ab8ed4 100644 --- a/src/program_proof/lockservice/aof_proof.v +++ b/src/program_proof/lockservice/aof_proof.v @@ -72,7 +72,7 @@ Definition is_aof aof_ptr γ (aof_ctx : (list u8) → iProp Σ) : iProp Σ := . (* TODO: upgrade to WPC *) -Lemma wp_CreateAppendOnlyFile (fname:string) data aof_ctx : +Lemma wp_CreateAppendOnlyFile (fname:byte_string) data aof_ctx : {{{ fname f↦{1} data ∗ aof_ctx data diff --git a/src/program_proof/lockservice/grove_ffi.v b/src/program_proof/lockservice/grove_ffi.v index 2b5625684..b70f8e978 100644 --- a/src/program_proof/lockservice/grove_ffi.v +++ b/src/program_proof/lockservice/grove_ffi.v @@ -26,10 +26,10 @@ Context `{!heapGS Σ}. Class filesysG Σ := FileSysG { filesys_gname : gname ; (* Name of str -> []byte authmap used for filesys ffi *) - #[global] filesys_inG :: mapG Σ string (list byte) + #[global] filesys_inG :: mapG Σ byte_string (list byte) }. -Definition file_pointsto {fG:filesysG Σ} (s:string) (c:list byte) (q:Qp): iProp Σ := +Definition file_pointsto {fG:filesysG Σ} (s:byte_string) (c:list byte) (q:Qp): iProp Σ := s [[filesys_gname]]↦{q} c. Context `{!filesysG Σ}. @@ -83,7 +83,7 @@ Axiom wpc_AtomicAppend : ∀ filename content_old content (content_sl:Slice.t) q filename f↦ (content_old ++ content) }}}. -Definition u64_to_string : u64 -> string := λ u, NilZero.string_of_int (Z.to_int (uint.Z u)). +Definition u64_to_string : u64 -> byte_string := λ u, NilZero.string_of_int (Z.to_int (uint.Z u)). (* Spec for W64ToString will be annoying *) Axiom wp_U64ToString : ∀ (u:u64), @@ -97,7 +97,7 @@ Axiom wp_U64ToString : ∀ (u:u64), Class rpcregG Σ := RpcRegG { rpcreg_gname : gname ; - #[global] rpcreg_inG :: ghost_mapG Σ (string*u64) ((list u8 → laterO (iPropO Σ)) * (list u8 → list u8 → laterO (iPropO Σ))) + #[global] rpcreg_inG :: ghost_mapG Σ (byte_string*u64) ((list u8 → laterO (iPropO Σ)) * (list u8 → list u8 → laterO (iPropO Σ))) }. (* XXX: these laters probably aren't a problem, because the eventual implementation of RPC will possibly have to use invariants to move the Pre to diff --git a/src/program_proof/lockservice/kv_proof.v b/src/program_proof/lockservice/kv_proof.v index 841444bba..e8004ae91 100644 --- a/src/program_proof/lockservice/kv_proof.v +++ b/src/program_proof/lockservice/kv_proof.v @@ -31,7 +31,7 @@ Definition Put_Pre γ : RPCValsC -> iProp Σ := (λ args, args.(W64_1) [[γ.(ks_ Definition Put_Post γ : RPCValsC -> u64 -> iProp Σ := (λ args _, args.(W64_1) [[γ.(ks_kvMapGN)]]↦ args.(W64_2))%I. (* FIXME: this is currently just a placeholder *) -Definition KVClerk_own γ ck_ptr (host : string) : iProp Σ := +Definition KVClerk_own γ ck_ptr (host : byte_string) : iProp Σ := ∃ (cl_ptr:loc), "Hcl_ptr" ∷ ck_ptr ↦[KVClerk :: "client"] #cl_ptr ∗ "Hprimary" ∷ ck_ptr ↦[KVClerk :: "primary"] #(str host) ∗ @@ -250,14 +250,14 @@ Qed. (* TODO: see if any more repetition can be removed *) -Definition is_kvserver_host γ (host:string) : iProp Σ := +Definition is_kvserver_host γ (host:byte_string) : iProp Σ := "#Hputspec" ∷ ( handler_is2 host (W64 1) γ.(ks_rpcGN) (Put_Pre γ) (Put_Post γ)) ∗ "#Hgetspec" ∷ (∀ va, handler_is2 host (W64 2) γ.(ks_rpcGN) (Get_Pre γ va) (Get_Post γ va)) ∗ "#Hrpcserver" ∷ is_RPCServer γ.(ks_rpcGN). -Lemma KVClerk__Get_spec (kck:loc) (srv:string) (key va:u64) γ : +Lemma KVClerk__Get_spec (kck:loc) (srv:byte_string) (key va:u64) γ : is_kvserver_host γ srv -∗ {{{ KVClerk_own γ kck srv ∗ (key [[γ.(ks_kvMapGN)]]↦ va) @@ -289,7 +289,7 @@ Proof. iExists _; iFrame. Qed. -Lemma KVClerk__Put_spec (kck:loc) (srv:string) (key va:u64) γ : +Lemma KVClerk__Put_spec (kck:loc) (srv:byte_string) (key va:u64) γ : is_kvserver_host γ srv -∗ {{{ KVClerk_own γ kck srv ∗ (key [[γ.(ks_kvMapGN)]]↦ _ ) diff --git a/src/program_proof/lockservice/rpc_proof.v b/src/program_proof/lockservice/rpc_proof.v index 9ed14f1c4..cb650e87b 100644 --- a/src/program_proof/lockservice/rpc_proof.v +++ b/src/program_proof/lockservice/rpc_proof.v @@ -58,7 +58,7 @@ Definition RPCServer_own_vol (sv:loc) (γrpc:rpc_names) (lastSeqM lastReplyM:gma Definition Reply64 := @RPCReply (u64). -Definition RPCClient_own_vol (cl_ptr:loc) (cid seqno:u64) (host:string) : iProp Σ := +Definition RPCClient_own_vol (cl_ptr:loc) (cid seqno:u64) (host:byte_string) : iProp Σ := ∃ (rawCl:loc), "%" ∷ ⌜uint.nat seqno > 0⌝ ∗ "Hcid" ∷ cl_ptr ↦[RPCClient :: "cid"] #cid ∗ @@ -67,7 +67,7 @@ Definition RPCClient_own_vol (cl_ptr:loc) (cid seqno:u64) (host:string) : iProp "HrawClOwn" ∷ grove_ffi.RPCClient_own rawCl host . -Definition RPCClient_own (cl_ptr:loc) (host:string) γrpc : iProp Σ := +Definition RPCClient_own (cl_ptr:loc) (host:byte_string) γrpc : iProp Σ := ∃ cid seqno, RPCClient_own_vol cl_ptr cid seqno host ∗ RPCClient_own_ghost γrpc cid seqno @@ -453,7 +453,7 @@ Definition EncodedPost2 {X:Type} Post : (X → list u8 → list u8 → iProp Σ) (* This says an rpc handler has the given PreCond and PostCond; it does NOT say that the handler sits behind a reply table with the given Pre/Post. *) -Definition handler_is2 (X:Type) (host:string) (rpcid:u64) PreCond PostCond : iProp Σ := +Definition handler_is2 (X:Type) (host:byte_string) (rpcid:u64) PreCond PostCond : iProp Σ := handler_is X host rpcid (EncodedPre2 PreCond) (EncodedPost2 PostCond) . @@ -461,7 +461,7 @@ Definition is_rpcHandler2 {X:Type} f Pre Post : iProp Σ := is_rpcHandler (X:=X) f (EncodedPre2 Pre) (EncodedPost2 Post) . -Lemma wp_RemoteProcedureCall2 (cl_ptr req_ptr reply_ptr:loc) (host:string) (rpcid:u64) (req:RPCRequestID) args (reply:Reply64) X PreCond PostCond x: +Lemma wp_RemoteProcedureCall2 (cl_ptr req_ptr reply_ptr:loc) (host:byte_string) (rpcid:u64) (req:RPCRequestID) args (reply:Reply64) X PreCond PostCond x: handler_is2 X host rpcid PreCond PostCond -∗ {{{ "#HargsPre" ∷ □ PreCond x req args ∗ @@ -549,7 +549,7 @@ Proof. done. Admitted. -Lemma RPCClient__MakeRequest_spec {X:Type} (host:string) (rpcid:u64) cl_ptr args γrpc X PreCond PostCond (x:X): +Lemma RPCClient__MakeRequest_spec {X:Type} (host:byte_string) (rpcid:u64) cl_ptr args γrpc X PreCond PostCond (x:X): ∀ RawPreCond, handler_is2 X host rpcid RawPreCond (λ y req args reply, RPCRequestStale γrpc req ∨ RPCReplyReceipt γrpc req reply.(Rep_Ret)) -∗ □(∀ y req γreq, is_RPCRequest γrpc γreq (PreCond x args) (PostCond x args) req -∗ RawPreCond y req args) -∗ {{{ @@ -648,7 +648,7 @@ Proof using Type*. iPureIntro. lia. Qed. -Lemma MakeRPCClient_spec γrpc (host : string) (cid : u64) : +Lemma MakeRPCClient_spec γrpc (host : byte_string) (cid : u64) : {{{ RPCClient_own_ghost γrpc cid 1 }}} MakeRPCClient #(str host) #cid {{{ cl, RET #cl; RPCClient_own cl host γrpc }}}. diff --git a/src/program_proof/mvcc/mvcc_prelude.v b/src/program_proof/mvcc/mvcc_prelude.v index ab665b8ee..3c916361c 100644 --- a/src/program_proof/mvcc/mvcc_prelude.v +++ b/src/program_proof/mvcc/mvcc_prelude.v @@ -3,12 +3,12 @@ From Perennial.program_logic Require Export atomic. (* prefer the ncfupd atomics (* Prefer untyped slices. *) Export Perennial.goose_lang.lib.slice.slice. -Definition dbval := option string. +Definition dbval := option byte_string. Canonical Structure dbvalO := leibnizO dbval. Notation Nil := (None : dbval). Notation Value x := (Some x : dbval). -Definition to_dbval (b : bool) (v : string) := +Definition to_dbval (b : bool) (v : byte_string) := if b then Value v else Nil. Definition dbmap := gmap u64 dbval. diff --git a/src/program_proof/mvcc/strnum.v b/src/program_proof/mvcc/strnum.v index 2f1d33bed..efbe97153 100644 --- a/src/program_proof/mvcc/strnum.v +++ b/src/program_proof/mvcc/strnum.v @@ -12,7 +12,7 @@ Lemma u64_to_string_inj n1 n2 : n1 = n2. Admitted. -Theorem wp_StringToU64 (s : string) (n : u64) : +Theorem wp_StringToU64 (s : byte_string) (n : u64) : {{{ ⌜u64_to_string n = s⌝ }}} StringToU64 #(LitString s) {{{ (n : u64), RET #n; ⌜u64_to_string n = s⌝ }}}. @@ -21,7 +21,7 @@ Admitted. Theorem wp_U64ToString (n : u64) : {{{ True }}} U64ToString #n - {{{ (s : string), RET #(LitString s); ⌜u64_to_string n = s⌝ }}}. + {{{ (s : byte_string), RET #(LitString s); ⌜u64_to_string n = s⌝ }}}. Admitted. End program. diff --git a/src/program_proof/mvcc/tuple_append_version.v b/src/program_proof/mvcc/tuple_append_version.v index bfb6faa3a..013dd4eb2 100644 --- a/src/program_proof/mvcc/tuple_append_version.v +++ b/src/program_proof/mvcc/tuple_append_version.v @@ -6,7 +6,7 @@ Context `{!heapGS Σ, !mvcc_ghostG Σ}. (*****************************************************************) (* func (tuple *Tuple) appendVersion(tid uint64, val string) *) (*****************************************************************) -Theorem wp_tuple__appendVersion tuple (tid : u64) (val : string) owned tidlast vers : +Theorem wp_tuple__appendVersion tuple (tid : u64) (val : byte_string) owned tidlast vers : {{{ own_tuple_phys tuple owned tidlast vers }}} Tuple__appendVersion #tuple #tid #(LitString val) {{{ RET #(); own_tuple_phys tuple false (W64 (uint.Z tid + 1)) (vers ++ [(tid, false, val)]) }}}. @@ -49,7 +49,7 @@ Qed. (* func (tuple *Tuple) AppendVersion(tid uint64, val string) *) (*****************************************************************) Theorem wp_tuple__AppendVersion - tuple (tid : u64) (val : string) (key : u64) (sid : u64) + tuple (tid : u64) (val : byte_string) (key : u64) (sid : u64) (phys : list dbval) γ : {{{ active_tid γ tid sid ∗ own_tuple_locked tuple key (uint.nat tid) phys (extend (S (uint.nat tid)) phys ++ [Value val]) γ diff --git a/src/program_proof/mvcc/tuple_kill_version.v b/src/program_proof/mvcc/tuple_kill_version.v index 3b8002057..34c46cc76 100644 --- a/src/program_proof/mvcc/tuple_kill_version.v +++ b/src/program_proof/mvcc/tuple_kill_version.v @@ -9,7 +9,7 @@ Context `{!heapGS Σ, !mvcc_ghostG Σ}. Theorem wp_tuple__killVersion tuple (tid : u64) owned tidlast vers : {{{ own_tuple_phys tuple owned tidlast vers }}} Tuple__killVersion #tuple #tid - {{{ (ok : bool), RET #ok; own_tuple_phys tuple false (uint.Z tid + 1) (vers ++ [(tid, true, "")]) }}}. + {{{ (ok : bool), RET #ok; own_tuple_phys tuple false (uint.Z tid + 1) (vers ++ [(tid, true, ""%go)]) }}}. Proof. iIntros (Φ) "HtuplePhys HΦ". iNamed "HtuplePhys". diff --git a/src/program_proof/mvcc/tuple_mk.v b/src/program_proof/mvcc/tuple_mk.v index 195f541b7..ab45cef1c 100644 --- a/src/program_proof/mvcc/tuple_mk.v +++ b/src/program_proof/mvcc/tuple_mk.v @@ -92,7 +92,7 @@ Proof. { iNext. unfold P. unfold own_tuple. - iExists false, (W64 1), (W64 0), [(W64 0, true, "")], [Nil; Nil]. + iExists false, (W64 1), (W64 0), [(W64 0, true, ""%go)], [Nil; Nil]. iFrame. iSplit. { (* Prove [HtupleAbs]. *) diff --git a/src/program_proof/mvcc/tuple_prelude.v b/src/program_proof/mvcc/tuple_prelude.v index 6e339bb38..bd05d2531 100644 --- a/src/program_proof/mvcc/tuple_prelude.v +++ b/src/program_proof/mvcc/tuple_prelude.v @@ -1,7 +1,7 @@ From Perennial.program_proof.mvcc Require Export mvcc_prelude mvcc_misc mvcc_ghost mvcc_inv. From Goose.github_com.mit_pdos.vmvcc Require Export tuple. -Definition pver := (u64 * bool * string)%type. +Definition pver := (u64 * bool * byte_string)%type. (* TODO: rename to [pver_to_val]. *) Definition ver_to_val (x : pver) := @@ -25,9 +25,9 @@ Definition spec_lookup (vers : list pver) (tid : u64) : dbval := | None => Nil end. -Lemma val_to_ver_with_lookup (x : val) (l : list (u64 * bool * string)) (i : nat) : +Lemma val_to_ver_with_lookup (x : val) (l : list (u64 * bool * byte_string)) (i : nat) : (ver_to_val <$> l) !! i = Some x -> - (∃ (b : u64) (d : bool) (v : string), x = ver_to_val (b, d, v) ∧ l !! i = Some (b, d, v)). + (∃ (b : u64) (d : bool) (v : byte_string), x = ver_to_val (b, d, v) ∧ l !! i = Some (b, d, v)). Proof. intros H. apply list_lookup_fmap_inv in H as [[[y1 y2] y3] [Heq Hsome]]. diff --git a/src/program_proof/mvcc/tuple_read_version.v b/src/program_proof/mvcc/tuple_read_version.v index b1e14b5ac..d7bfbfea9 100644 --- a/src/program_proof/mvcc/tuple_read_version.v +++ b/src/program_proof/mvcc/tuple_read_version.v @@ -7,7 +7,7 @@ Context `{!heapGS Σ, !mvcc_ghostG Σ}. (* func findVersion(tid uint64, vers []Version) Version *) (*******************************************************************) Local Theorem wp_findVersion (tid : u64) (versS : Slice.t) - (vers : list (u64 * bool * string)) : + (vers : list (u64 * bool * byte_string)) : {{{ ⌜∃ (ver : pver), (ver ∈ vers) ∧ (uint.Z ver.1.1 < uint.Z tid)⌝ ∗ slice.own_slice versS (structTy Version) (DfracOwn 1) (ver_to_val <$> vers) }}} @@ -49,7 +49,7 @@ Proof. (* idx++ *) (* } *) (***********************************************************) - set P := λ (b : bool), (∃ (ver : u64 * bool * string) (idx : u64), + set P := λ (b : bool), (∃ (ver : u64 * bool * byte_string) (idx : u64), "HverR" ∷ (verR ↦[struct.t Version] ver_to_val ver) ∗ "HidxR" ∷ (idxR ↦[uint64T] #idx) ∗ "HversS" ∷ own_slice_small versS (struct.t Version) (DfracOwn 1) (ver_to_val <$> vers) ∗ @@ -144,7 +144,7 @@ Proof. } { (* Loop entry. *) unfold P. - iExists (W64 0, false, ""). + iExists (W64 0, false, ""%go). iExists _. iFrame. iPureIntro. @@ -307,7 +307,7 @@ Theorem wp_tuple__ReadVersion ⌜owned = false ∨ (uint.nat tid < length vchain)%nat⌝ }}} Tuple__ReadVersion #tuple #tid - {{{ (val : string) (found : bool), RET (#(LitString val), #found); + {{{ (val : byte_string) (found : bool), RET (#(LitString val), #found); active_tid γ tid sid ∗ ptuple_ptsto γ key (to_dbval found val) (uint.nat tid) }}}. Proof. diff --git a/src/program_proof/mvcc/tuple_remove_versions.v b/src/program_proof/mvcc/tuple_remove_versions.v index deb868054..5b11b2d3b 100644 --- a/src/program_proof/mvcc/tuple_remove_versions.v +++ b/src/program_proof/mvcc/tuple_remove_versions.v @@ -5,7 +5,7 @@ Context `{!heapGS Σ, !mvcc_ghostG Σ}. Lemma val_to_ver_with_val_ty (x : val) : val_ty x (uint64T * (boolT * (stringT * unitT))%ht) -> - (∃ (b : u64) (e : bool) (v : string), x = ver_to_val (b, e, v)). + (∃ (b : u64) (e : bool) (v : byte_string), x = ver_to_val (b, e, v)). Proof. intros H. inversion_clear H. diff --git a/src/program_proof/mvcc/txn_read.v b/src/program_proof/mvcc/txn_read.v index eed906c45..907ec6f65 100644 --- a/src/program_proof/mvcc/txn_read.v +++ b/src/program_proof/mvcc/txn_read.v @@ -34,7 +34,7 @@ Context `{!heapGS Σ, !mvcc_ghostG Σ}. Theorem wp_txn__Read txn tid view (k : u64) dbv γ τ : {{{ own_txn txn tid view γ τ ∗ txnmap_ptsto τ k dbv }}} Txn__Read #txn #k - {{{ (v : string) (found : bool), RET (#(LitString v), #found); + {{{ (v : byte_string) (found : bool), RET (#(LitString v), #found); own_txn txn tid view γ τ ∗ txnmap_ptsto τ k dbv ∗ ⌜dbv = to_dbval found v⌝ }}}. Proof. @@ -223,7 +223,7 @@ Proof. by iFrame "Hptsto". Qed. -Theorem wp_txn__Read_found txn tid view (k : u64) (v : string) γ τ : +Theorem wp_txn__Read_found txn tid view (k : u64) (v : byte_string) γ τ : {{{ own_txn txn tid view γ τ ∗ txnmap_ptsto τ k (Some v) }}} Txn__Read #txn #k {{{ RET (#(LitString v), #true); diff --git a/src/program_proof/mvcc/wrbuf_prelude.v b/src/program_proof/mvcc/wrbuf_prelude.v index 901cb27fc..f063fe144 100644 --- a/src/program_proof/mvcc/wrbuf_prelude.v +++ b/src/program_proof/mvcc/wrbuf_prelude.v @@ -1,12 +1,12 @@ From Perennial.program_proof.mvcc Require Export mvcc_prelude mvcc_misc mvcc_ghost. From Goose.github_com.mit_pdos.vmvcc Require Export wrbuf. -Definition wrent := (u64 * string * bool * loc)%type. +Definition wrent := (u64 * byte_string * bool * loc)%type. Definition wrent_to_val (x : wrent) := (#x.1.1.1, (#(LitString x.1.1.2), (#x.1.2, (#x.2, #()))))%V. -Lemma wrent_to_val_unfold (k : u64) (v : string) (w : bool) (t : loc) : +Lemma wrent_to_val_unfold (k : u64) (v : byte_string) (w : bool) (t : loc) : (#k, (#(LitString v), (#w, (#t, #()))))%V = wrent_to_val (k, v, w, t). Proof. reflexivity. Qed. @@ -18,7 +18,7 @@ Definition wrent_to_key_tpl (x : wrent) : (u64 * loc) := Lemma val_to_wrent_with_val_ty (x : val) : val_ty x (uint64T * (stringT * (boolT * (ptrT * unitT))))%ht -> - (∃ (k : u64) (v : string) (w : bool) (t : loc), x = wrent_to_val (k, v, w, t)). + (∃ (k : u64) (v : byte_string) (w : bool) (t : loc), x = wrent_to_val (k, v, w, t)). Proof. intros H. inversion_clear H. @@ -46,7 +46,7 @@ Qed. Lemma wrent_to_val_with_lookup (x : val) (l : list wrent) (i : nat) : (wrent_to_val <$> l) !! i = Some x -> - (∃ (k : u64) (v : string) (w : bool) (t : loc), x = wrent_to_val (k, v, w, t) ∧ l !! i = Some (k, v, w, t)). + (∃ (k : u64) (v : byte_string) (w : bool) (t : loc), x = wrent_to_val (k, v, w, t) ∧ l !! i = Some (k, v, w, t)). Proof. intros H. apply list_lookup_fmap_inv in H as [[[[k v] w] t] [Heq Hsome]]. diff --git a/src/program_proof/mvcc/wrbuf_proof.v b/src/program_proof/mvcc/wrbuf_proof.v index 38fd16cc2..9f24bcea4 100644 --- a/src/program_proof/mvcc/wrbuf_proof.v +++ b/src/program_proof/mvcc/wrbuf_proof.v @@ -197,7 +197,7 @@ Proof. Qed. (* TODO: Return values first or others first? Make it consistent. *) -Definition spec_wrbuf__Lookup (v : string) (b ok : bool) (key : u64) (m : gmap u64 dbval) := +Definition spec_wrbuf__Lookup (v : byte_string) (b ok : bool) (key : u64) (m : gmap u64 dbval) := if ok then m !! key = Some (to_dbval b v) else m !! key = None. (*****************************************************************) @@ -206,7 +206,7 @@ Definition spec_wrbuf__Lookup (v : string) (b ok : bool) (key : u64) (m : gmap u Theorem wp_wrbuf__Lookup wrbuf (key : u64) m : {{{ own_wrbuf_xtpls wrbuf m }}} WrBuf__Lookup #wrbuf #key - {{{ (v : string) (b ok : bool), RET (#(LitString v), #b, #ok); + {{{ (v : byte_string) (b ok : bool), RET (#(LitString v), #b, #ok); own_wrbuf_xtpls wrbuf m ∗ ⌜spec_wrbuf__Lookup v b ok key m⌝ }}}. Proof. @@ -271,7 +271,7 @@ Qed. (*****************************************************************) (* func (wrbuf *WrBuf) Put(key, val uint64) *) (*****************************************************************) -Theorem wp_wrbuf__Put wrbuf (key : u64) (val : string) m : +Theorem wp_wrbuf__Put wrbuf (key : u64) (val : byte_string) m : {{{ own_wrbuf_xtpls wrbuf m }}} WrBuf__Put #wrbuf #key #(LitString val) {{{ RET #(); own_wrbuf_xtpls wrbuf (<[ key := Value val ]> m) }}}. @@ -547,7 +547,7 @@ Proof. iApply "HΦ". unfold spec_search in Hsearch. (* [(W64 0), ""] is the zero-value of [u64, string]. *) - set ents' := (ents ++ [(key, "", false, null)]). + set ents' := (ents ++ [(key, ""%go, false, null)]). unfold own_wrbuf_xtpls. iExists _, ents'. diff --git a/src/program_proof/pav/serde.v b/src/program_proof/pav/serde.v index a9c0e00fc..7c965e9cb 100644 --- a/src/program_proof/pav/serde.v +++ b/src/program_proof/pav/serde.v @@ -146,13 +146,13 @@ End MapLabelPre. Module UpdateProof. Record t : Type := mk { - Updates : gmap string (list w8); + Updates : gmap byte_string (list w8); Sig: list w8 }. Section defs. Context `{!heapGS Σ}. Definition own (ptr : loc) (obj : t) : iProp Σ := - ∃ (updates_mref : loc) (updatesM : gmap string (Slice.t)) sig_sl, + ∃ (updates_mref : loc) (updatesM : gmap byte_string (Slice.t)) sig_sl, "HUpdates" ∷ ptr ↦[UpdateProof :: "Updates"] #updates_mref ∗ "HSig" ∷ ptr ↦[UpdateProof :: "Sig"] (slice_val sig_sl) ∗ "#HUpdatesM" ∷ own_map updates_mref DfracDiscarded updatesM ∗ diff --git a/src/program_proof/rsm/distx/program/index.v b/src/program_proof/rsm/distx/program/index.v index 5744ab365..adec01396 100644 --- a/src/program_proof/rsm/distx/program/index.v +++ b/src/program_proof/rsm/distx/program/index.v @@ -13,7 +13,7 @@ Section program. Persistent (is_index idx α). Admitted. - Theorem wp_Index__GetTuple (idx : loc) (key : string) α : + Theorem wp_Index__GetTuple (idx : loc) (key : byte_string) α : key ∈ keys_all -> is_index idx α -∗ {{{ True }}} diff --git a/src/program_proof/rsm/distx/program/replica.v b/src/program_proof/rsm/distx/program/replica.v index d0765b37a..f35d5ba53 100644 --- a/src/program_proof/rsm/distx/program/replica.v +++ b/src/program_proof/rsm/distx/program/replica.v @@ -868,7 +868,7 @@ Section program. by iApply "HΦ". Qed. - Theorem wp_Replica__Read (rp : loc) (ts : u64) (key : string) (gid : groupid) γ p α : + Theorem wp_Replica__Read (rp : loc) (ts : u64) (key : byte_string) (gid : groupid) γ p α : safe_read gid (uint.nat ts) key -> know_distx_inv γ p -∗ is_replica rp gid γ α -∗ @@ -982,7 +982,7 @@ Section program. ([∗ map] key ↦ tpl ∈ tpls_group gid tpls, hist_repl_lb γ key tpl.1). Theorem wp_Replica__applyRead - (rp : loc) (ts : u64) (key : string) (tpls tpls' : gmap dbkey dbtpl) + (rp : loc) (ts : u64) (key : byte_string) (tpls tpls' : gmap dbkey dbtpl) (stm stm' : gmap nat txnst) gid γ α : dom tpls = keys_all -> valid_key key -> diff --git a/src/program_proof/rsm/distx/program/replica_group.v b/src/program_proof/rsm/distx/program/replica_group.v index ff8a6083d..e5ff0604a 100644 --- a/src/program_proof/rsm/distx/program/replica_group.v +++ b/src/program_proof/rsm/distx/program/replica_group.v @@ -63,7 +63,7 @@ Section program. (*@ } @*) Admitted. - Theorem wp_ReplicaGroup__Read (rg : loc) (ts : u64) (key : string) gid γ : + Theorem wp_ReplicaGroup__Read (rg : loc) (ts : u64) (key : byte_string) gid γ : safe_read gid (uint.nat ts) key -> is_rg rg gid γ -∗ {{{ True }}} diff --git a/src/program_proof/rsm/distx/program/tuple.v b/src/program_proof/rsm/distx/program/tuple.v index dacf7b050..5ccd175c6 100644 --- a/src/program_proof/rsm/distx/program/tuple.v +++ b/src/program_proof/rsm/distx/program/tuple.v @@ -12,13 +12,13 @@ Section resource. the replica invariant, essentially forcing GC to not change the abstract view. *) - Definition hist_phys_quarter α (key : string) (hist : dbhist) : iProp Σ. + Definition hist_phys_quarter α (key : byte_string) (hist : dbhist) : iProp Σ. Admitted. - Definition hist_phys_half α (key : string) (hist : dbhist) : iProp Σ. + Definition hist_phys_half α (key : byte_string) (hist : dbhist) : iProp Σ. Admitted. - Definition hist_phys_lb α (key : string) (hist : dbhist) : iProp Σ. + Definition hist_phys_lb α (key : byte_string) (hist : dbhist) : iProp Σ. Admitted. #[global] @@ -43,13 +43,13 @@ Section resource. ⌜prefix histp hist⌝. Admitted. - Definition hist_phys_at α (key : string) (ts : nat) (v : dbval) : iProp Σ := + Definition hist_phys_at α (key : byte_string) (ts : nat) (v : dbval) : iProp Σ := ∃ hist, ⌜hist !! ts = Some v⌝ ∗ hist_phys_lb α key hist. - Definition ts_phys_half α (key : string) (tsprep : nat) : iProp Σ. + Definition ts_phys_half α (key : byte_string) (tsprep : nat) : iProp Σ. Admitted. - Definition tuple_phys_half α (key : string) (hist : dbhist) (tsprep : nat) : iProp Σ := + Definition tuple_phys_half α (key : byte_string) (hist : dbhist) (tsprep : nat) : iProp Σ := hist_phys_half α key hist ∗ ts_phys_half α key tsprep. End resource. @@ -57,7 +57,7 @@ End resource. Section program. Context `{!heapGS Σ, !distx_ghostG Σ}. - Definition is_tuple (tuple : loc) (key : string) (α : replica_names) : iProp Σ. + Definition is_tuple (tuple : loc) (key : byte_string) (α : replica_names) : iProp Σ. Admitted. #[global] @@ -71,7 +71,7 @@ Section program. timestamp different from the prepared timestamp. A more fundamental reason to this difference is that while Paxos allows deducing commit safety at the *replica* level, PCR can only deduce such at the *replica group* level. *) - Theorem wp_Tuple__AppendVersion (tuple : loc) (tid : u64) (val : string) key α : + Theorem wp_Tuple__AppendVersion (tuple : loc) (tid : u64) (val : byte_string) key α : is_tuple tuple key α -∗ {{{ True }}} <<< ∀∀ hist, hist_phys_half α key hist ∗ ⌜(length hist ≤ uint.nat tid)%nat⌝ >>> diff --git a/src/program_proof/rsm/distx/program/txn.v b/src/program_proof/rsm/distx/program/txn.v index 00405fca8..075afe49b 100644 --- a/src/program_proof/rsm/distx/program/txn.v +++ b/src/program_proof/rsm/distx/program/txn.v @@ -145,7 +145,7 @@ Section program. (* diff from [own_txn_stable] *) "%Hptgs" ∷ ⌜list_to_set ptgs = ptgroups (dom wrs)⌝. - Lemma wp_ResolveRead γ p (tid : u64) (key : string) (ts : nat) : + Lemma wp_ResolveRead γ p (tid : u64) (key : byte_string) (ts : nat) : ⊢ {{{ ⌜uint.nat tid = ts⌝ }}} <<< ∀∀ acs, txn_proph γ p acs >>> ResolveRead #p #tid #(LitString key) @ ∅ @@ -170,7 +170,7 @@ Section program. {{{ RET #(); own_wrs wrsP wrs }}}. Admitted. - Theorem wp_KeyToGroup (key : string) : + Theorem wp_KeyToGroup (key : byte_string) : {{{ True }}} KeyToGroup #(LitString key) {{{ (gid : u64), RET #gid; ⌜key_to_group key = gid⌝ }}}. @@ -181,7 +181,7 @@ Section program. (*@ } @*) Admitted. - Theorem wp_Txn__getwrs (txn : loc) (key : string) wrs : + Theorem wp_Txn__getwrs (txn : loc) (key : byte_string) wrs : {{{ own_txn_wrs txn wrs }}} Txn__getwrs #txn #(LitString key) {{{ (v : dbval) (ok : bool), RET (dbval_to_val v, #ok); @@ -235,7 +235,7 @@ Section program. by destruct Hv. Qed. - Theorem wp_Txn__setwrs (txn : loc) (key : string) (value : dbval) wrs : + Theorem wp_Txn__setwrs (txn : loc) (key : byte_string) (value : dbval) wrs : {{{ own_txn_wrs txn wrs }}} Txn__setwrs #txn #(LitString key) (dbval_to_val value) {{{ RET #(); own_txn_wrs txn (<[key := value]> wrs) }}}. diff --git a/src/program_proof/rsm/distx/program/txnlog.v b/src/program_proof/rsm/distx/program/txnlog.v index 8f87de407..a3ed86745 100644 --- a/src/program_proof/rsm/distx/program/txnlog.v +++ b/src/program_proof/rsm/distx/program/txnlog.v @@ -101,7 +101,7 @@ Section program. Admitted. Theorem wp_TxnLog__SubmitRead - (log : loc) (ts : u64) (key : string) (gid : groupid) γ : + (log : loc) (ts : u64) (key : byte_string) (gid : groupid) γ : is_txnlog log gid γ -∗ {{{ True }}} <<< ∀∀ vs, cpool_half γ gid vs >>> diff --git a/src/program_proof/rsm/fpaxos_inv.v b/src/program_proof/rsm/fpaxos_inv.v index 931c9c6a7..25cf52a36 100644 --- a/src/program_proof/rsm/fpaxos_inv.v +++ b/src/program_proof/rsm/fpaxos_inv.v @@ -147,7 +147,7 @@ Section pure. let ps := fmap (latest_before n) bsq in map_fold latest_before_quorum_step O ps. - Definition is_fast (l : ballot) (n : nat) (v : string) := + Definition is_fast (l : ballot) (n : nat) (v : byte_string) := l !! n = Some (FAccept v). #[local] @@ -155,10 +155,10 @@ Section pure. Decision (is_fast l n v). Proof. unfold is_fast. apply _. Qed. - Definition nfast (bsq : gmap A ballot) (n : nat) (v : string) := + Definition nfast (bsq : gmap A ballot) (n : nat) (v : byte_string) := size (filter (λ x : A * ballot, is_fast x.2 n v) bsq). - Definition nfastneg (bsq : gmap A ballot) (n : nat) (v : string) := + Definition nfastneg (bsq : gmap A ballot) (n : nat) (v : byte_string) := size (filter (λ x : A * ballot, not (is_fast x.2 n v)) bsq). Definition equal_max_occurrence (bsq : gmap A ballot) n v := diff --git a/src/program_proof/rsm/fpaxos_top.v b/src/program_proof/rsm/fpaxos_top.v index 6cc701069..2aeb0a52b 100644 --- a/src/program_proof/rsm/fpaxos_top.v +++ b/src/program_proof/rsm/fpaxos_top.v @@ -3,15 +3,15 @@ *) From Perennial.program_proof Require Export grove_prelude. -Inductive proposal : Set := +Inductive proposal : Type := | Any -| Proposed (v : string). +| Proposed (v : byte_string). Definition proposals := gmap nat proposal. -Inductive vote : Set := +Inductive vote : Type := | Reject | CAccept -| FAccept (v : string). +| FAccept (v : byte_string). Definition ballot := list vote. #[global] @@ -19,8 +19,8 @@ Instance vote_eq_decision : EqDecision vote. Proof. solve_decision. Qed. -Inductive consensus : Set := -| Chosen (v : string) +Inductive consensus : Type := +| Chosen (v : byte_string) | Free. Definition prefixes `{Countable A} {B : Type} (lbs ls : gmap A (list B)) := diff --git a/src/program_proof/rsm/spaxos_examples.v b/src/program_proof/rsm/spaxos_examples.v index ae25abc36..bae24c882 100644 --- a/src/program_proof/rsm/spaxos_examples.v +++ b/src/program_proof/rsm/spaxos_examples.v @@ -3,7 +3,7 @@ From Perennial.program_proof.rsm Require Import spaxos_prelude spaxos_propose. Section prog. Context `{!heapGS Σ, !spaxos_ghostG Σ}. - Definition of_length_five s := String.length s = 5%nat. + Definition of_length_five (s : byte_string) := length s = 5%nat. Definition length_of_consensus v := match v with @@ -11,7 +11,7 @@ Section prog. | _ => True end. - Definition length_of_candidates (vs : gset string) := + Definition length_of_candidates (vs : gset byte_string) := set_Forall of_length_five vs. Definition inv_example1 γ : iProp Σ := diff --git a/src/program_proof/rsm/spaxos_ghost.v b/src/program_proof/rsm/spaxos_ghost.v index 0f13c5c01..837b10c3f 100644 --- a/src/program_proof/rsm/spaxos_ghost.v +++ b/src/program_proof/rsm/spaxos_ghost.v @@ -24,10 +24,10 @@ Section consensus. Definition is_chosen_consensus γ v : iProp Σ := own_consensus_half γ (Chosen v). - Definition own_candidates γ (vs : gset string) : iProp Σ. + Definition own_candidates γ (vs : gset byte_string) : iProp Σ. Admitted. - Definition own_candidates_half γ (vs : gset string) : iProp Σ. + Definition own_candidates_half γ (vs : gset byte_string) : iProp Σ. Admitted. (* Type class instances. *) @@ -138,10 +138,10 @@ Section proposal. Implicit Type (γ : spaxos_names). (* Definitions. *) - Definition is_proposal γ (n : nat) (v : string) : iProp Σ. + Definition is_proposal γ (n : nat) (v : byte_string) : iProp Σ. Admitted. - Definition own_proposals γ (ps : gmap nat string) : iProp Σ. + Definition own_proposals γ (ps : gmap nat byte_string) : iProp Σ. Admitted. (* Type class instances. *) diff --git a/src/program_proof/rsm/spaxos_inv.v b/src/program_proof/rsm/spaxos_inv.v index 43d70a6c5..5b5b334b3 100644 --- a/src/program_proof/rsm/spaxos_inv.v +++ b/src/program_proof/rsm/spaxos_inv.v @@ -519,7 +519,7 @@ Section pure. Definition spaxos_prepare (bs : gmap A ballot) (x : A) (n : nat) := alter (λ l, extend false n l) x bs. - Definition spaxos_propose (ps : proposals) (n : nat) (v : string) := + Definition spaxos_propose (ps : proposals) (n : nat) (v : byte_string) := <[n := v]> ps. Definition spaxos_advance (ts : gmap A nat) (x : A) (n : nat) := diff --git a/src/program_proof/rsm/spaxos_propose.v b/src/program_proof/rsm/spaxos_propose.v index d9cc68fe7..f5bc70db4 100644 --- a/src/program_proof/rsm/spaxos_propose.v +++ b/src/program_proof/rsm/spaxos_propose.v @@ -28,7 +28,7 @@ Qed. Definition consented_impl_committed (v c : consensus) := if v then c = v else True. -Definition proposals_incl_candidates (vs : gset string) (ps : gmap nat string) := +Definition proposals_incl_candidates (vs : gset byte_string) (ps : gmap nat byte_string) := map_img ps ⊆ vs. Definition spaxos_inv sc γ : iProp Σ := @@ -67,7 +67,7 @@ Instance is_proposal_nz_persistent γ n v : Persistent (is_proposal_nz γ n v). Proof. unfold is_proposal_nz. case_decide; apply _. Qed. -Definition is_chosen_commitment_learned γ (l : bool) (v : string) : iProp Σ := +Definition is_chosen_commitment_learned γ (l : bool) (v : byte_string) : iProp Σ := (if l then is_chosen_commitment γ v else True)%I. #[global] @@ -106,7 +106,7 @@ Context `{!heapGS Σ, !spaxos_ghostG Σ}. (*@ peers map[uint64]*Paxos @*) (*@ } @*) Definition own_paxos (paxos : loc) (nid : u64) γ : iProp Σ := - ∃ (termc termp : u64) (decreep : string) (learned : bool) (blt : ballot), + ∃ (termc termp : u64) (decreep : byte_string) (learned : bool) (blt : ballot), "Htermc" ∷ paxos ↦[Paxos :: "termc"] #termc ∗ "%Hnz" ∷ ⌜uint.nat termc ≠ O⌝ ∗ "Htermp" ∷ paxos ↦[Paxos :: "termp"] #termp ∗ @@ -244,7 +244,7 @@ Theorem wp_Paxos__outcome (px : loc) nid sc γ : {{{ True }}} <<< ∀∀ c, own_consensus_half γ c >>> Paxos__outcome #px @ ↑spaxosN - <<< ∃∃ (v : string) (ok : bool), own_consensus_half γ (if ok then Chosen v else c) >>> + <<< ∃∃ (v : byte_string) (ok : bool), own_consensus_half γ (if ok then Chosen v else c) >>> {{{ RET (#(LitString v), #ok); True }}}. Proof. iIntros "#Hnode" (Φ) "!> _ HAU". @@ -294,7 +294,7 @@ Proof. iDestruct (proposal_lookup with "Hproposed Hps") as %Hin. iMod (consensus_update decreep with "Hv Hvs") as "[Hv Hvs]". { unfold proposals_incl_candidates in Hpic. - apply (elem_of_map_img_2 (SA:=gset string)) in Hin. + apply (elem_of_map_img_2 (SA:=gset byte_string)) in Hin. set_solver. } iDestruct (consensus_split with "Hv") as "[Hv Hv']". @@ -308,7 +308,7 @@ Theorem wp_Paxos__Outcome (px : loc) nid sc γ : {{{ True }}} <<< ∀∀ c, own_consensus_half γ c >>> Paxos__Outcome #px @ ↑spaxosN - <<< ∃∃ (v : string) (ok : bool), own_consensus_half γ (if ok then Chosen v else c) >>> + <<< ∃∃ (v : byte_string) (ok : bool), own_consensus_half γ (if ok then Chosen v else c) >>> {{{ RET (#(LitString v), #ok); True }}}. Proof. iIntros "#Hpaxos" (Φ) "!> _ HAU". @@ -329,7 +329,7 @@ Proof. by iApply "HΦ". Qed. -Definition node_prepared (term termp : u64) (decree : string) nid γ : iProp Σ := +Definition node_prepared (term termp : u64) (decree : byte_string) nid γ : iProp Σ := ∃ (l : ballot), "#Hlb" ∷ is_ballot_lb γ nid l ∗ "#Hdecree" ∷ is_proposal_nz γ (uint.nat termp) decree ∗ @@ -340,7 +340,7 @@ Theorem wp_Paxos__prepare (px : loc) (term : u64) nid sc γ : is_paxos_node px nid sc γ -∗ {{{ True }}} Paxos__prepare #px #term - {{{ (termp : u64) (decree : string) (ok : bool), RET (#termp, #(LitString decree), #ok); + {{{ (termp : u64) (decree : byte_string) (ok : bool), RET (#termp, #(LitString decree), #ok); if ok then node_prepared term termp decree nid γ else True }}}. Proof. @@ -435,7 +435,7 @@ Theorem wp_Paxos__advance (px : loc) nid sc γ : is_paxos_node px nid sc γ -∗ {{{ True }}} Paxos__advance #px - {{{ (term : u64) (termp : u64) (decree : string), RET (#term, #termp, #(LitString decree)); + {{{ (term : u64) (termp : u64) (decree : byte_string), RET (#term, #termp, #(LitString decree)); node_prepared term termp decree nid γ ∗ ⌜is_term_of_node nid (uint.nat term) ∧ uint.nat term ≠ O⌝ }}}. Proof. @@ -520,12 +520,12 @@ Proof. apply latest_term_extend_false. Qed. -Definition node_accepted (term : u64) (decree : string) nid γ : iProp Σ := +Definition node_accepted (term : u64) (decree : byte_string) nid γ : iProp Σ := ∃ (l : ballot), "#Hlb" ∷ is_ballot_lb γ nid l ∗ "%Haccin" ∷ ⌜accepted_in l (uint.nat term)⌝. -Theorem wp_Paxos__accept (px : loc) (term : u64) (decree : string) nid sc γ : +Theorem wp_Paxos__accept (px : loc) (term : u64) (decree : byte_string) nid sc γ : is_proposal γ (uint.nat term) decree -∗ is_paxos_node px nid sc γ -∗ {{{ True }}} @@ -647,7 +647,7 @@ Qed. Definition reached_quorum (sc n : nat) := sc / 2 < n. Definition quorum_prepared - (term : u64) (terml : u64) (decreel : string) (sc : nat) (γ : spaxos_names) : iProp Σ := + (term : u64) (terml : u64) (decreel : byte_string) (sc : nat) (γ : spaxos_names) : iProp Σ := ∃ (bsqlb : gmap u64 ballot), "#Hlbs" ∷ ([∗ map] x ↦ l ∈ bsqlb, is_ballot_lb γ x l) ∗ "#Hproposal" ∷ is_proposal_nz γ (uint.nat terml) decreel ∗ @@ -661,8 +661,8 @@ Instance quorum_prepared_persistent term terml decree sc γ : Proof. apply _. Qed. Theorem wp_Paxos__accept__proposer - {px : loc} {term : u64} {decree : string} - (v : string) (terml : u64) decreel nid sc γ : + {px : loc} {term : u64} {decree : byte_string} + (v : byte_string) (terml : u64) decreel nid sc γ : is_term_of_node nid (uint.nat term) -> decree = (if decide (uint.nat terml = O) then v else decreel) -> (* (if decide (uint.nat terml = O) then True else decree = decreel) -> *) @@ -851,11 +851,11 @@ Proof. - (* Case: Adding [v] to [ps]. *) etransitivity; [apply map_img_insert_subseteq | set_solver]. - (* Case: Adding [decreel] to [ps]. *) - transitivity (map_img (SA:=gset string) ps); last by set_solver. + transitivity (map_img (SA:=gset byte_string) ps); last by set_solver. specialize (Hterml H). clear -Hterml. etransitivity; first apply map_img_insert_subseteq. - apply (elem_of_map_img_2 (SA:=gset string)) in Hterml. + apply (elem_of_map_img_2 (SA:=gset byte_string)) in Hterml. set_solver. } iMod ("HinvC" with "[Hv Hvs Hc Hbs Hps Hts]") as "_"; first by eauto 10 with iFrame. @@ -941,12 +941,12 @@ Lemma ite_apply (A B : Type) (b : bool) (f : A -> B) x y : (if b then f x else f y) = f (if b then x else y). Proof. destruct b; done. Qed. -Theorem wp_Paxos__prepareAll (px : loc) (term terma : u64) (decreea : string) nid sc γ : +Theorem wp_Paxos__prepareAll (px : loc) (term terma : u64) (decreea : byte_string) nid sc γ : node_prepared term terma decreea nid γ -∗ is_paxos_comm px nid sc γ -∗ {{{ True }}} Paxos__prepareAll #px #term #terma #(LitString decreea) - {{{ (termp : u64) (decree : string) (ok : bool), RET (#termp, #(LitString decree), #ok); + {{{ (termp : u64) (decree : byte_string) (ok : bool), RET (#termp, #(LitString decree), #ok); if ok then quorum_prepared term termp decree sc γ else True }}}. Proof. @@ -983,7 +983,7 @@ Proof. wp_loadField. iMod (readonly_load with "HpeersMR") as (q) "HpeersM". set P := (λ (m : gmap u64 loc), - ∃ (terml : u64) (decreel : string) (n : u64) (bsqlb : gmap u64 ballot), + ∃ (terml : u64) (decreel : byte_string) (n : u64) (bsqlb : gmap u64 ballot), "HtermlRef" ∷ termlRef ↦[uint64T] #terml ∗ "HdecreelRef" ∷ decreelRef ↦[stringT] #(str decreel) ∗ "HnRef" ∷ nRef ↦[uint64T] #n ∗ @@ -1121,7 +1121,7 @@ Instance quorum_accepted_persistent term sc γ : Persistent (quorum_accepted γ term sc). Proof. apply _. Qed. -Theorem wp_Paxos__acceptAll (px : loc) (term : u64) (decree : string) nid sc γ : +Theorem wp_Paxos__acceptAll (px : loc) (term : u64) (decree : byte_string) nid sc γ : node_accepted term decree nid γ -∗ is_proposal γ (uint.nat term) decree -∗ is_paxos_comm px nid sc γ -∗ @@ -1232,7 +1232,7 @@ Proof. by iFrame "∗ # %". Qed. -Theorem wp_Paxos__learn (px : loc) (term : u64) (decree : string) nid sc γ : +Theorem wp_Paxos__learn (px : loc) (term : u64) (decree : byte_string) nid sc γ : is_proposal γ (uint.nat term) decree -∗ is_chosen_commitment γ decree -∗ is_paxos_node px nid sc γ -∗ @@ -1330,7 +1330,7 @@ Proof. by iApply "HΦ". Qed. -Theorem wp_Paxos__learnAll (px : loc) (term : u64) (decree : string) nid sc γ : +Theorem wp_Paxos__learnAll (px : loc) (term : u64) (decree : byte_string) nid sc γ : is_proposal γ (uint.nat term) decree -∗ is_chosen_commitment γ decree -∗ is_paxos_comm px nid sc γ -∗ @@ -1367,7 +1367,7 @@ End temp. Section prog. Context `{!heapGS Σ, !spaxos_ghostG Σ}. -Theorem wp_Paxos__Propose (px : loc) (v : string) nid sc γ : +Theorem wp_Paxos__Propose (px : loc) (v : byte_string) nid sc γ : is_paxos px nid sc γ -∗ {{{ True }}} <<< ∀∀ vs, own_candidates_half γ vs >>> diff --git a/src/program_proof/rsm/spaxos_top.v b/src/program_proof/rsm/spaxos_top.v index 1ca0b5db0..1603b427d 100644 --- a/src/program_proof/rsm/spaxos_top.v +++ b/src/program_proof/rsm/spaxos_top.v @@ -4,10 +4,10 @@ From Perennial.program_proof Require Export grove_prelude. From Perennial.program_logic Require Export atomic. (* prefer the ncfupd atomics *) -Definition proposals := gmap nat string. +Definition proposals := gmap nat byte_string. Definition ballot := list bool. -Inductive consensus : Set := -| Chosen (v : string) +Inductive consensus : Type := +| Chosen (v : byte_string) | Free. Definition prefixes `{Countable A} {B : Type} (lbs ls : gmap A (list B)) := diff --git a/src/program_proof/tulip/base.v b/src/program_proof/tulip/base.v index 56539bfdd..d31363d8a 100644 --- a/src/program_proof/tulip/base.v +++ b/src/program_proof/tulip/base.v @@ -6,8 +6,8 @@ From Perennial.Helpers Require finite. Local Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations. -Definition dbkey := string. -Definition dbval := option string. +Definition dbkey := byte_string. +Definition dbval := option byte_string. Definition dbhist := list dbval. Definition dbtpl := (dbhist * nat)%type. Definition dbmod := (dbkey * dbval)%type. @@ -22,14 +22,14 @@ Inductive txnres := | ResCommitted (wrs : dbmap) | ResAborted. -Definition fstring := {k : string | String.length k < 2 ^ 64}. +Definition fstring := {k : byte_string | (length k < (Z.to_nat (2 ^ 64)%Z))%nat }. #[local] Instance fstring_finite : finite.Finite fstring. -Proof. apply Helpers.finite.string_finite_Zlt_length. Qed. +Proof. apply Helpers.finite.list_finite_lt_length. Qed. -Definition keys_all : gset string := +Definition keys_all : gset byte_string := list_to_set (map proj1_sig (finite.enum fstring)). (** Transaction status on group/replica. *) @@ -163,7 +163,7 @@ Definition dblog := list ccommand. (** Converting keys to group IDs. *) Definition key_to_group (key : dbkey) : u64 := - String.length key `mod` size gids_all. + length key `mod` size gids_all. (** Participant groups. *) Definition ptgroups (keys : gset dbkey) : gset u64 := @@ -295,12 +295,13 @@ Definition valid_key (key : dbkey) := key ∈ keys_all. Lemma valid_key_length key : valid_key key -> - String.length key < 2 ^ 64. + length key < 2 ^ 64. Proof. intros Hvk. rewrite /valid_key /keys_all in Hvk. apply elem_of_list_to_set, elem_of_list_fmap_2 in Hvk. - by destruct Hvk as ([k Hk] & -> & _). + destruct Hvk as ([k Hk] & -> & _). + simpl. lia. Qed. Definition valid_ccommand gid (c : ccommand) := diff --git a/src/program_proof/tulip/encode.v b/src/program_proof/tulip/encode.v index 358760405..f247b87fb 100644 --- a/src/program_proof/tulip/encode.v +++ b/src/program_proof/tulip/encode.v @@ -1,80 +1,14 @@ From Perennial.program_proof Require Import grove_prelude. From Perennial.program_proof.tulip Require Import base. -(* TODO: this really should be made general. *) - -Definition encode_string (x : string) : list u8 := - let bs := string_to_bytes x in - u64_le (U64 (length bs)) ++ bs. - -Opaque encode_string. - -Definition encode_strings_step (bs : list u8) (x : string) : list u8 := - bs ++ encode_string x. - -Definition encode_strings_xlen (xs : list string) : list u8 := - foldl encode_strings_step [] xs. - -Definition encode_strings (xs : list string) : list u8 := - u64_le (U64 (length xs)) ++ encode_strings_xlen xs. - -Lemma encode_strings_xlen_snoc xs x : - encode_strings_xlen (xs ++ [x]) = encode_strings_xlen xs ++ encode_string x. -Proof. - by rewrite /encode_strings_xlen foldl_snoc /encode_strings_step. -Qed. - -Lemma foldl_encode_strings_step_app (bs : list u8) (xs : list string) : - foldl encode_strings_step bs xs = bs ++ foldl encode_strings_step [] xs. -Proof. - generalize dependent bs. - induction xs as [| x xs IH]; intros bs. - { by rewrite /= app_nil_r. } - rewrite /= (IH (encode_strings_step bs x)) (IH (encode_strings_step [] x)). - rewrite {1 3}/encode_strings_step. - by rewrite app_nil_l app_assoc. -Qed. - -Lemma encode_strings_xlen_cons xs x : - encode_strings_xlen (x :: xs) = encode_string x ++ encode_strings_xlen xs. -Proof. - rewrite /encode_strings_xlen /= foldl_encode_strings_step_app. - by rewrite {1}/encode_strings_step app_nil_l. -Qed. - -Lemma encode_strings_xlen_length_inv xs n : - (length (encode_strings_xlen xs) ≤ n)%nat -> - (length xs ≤ n)%nat. -Proof. - generalize dependent n. - induction xs as [| x xs IH]; intros n; first done. - rewrite encode_strings_xlen_cons length_app /=. - assert (length (encode_string x) ≠ O). - { by destruct (nil_or_length_pos (encode_string x)). } - intros Hlen. - assert (Hlenxs : (length xs ≤ pred n)%nat). - { apply IH. lia. } - lia. -Qed. - -Lemma encode_strings_length_inv xs n : - (length (encode_strings xs) ≤ n)%nat -> - (length xs ≤ n)%nat. -Proof. - rewrite /encode_strings length_app. - intros Hn. - pose proof (encode_strings_xlen_length_inv xs n) as Hlen. - lia. -Qed. - Definition encode_dbval (x : dbval) : list u8 := match x with - | Some v => [U8 1] ++ encode_string v + | Some v => [U8 1] ++ v | None => [U8 0] end. Definition encode_dbmod (x : dbmod) : list u8 := - encode_string x.1 ++ encode_dbval x.2. + x.1 ++ encode_dbval x.2. Definition encode_dbmods_step (bs : list u8) (x : dbmod) : list u8 := bs ++ encode_dbmod x. @@ -117,7 +51,7 @@ Proof. induction xs as [| x xs IH]; intros n; first done. rewrite encode_dbmods_xlen_cons length_app /=. assert (length (encode_dbmod x) ≠ O). - { by destruct (nil_or_length_pos (encode_dbmod x)). } + { by destruct x as [[] []]. } intros Hlen. assert (Hlenxs : (length xs ≤ pred n)%nat). { apply IH. lia. } diff --git a/src/program_proof/tulip/inv.v b/src/program_proof/tulip/inv.v index 2744cf667..e0899972a 100644 --- a/src/program_proof/tulip/inv.v +++ b/src/program_proof/tulip/inv.v @@ -193,7 +193,7 @@ Section inv_network. Proof. destruct req; apply _. Defined. Definition safe_read_resp - γ (ts rid : u64) (key : string) (ver : dbpver) (slow : bool) : iProp Σ := + γ (ts rid : u64) (key : byte_string) (ver : dbpver) (slow : bool) : iProp Σ := "#Hsafe" ∷ fast_or_slow_read γ rid key (uint.nat ver.1) (uint.nat ts) ver.2 slow ∗ "%Hrid" ∷ ⌜rid ∈ rids_all⌝. diff --git a/src/program_proof/tulip/inv_txnlog.v b/src/program_proof/tulip/inv_txnlog.v index 5bdf2173d..2f6e374dc 100644 --- a/src/program_proof/tulip/inv_txnlog.v +++ b/src/program_proof/tulip/inv_txnlog.v @@ -14,10 +14,10 @@ Definition encode_commit_cmd (ts : nat) (m : dbmap) (data : list u8) := Definition encode_abort_cmd (ts : nat) (data : list u8) := data = u64_le (U64 0) ++ u64_le (W64 ts). -Definition encode_ccommand (ccmd : ccommand) (s : string) := +Definition encode_ccommand (ccmd : ccommand) (s : byte_string) := match ccmd with - | CmdCommit ts pwrs => encode_commit_cmd ts pwrs (string_to_bytes s) - | CmdAbort ts => encode_abort_cmd ts (string_to_bytes s) + | CmdCommit ts pwrs => encode_commit_cmd ts pwrs s + | CmdAbort ts => encode_abort_cmd ts s end. Section inv_txnlog. diff --git a/src/program_proof/tulip/msg.v b/src/program_proof/tulip/msg.v index fff469e05..a25ad8f17 100644 --- a/src/program_proof/tulip/msg.v +++ b/src/program_proof/tulip/msg.v @@ -2,7 +2,7 @@ From Perennial.program_proof Require Import grove_prelude. From Perennial.program_proof.tulip Require Import base encode. Inductive txnreq := -| ReadReq (ts : u64) (key : string) +| ReadReq (ts : u64) (key : byte_string) | FastPrepareReq (ts : u64) (pwrs : dbmap) | ValidateReq (ts : u64) (rank : u64) (pwrs : dbmap) | PrepareReq (ts : u64) (rank : u64) @@ -57,10 +57,10 @@ Proof. intros [| | | | | | | |] => //=. Qed. -Definition encode_read_req_xkind (ts : u64) (key : string) := - u64_le ts ++ encode_string key. +Definition encode_read_req_xkind (ts : u64) (key : byte_string) := + u64_le ts ++ key. -Definition encode_read_req (ts : u64) (key : string) (data : list u8) := +Definition encode_read_req (ts : u64) (key : byte_string) (data : list u8) := data = u64_le (U64 100) ++ encode_read_req_xkind ts key. Definition encode_fast_prepare_req_xkind (ts : u64) (m : dbmap) (data : list u8) := @@ -162,7 +162,7 @@ Instance rpres_to_u64_inj : Proof. intros x y H. by destruct x, y. Defined. Inductive txnresp := -| ReadResp (ts : u64) (rid : u64) (key : string) (ver : dbpver) (slow : bool) +| ReadResp (ts : u64) (rid : u64) (key : byte_string) (ver : dbpver) (slow : bool) | FastPrepareResp (ts : u64) (rid : u64) (res : rpres) | ValidateResp (ts : u64) (rid : u64) (res : rpres) | PrepareResp (ts : u64) (rank : u64) (rid : u64) (res : rpres) @@ -214,12 +214,12 @@ Proof. Qed. Definition encode_read_resp_xkind - (ts rid : u64) (key : string) (ver : dbpver) (slow : bool) := - u64_le ts ++ u64_le rid ++ encode_string key ++ + (ts rid : u64) (key : byte_string) (ver : dbpver) (slow : bool) := + u64_le ts ++ u64_le rid ++ key ++ encode_dbpver ver ++ [if slow then U8 1 else U8 0]. Definition encode_read_resp - (ts rid : u64) (key : string) (ver : dbpver) (slow : bool) := + (ts rid : u64) (key : byte_string) (ver : dbpver) (slow : bool) := u64_le (U64 100) ++ encode_read_resp_xkind ts rid key ver slow. Definition encode_ts_rid_res (ts rid : u64) (res : rpres) := diff --git a/src/program_proof/tulip/paxos/base.v b/src/program_proof/tulip/paxos/base.v index eb447a9a0..75a2dff82 100644 --- a/src/program_proof/tulip/paxos/base.v +++ b/src/program_proof/tulip/paxos/base.v @@ -4,7 +4,7 @@ From Perennial.base_logic Require Import ghost_map mono_nat saved_prop. From Perennial.program_proof Require Import grove_prelude. From Perennial.program_proof.rsm.pure Require Import quorum. -Definition ledger := list string. +Definition ledger := list byte_string. Definition proposals := gmap nat ledger. @@ -380,8 +380,8 @@ Inductive pxcmd := | CmdPaxosAccept (lsn : nat) (ents : ledger) | CmdPaxosExpand (lsn : nat). -Definition stringO := leibnizO string. -Definition stringmlR := mono_listR stringO. +Definition byte_stringO := listO w8. +Definition byte_stringmlR := mono_listR byte_stringO. Definition lsnmR := gmapR nat (dfrac_agreeR natO). Canonical Structure nodedecO := leibnizO nodedec. Definition declistR := mono_listR nodedecO. @@ -393,11 +393,11 @@ Definition node_natmR := gmapR u64 (dfrac_agreeR natO). Definition node_ledgerR := gmapR u64 (dfrac_agreeR ledgerO). Definition pxcmdlO := leibnizO (list pxcmd). Definition node_pxcmdlR := gmapR u64 (dfrac_agreeR pxcmdlO). -Definition node_stringR := gmapR u64 (agreeR stringO). +Definition node_stringR := gmapR u64 (agreeR byte_stringO). Class paxos_ghostG (Σ : gFunctors) := - { #[global] stringmlG :: inG Σ stringmlR; - #[global] cpoolG :: ghost_mapG Σ string unit; + { #[global] byte_stringmlG :: inG Σ byte_stringmlR; + #[global] cpoolG :: ghost_mapG Σ byte_string unit; #[global] proposalG :: ghost_mapG Σ nat gname; #[global] base_proposalG :: ghost_mapG Σ nat ledger; #[global] prepare_lsnG :: inG Σ lsnmR; @@ -414,9 +414,9 @@ Class paxos_ghostG (Σ : gFunctors) := Definition paxos_ghostΣ := #[ GFunctor lsnmR; - ghost_mapΣ string unit; + ghost_mapΣ byte_string unit; ghost_mapΣ nat gname; - GFunctor stringmlR; + GFunctor byte_stringmlR; ghost_mapΣ nat ledger; GFunctor node_declistR; GFunctor node_proposalmR; diff --git a/src/program_proof/tulip/paxos/inv.v b/src/program_proof/tulip/paxos/inv.v index c2a56b3ff..9a4958834 100644 --- a/src/program_proof/tulip/paxos/inv.v +++ b/src/program_proof/tulip/paxos/inv.v @@ -520,7 +520,7 @@ Section inv_file. Definition paxosfileNS := paxosNS .@ "file". Definition node_file_inv (γ : paxos_names) (nid : u64) : iProp Σ := - ∃ (wal : list pxcmd) (fname : string) (content : list u8), + ∃ (wal : list pxcmd) (fname : byte_string) (content : list u8), "Hwalfile" ∷ own_node_wal_half γ nid wal ∗ "Hfile" ∷ fname f↦ content ∗ "#Hwalfname" ∷ is_node_wal_fname γ nid fname ∗ @@ -548,8 +548,8 @@ Section inv_network. is_prepare_lsn γ (uint.nat term) (uint.nat lsnlc). Definition safe_append_entries_req - γ nids (term lsnlc lsne : u64) (ents : list string) : iProp Σ := - ∃ (logleader logcmt : list string), + γ nids (term lsnlc lsne : u64) (ents : list byte_string) : iProp Σ := + ∃ (logleader logcmt : list byte_string), "#Hpfb" ∷ prefix_base_ledger γ (uint.nat term) logleader ∗ "#Hpfg" ∷ prefix_growing_ledger γ (uint.nat term) logleader ∗ "#Hlogcmt" ∷ safe_ledger_above γ nids (uint.nat term) logcmt ∗ @@ -575,8 +575,8 @@ Section inv_network. Proof. destruct req; apply _. Defined. Definition safe_request_vote_resp - γ (nids : gset u64) (nid term terme : u64) (ents : list string) : iProp Σ := - ∃ (logpeer : list string) (lsne : u64), + γ (nids : gset u64) (nid term terme : u64) (ents : list byte_string) : iProp Σ := + ∃ (logpeer : list byte_string) (lsne : u64), "#Hpromise" ∷ past_nodedecs_latest_before γ nid (uint.nat term) (uint.nat terme) logpeer ∗ "#Hlsne" ∷ is_prepare_lsn γ (uint.nat term) (uint.nat lsne) ∗ "%Hents" ∷ ⌜drop (uint.nat lsne) logpeer = ents⌝ ∗ @@ -584,7 +584,7 @@ Section inv_network. Definition safe_append_entries_resp γ (nids : gset u64) (nid term lsneq : u64) : iProp Σ := - ∃ (logacpt : list string), + ∃ (logacpt : list byte_string), "#Haoc" ∷ (is_accepted_proposal_lb γ nid (uint.nat term) logacpt ∨ safe_ledger_above γ nids (uint.nat term) logacpt) ∗ "%Hlogacpt" ∷ ⌜length logacpt = uint.nat lsneq⌝ ∗ @@ -1195,7 +1195,7 @@ End lemma. Section alloc. Context `{!heapGS Σ, !paxos_ghostG Σ}. - Lemma paxos_inv_alloc addrm (fnames : gmap u64 string) : + Lemma paxos_inv_alloc addrm (fnames : gmap u64 byte_string) : let nids := dom addrm in (1 < size addrm)%nat -> dom fnames = dom addrm -> diff --git a/src/program_proof/tulip/paxos/msg.v b/src/program_proof/tulip/paxos/msg.v index 77630f372..33f713340 100644 --- a/src/program_proof/tulip/paxos/msg.v +++ b/src/program_proof/tulip/paxos/msg.v @@ -4,7 +4,7 @@ From Perennial.program_proof.tulip Require Import encode. Inductive pxreq := | RequestVoteReq (term : u64) (lsnlc : u64) -| AppendEntriesReq (term : u64) (lsnlc : u64) (lsne : u64) (ents : list string). +| AppendEntriesReq (term : u64) (lsnlc : u64) (lsne : u64) (ents : list byte_string). #[global] Instance pxreq_eq_decision : @@ -35,11 +35,11 @@ Definition encode_request_vote_req (term lsnlc : u64) := u64_le (U64 0) ++ encode_request_vote_req_xkind term lsnlc. Definition encode_append_entries_req_xkind - (term lsnlc lsne : u64) (ents : list string) := - u64_le term ++ u64_le lsnlc ++ u64_le lsne ++ encode_strings ents. + (term lsnlc lsne : u64) (ents : list byte_string) := + u64_le term ++ u64_le lsnlc ++ u64_le lsne ++ concat ents. Definition encode_append_entries_req - (term lsnlc lsne : u64) (ents : list string) := + (term lsnlc lsne : u64) (ents : list byte_string) := u64_le (U64 1) ++ encode_append_entries_req_xkind term lsnlc lsne ents. Definition encode_pxreq (req : pxreq) : list u8 := @@ -51,7 +51,7 @@ Definition encode_pxreq (req : pxreq) : list u8 := end. Inductive pxresp := -| RequestVoteResp (nid term terme : u64) (ents : list string) +| RequestVoteResp (nid term terme : u64) (ents : list byte_string) | AppendEntriesResp (nid term lsneq : u64). #[global] @@ -77,11 +77,11 @@ Proof. Qed. Definition encode_request_vote_resp_xkind - (nid term terme : u64) (ents : list string) := - u64_le nid ++ u64_le term ++ u64_le terme ++ encode_strings ents. + (nid term terme : u64) (ents : list byte_string) := + u64_le nid ++ u64_le term ++ u64_le terme ++ concat ents. Definition encode_request_vote_resp - (nid term terme : u64) (ents : list string) := + (nid term terme : u64) (ents : list byte_string) := u64_le (U64 0) ++ encode_request_vote_resp_xkind nid term terme ents. Definition encode_append_entries_resp_xkind (nid term lsneq : u64) := diff --git a/src/program_proof/tulip/paxos/program/encode_accept_request.v b/src/program_proof/tulip/paxos/program/encode_accept_request.v index 1fcf76c67..0a88db760 100644 --- a/src/program_proof/tulip/paxos/program/encode_accept_request.v +++ b/src/program_proof/tulip/paxos/program/encode_accept_request.v @@ -8,7 +8,7 @@ Section encode_accept_request. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_EncodeAcceptRequest - (term lsnc lsne : u64) (entsP : Slice.t) (ents : list string) : + (term lsnc lsne : u64) (entsP : Slice.t) (ents : list byte_string) : {{{ own_slice entsP stringT (DfracOwn 1) ents }}} EncodeAcceptRequest #term #lsnc #lsne (to_val entsP) {{{ (dataP : Slice.t) (data : list u8), RET (to_val dataP); diff --git a/src/program_proof/tulip/paxos/program/encode_prepare_response.v b/src/program_proof/tulip/paxos/program/encode_prepare_response.v index ec266cee6..1bc871f2b 100644 --- a/src/program_proof/tulip/paxos/program/encode_prepare_response.v +++ b/src/program_proof/tulip/paxos/program/encode_prepare_response.v @@ -8,7 +8,7 @@ Section encode_prepare_response. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_EncodePrepareResponse - (nid term terma : u64) (entsP : Slice.t) (ents : list string) : + (nid term terma : u64) (entsP : Slice.t) (ents : list byte_string) : {{{ own_slice entsP stringT (DfracOwn 1) ents }}} EncodePrepareResponse #nid #term #terma (to_val entsP) {{{ (dataP : Slice.t) (data : list u8), RET (to_val dataP); diff --git a/src/program_proof/tulip/paxos/program/mk_paxos.v b/src/program_proof/tulip/paxos/program/mk_paxos.v index 7332c8344..9e7a242c9 100644 --- a/src/program_proof/tulip/paxos/program/mk_paxos.v +++ b/src/program_proof/tulip/paxos/program/mk_paxos.v @@ -7,7 +7,7 @@ Section mk_paxos. Theorem wp_mkPaxos (nidme : u64) (termc : u64) (terml : u64) (lsnc : u64) - (logP : Slice.t) (log : list string) (addrmP : loc) (addrm : gmap u64 chan) (fname : string) γ : + (logP : Slice.t) (log : list byte_string) (addrmP : loc) (addrm : gmap u64 chan) (fname : byte_string) γ : (1 < size addrm)%nat -> nidme ∈ dom addrm -> 0 ≤ uint.Z nidme < max_nodes -> diff --git a/src/program_proof/tulip/paxos/program/paxos_accept.v b/src/program_proof/tulip/paxos/program/paxos_accept.v index c0b85806a..f3b77ab43 100644 --- a/src/program_proof/tulip/paxos/program/paxos_accept.v +++ b/src/program_proof/tulip/paxos/program/paxos_accept.v @@ -7,7 +7,7 @@ Section accept. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_Paxos__accept - (px : loc) (lsn : u64) (term : u64) (entsP : Slice.t) (ents logleader : list string) + (px : loc) (lsn : u64) (term : u64) (entsP : Slice.t) (ents logleader : list byte_string) (nidme : u64) nids γ : nidme ∈ nids -> (uint.nat lsn ≤ length logleader)%nat -> @@ -21,7 +21,7 @@ Section accept. own_slice entsP stringT (DfracOwn 1) ents }}} Paxos__accept #px #lsn #term (to_val entsP) - {{{ (lsna : u64) (loga : list string), RET #lsna; + {{{ (lsna : u64) (loga : list byte_string), RET #lsna; own_paxos_following_with_termc px nidme term nids γ ∗ (is_accepted_proposal_lb γ nidme (uint.nat term) loga ∨ safe_ledger_above γ nids (uint.nat term) loga) ∗ diff --git a/src/program_proof/tulip/paxos/program/paxos_collect.v b/src/program_proof/tulip/paxos/program/paxos_collect.v index dd3e6521a..808556154 100644 --- a/src/program_proof/tulip/paxos/program/paxos_collect.v +++ b/src/program_proof/tulip/paxos/program/paxos_collect.v @@ -7,8 +7,8 @@ Section collect. Theorem wp_Paxos__collect (px : loc) (nid : u64) (term : u64) - (nidme : u64) (entsP : Slice.t) (ents : list string) - (termc lsnc : u64) (logpeer : list string) nids γ : + (nidme : u64) (entsP : Slice.t) (ents : list byte_string) + (termc lsnc : u64) (logpeer : list byte_string) nids γ : nid ∈ nids -> drop (uint.nat lsnc) logpeer = ents -> past_nodedecs_latest_before γ nid (uint.nat termc) (uint.nat term) logpeer -∗ diff --git a/src/program_proof/tulip/paxos/program/paxos_commit.v b/src/program_proof/tulip/paxos/program/paxos_commit.v index b3081223f..6f9747853 100644 --- a/src/program_proof/tulip/paxos/program/paxos_commit.v +++ b/src/program_proof/tulip/paxos/program/paxos_commit.v @@ -7,7 +7,7 @@ Section commit. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_Paxos__commit - (px : loc) (lsn : u64) (nidme term : u64) (logc : list string) nids γ : + (px : loc) (lsn : u64) (nidme term : u64) (logc : list byte_string) nids γ : nidme ∈ nids -> length logc = uint.nat lsn -> safe_ledger_above γ nids (uint.nat term) logc -∗ diff --git a/src/program_proof/tulip/paxos/program/paxos_forward.v b/src/program_proof/tulip/paxos/program/paxos_forward.v index de733219f..78e616b01 100644 --- a/src/program_proof/tulip/paxos/program/paxos_forward.v +++ b/src/program_proof/tulip/paxos/program/paxos_forward.v @@ -6,7 +6,7 @@ Section forward. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_Paxos__forward - (px : loc) (nid lsn : u64) (nidme termc : u64) (loga : list string) nids γ : + (px : loc) (nid lsn : u64) (nidme termc : u64) (loga : list byte_string) nids γ : nid ≠ nidme -> nid ∈ nids -> length loga = uint.nat lsn -> diff --git a/src/program_proof/tulip/paxos/program/paxos_getlsnc.v b/src/program_proof/tulip/paxos/program/paxos_getlsnc.v index 0f6c5d0bf..21742c408 100644 --- a/src/program_proof/tulip/paxos/program/paxos_getlsnc.v +++ b/src/program_proof/tulip/paxos/program/paxos_getlsnc.v @@ -8,7 +8,7 @@ Section getlsnc. Theorem wp_Paxos__getlsnc (px : loc) (nidme termc : u64) nids γ : {{{ own_paxos_leading_with_termc px nidme termc nids γ }}} Paxos__getlsnc #px - {{{ (lsnc : u64) (logc : list string), RET #lsnc; + {{{ (lsnc : u64) (logc : list byte_string), RET #lsnc; own_paxos_leading_with_termc px nidme termc nids γ ∗ safe_ledger_above γ nids (uint.nat termc) logc ∗ ⌜length logc = uint.nat lsnc⌝ diff --git a/src/program_proof/tulip/paxos/program/paxos_learn.v b/src/program_proof/tulip/paxos/program/paxos_learn.v index 8e2f2a3b0..f83abe72c 100644 --- a/src/program_proof/tulip/paxos/program/paxos_learn.v +++ b/src/program_proof/tulip/paxos/program/paxos_learn.v @@ -6,7 +6,7 @@ Section learn. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_Paxos__learn - (px : loc) (lsn term : u64) (nidme : u64) (logc : list string) nids γ : + (px : loc) (lsn term : u64) (nidme : u64) (logc : list byte_string) nids γ : nidme ∈ nids -> length logc = uint.nat lsn -> safe_ledger_above γ nids (uint.nat term) logc -∗ diff --git a/src/program_proof/tulip/paxos/program/paxos_log.v b/src/program_proof/tulip/paxos/program/paxos_log.v index 741c6b9dd..46d762132 100644 --- a/src/program_proof/tulip/paxos/program/paxos_log.v +++ b/src/program_proof/tulip/paxos/program/paxos_log.v @@ -29,7 +29,7 @@ Section log. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_logAdvance - (fname : string) (termW : u64) (lsnW : u64) (entsS : Slice.t) (ents : list string) : + (fname : byte_string) (termW : u64) (lsnW : u64) (entsS : Slice.t) (ents : list byte_string) : let lsn := uint.nat lsnW in let term := uint.nat termW in ⊢ @@ -90,7 +90,7 @@ Section log. Qed. Theorem wp_logAccept - (fname : string) (lsnW : u64) (entsS : Slice.t) (ents : list string) : + (fname : byte_string) (lsnW : u64) (entsS : Slice.t) (ents : list byte_string) : let lsn := uint.nat lsnW in ⊢ {{{ own_slice_small entsS stringT (DfracOwn 1) ents }}} @@ -146,7 +146,7 @@ Section log. by iApply "HΦ". Qed. - Theorem wp_logPrepare (fname : string) (termW : u64) : + Theorem wp_logPrepare (fname : byte_string) (termW : u64) : let term := uint.nat termW in ⊢ {{{ True }}} @@ -199,7 +199,7 @@ Section log. by iApply "HΦ". Qed. - Theorem wp_logAppend (fname : string) (ent : string) : + Theorem wp_logAppend (fname : byte_string) (ent : byte_string) : ⊢ {{{ True }}} <<< ∀∀ bs wal, fname f↦ bs ∗ ⌜encode_paxos_cmds wal bs⌝ >>> @@ -251,7 +251,7 @@ Section log. by iApply "HΦ". Qed. - Theorem wp_logExtend (fname : string) (entsS : Slice.t) (ents : list string) : + Theorem wp_logExtend (fname : byte_string) (entsS : Slice.t) (ents : list byte_string) : ⊢ {{{ own_slice_small entsS stringT (DfracOwn 1) ents }}} <<< ∀∀ bs wal, fname f↦ bs ∗ ⌜encode_paxos_cmds wal bs⌝ >>> @@ -304,7 +304,7 @@ Section log. by iApply "HΦ". Qed. - Theorem wp_logExpand (fname : string) (lsnW : u64) : + Theorem wp_logExpand (fname : byte_string) (lsnW : u64) : let lsn := uint.nat lsnW in ⊢ {{{ True }}} diff --git a/src/program_proof/tulip/paxos/program/paxos_lookup.v b/src/program_proof/tulip/paxos/program/paxos_lookup.v index 0d8cb1338..837d15ebb 100644 --- a/src/program_proof/tulip/paxos/program/paxos_lookup.v +++ b/src/program_proof/tulip/paxos/program/paxos_lookup.v @@ -12,7 +12,7 @@ Section lookup. <<< ∀∀ log cpool, own_consensus_half γ log cpool >>> Paxos__Lookup #px #lsn @ ↑paxosNS <<< ∃∃ log', own_consensus_half γ log' cpool ∗ ⌜cpool_subsume_log log' cpool⌝ >>> - {{{ (v : string) (ok : bool), RET (#(LitString v), #ok); + {{{ (v : byte_string) (ok : bool), RET (#(LitString v), #ok); ⌜if ok then log' !! (uint.nat lsn) = Some v else True⌝ }}}. Proof. diff --git a/src/program_proof/tulip/paxos/program/paxos_obtain.v b/src/program_proof/tulip/paxos/program/paxos_obtain.v index 7a1cc4af7..37e37c188 100644 --- a/src/program_proof/tulip/paxos/program/paxos_obtain.v +++ b/src/program_proof/tulip/paxos/program/paxos_obtain.v @@ -8,7 +8,7 @@ Section obtain. Theorem wp_Paxos__obtain (px : loc) (nid : u64) (nidme termc : u64) nids γ : {{{ own_paxos_leading_with_termc px nidme termc nids γ }}} Paxos__obtain #px #nid - {{{ (lsne : u64) (entsP : Slice.t) (ents loga : list string), RET (#lsne, (to_val entsP)); + {{{ (lsne : u64) (entsP : Slice.t) (ents loga : list byte_string), RET (#lsne, (to_val entsP)); own_paxos_leading_with_termc px nidme termc nids γ ∗ own_slice entsP stringT (DfracOwn 1) ents ∗ prefix_base_ledger γ (uint.nat termc) loga ∗ diff --git a/src/program_proof/tulip/paxos/program/paxos_prepare.v b/src/program_proof/tulip/paxos/program/paxos_prepare.v index efa8899dd..0a6e82e61 100644 --- a/src/program_proof/tulip/paxos/program/paxos_prepare.v +++ b/src/program_proof/tulip/paxos/program/paxos_prepare.v @@ -9,7 +9,7 @@ Section prepare. termc ≠ terml -> {{{ own_paxos_with_termc_terml px nidme termc terml nids γ }}} Paxos__prepare #px #lsn - {{{ (entsP : Slice.t) (ents logpeer : list string), RET (#terml, (to_val entsP)); + {{{ (entsP : Slice.t) (ents logpeer : list byte_string), RET (#terml, (to_val entsP)); own_paxos_with_termc_terml px nidme termc terml nids γ ∗ own_slice entsP stringT (DfracOwn 1) ents ∗ past_nodedecs_latest_before γ nidme (uint.nat termc) (uint.nat terml) logpeer ∗ diff --git a/src/program_proof/tulip/paxos/program/paxos_submit.v b/src/program_proof/tulip/paxos/program/paxos_submit.v index 6ff7f6ab0..39d7e9b60 100644 --- a/src/program_proof/tulip/paxos/program/paxos_submit.v +++ b/src/program_proof/tulip/paxos/program/paxos_submit.v @@ -6,7 +6,7 @@ From Goose.github_com.mit_pdos.tulip Require Import paxos. Section submit. Context `{!heapGS Σ, !paxos_ghostG Σ}. - Theorem wp_Paxos__Submit (px : loc) (c : string) nidme γ : + Theorem wp_Paxos__Submit (px : loc) (c : byte_string) nidme γ : is_paxos px nidme γ -∗ {{{ True }}} <<< ∀∀ cpool, own_cpool_half γ cpool >>> diff --git a/src/program_proof/tulip/paxos/program/repr.v b/src/program_proof/tulip/paxos/program/repr.v index ca171e281..a4ce2604e 100644 --- a/src/program_proof/tulip/paxos/program/repr.v +++ b/src/program_proof/tulip/paxos/program/repr.v @@ -86,9 +86,9 @@ Section repr. "%Haddrpeers" ∷ ⌜map_Forall (λ nid x, addrm !! nid = Some x.2) conns⌝. Definition own_paxos_candidate_only - (nidme termc terml termp : u64) (logc : list string) + (nidme termc terml termp : u64) (logc : list byte_string) (entspP : Slice.t) (resppP : loc) nids γ : iProp Σ := - ∃ (entsp : list string) (respp : gmap u64 bool), + ∃ (entsp : list byte_string) (respp : gmap u64 bool), "Hentsp" ∷ own_slice entspP stringT (DfracOwn 1) entsp ∗ "Hrespp" ∷ own_map resppP (DfracOwn 1) respp ∗ "#Hvotes" ∷ votes_in γ (dom respp) (uint.nat termc) (uint.nat termp) (logc ++ entsp) ∗ @@ -99,7 +99,7 @@ Section repr. "%Hpltc" ∷ ⌜uint.Z termp < uint.Z termc⌝. Definition own_paxos_candidate - (paxos : loc) (nid termc terml : u64) (logc : list string) (iscand : bool) nids γ : iProp Σ := + (paxos : loc) (nid termc terml : u64) (logc : list byte_string) (iscand : bool) nids γ : iProp Σ := ∃ (termp : u64) (entspP : Slice.t) (resppP : loc), "HiscandP" ∷ paxos ↦[Paxos :: "iscand"] #iscand ∗ "HtermpP" ∷ paxos ↦[Paxos :: "termp"] #termp ∗ @@ -137,7 +137,7 @@ Section repr. accepted_or_committed_until γ nids nid a t (uint.nat i)). Definition own_paxos_leader_only - (termc terml : u64) (log : list string) (lsnpeersP : loc) (peers : gset u64) + (termc terml : u64) (log : list byte_string) (lsnpeersP : loc) (peers : gset u64) nids γ : iProp Σ := ∃ (lsnpeers : gmap u64 u64), "Hps" ∷ own_proposal γ (uint.nat termc) log ∗ @@ -148,7 +148,7 @@ Section repr. "%Hinclnids" ∷ ⌜dom lsnpeers ⊆ peers⌝. Definition own_paxos_leader - (paxos : loc) (nidme termc terml : u64) (log : list string) (isleader : bool) + (paxos : loc) (nidme termc terml : u64) (log : list byte_string) (isleader : bool) nids γ : iProp Σ := ∃ (lsnpeersP : loc), "HisleaderP" ∷ paxos ↦[Paxos :: "isleader"] #isleader ∗ @@ -166,7 +166,7 @@ Section repr. "%Hsc" ∷ ⌜size nids = uint.nat sc⌝. Definition own_paxos_common - (paxos : loc) (nidme termc terml lsnc : u64) (log : list string) nids γ : iProp Σ := + (paxos : loc) (nidme termc terml lsnc : u64) (log : list byte_string) nids γ : iProp Σ := ∃ (hb : bool) (logP : Slice.t), "HhbP" ∷ paxos ↦[Paxos :: "hb"] #hb ∗ "HtermcP" ∷ paxos ↦[Paxos :: "termc"] #termc ∗ @@ -197,7 +197,7 @@ Section repr. predicates should be existentially quantified. *) Definition own_paxos_internal (paxos : loc) (nidme termc terml lsnc : u64) (iscand isleader : bool) nids γ : iProp Σ := - ∃ (log : list string), + ∃ (log : list byte_string), let logc := (take (uint.nat lsnc) log) in "Hpx" ∷ own_paxos_common paxos nidme termc terml lsnc log nids γ ∗ "Hcand" ∷ own_paxos_candidate paxos nidme termc terml logc iscand nids γ ∗ @@ -266,7 +266,7 @@ Section repr. Proof. iIntros "Hpx". iFrame. Qed. Definition is_paxos_fname (paxos : loc) (nidme : u64) γ : iProp Σ := - ∃ (fname : string), + ∃ (fname : byte_string), "#HfnameP" ∷ readonly (paxos ↦[Paxos :: "fname"] #(LitString fname)) ∗ "#Hfnameme" ∷ is_node_wal_fname γ nidme fname. diff --git a/src/program_proof/tulip/paxos/program/resume.v b/src/program_proof/tulip/paxos/program/resume.v index 7df8ef26d..125aa2e46 100644 --- a/src/program_proof/tulip/paxos/program/resume.v +++ b/src/program_proof/tulip/paxos/program/resume.v @@ -4,7 +4,7 @@ From Goose.github_com.mit_pdos.tulip Require Import paxos. Section resume. Context `{!heapGS Σ, !paxos_ghostG Σ}. - Theorem wp_resume (fname : string) (nidme termc terml lsnc : u64) (log : list string) γ : + Theorem wp_resume (fname : byte_string) (nidme termc terml lsnc : u64) (log : list byte_string) γ : {{{ own_current_term_half γ nidme (uint.nat termc) ∗ own_ledger_term_half γ nidme (uint.nat terml) ∗ own_committed_lsn_half γ nidme (uint.nat lsnc) ∗ diff --git a/src/program_proof/tulip/paxos/program/start.v b/src/program_proof/tulip/paxos/program/start.v index 2995676d9..ba11d0aee 100644 --- a/src/program_proof/tulip/paxos/program/start.v +++ b/src/program_proof/tulip/paxos/program/start.v @@ -9,8 +9,8 @@ Section start. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_Start - (nidme : u64) (termc : u64) (terml : u64) (lsnc : u64) (log : list string) - (addrmP : loc) (addrm : gmap u64 chan) (fname : string) γ : + (nidme : u64) (termc : u64) (terml : u64) (lsnc : u64) (log : list byte_string) + (addrmP : loc) (addrm : gmap u64 chan) (fname : byte_string) γ : termc = (W64 0) -> terml = (W64 0) -> lsnc = (W64 0) -> diff --git a/src/program_proof/tulip/paxos/res.v b/src/program_proof/tulip/paxos/res.v index 6709c48a1..4a026926f 100644 --- a/src/program_proof/tulip/paxos/res.v +++ b/src/program_proof/tulip/paxos/res.v @@ -17,22 +17,22 @@ Section res. (** Elements. *) Definition own_log_half γ (l : ledger) : iProp Σ := - own γ.(consensus_log) (mono_list_auth (A:=stringO) (DfracOwn (1 / 2)) l). + own γ.(consensus_log) (mono_list_auth (A:=byte_stringO) (DfracOwn (1 / 2)) l). Definition is_log_lb γ (l : ledger) : iProp Σ := - own γ.(consensus_log) (mono_list_lb (A:=stringO) l). + own γ.(consensus_log) (mono_list_lb (A:=byte_stringO) l). - Definition is_cmd_receipt γ (c : string) : iProp Σ := + Definition is_cmd_receipt γ (c : byte_string) : iProp Σ := ghost_map_elem γ.(consensus_cpool) c DfracDiscarded tt. - Definition own_cpool_half γ (vs : gset string) : iProp Σ := + Definition own_cpool_half γ (vs : gset byte_string) : iProp Σ := ghost_map_auth γ.(consensus_cpool) (1 / 2) (gset_to_gmap tt vs) ∗ ([∗ set] v ∈ vs, is_cmd_receipt γ v). - Definition own_consensus_half γ (l : ledger) (vs : gset string) : iProp Σ := + Definition own_consensus_half γ (l : ledger) (vs : gset byte_string) : iProp Σ := own_log_half γ l ∗ own_cpool_half γ vs. - Definition cpool_subsume_log (l : ledger) (vs : gset string) := + Definition cpool_subsume_log (l : ledger) (vs : gset byte_string) := Forall (λ v, v ∈ vs) l. (** Type class instances. *) @@ -170,12 +170,12 @@ Section res. Definition own_proposal γ (t : nat) (v : ledger) : iProp Σ := ∃ name, is_proposal_name γ t name ∗ - own name (mono_list_auth (A:=stringO) (DfracOwn (1 / 2)) v). + own name (mono_list_auth (A:=byte_stringO) (DfracOwn (1 / 2)) v). Definition is_proposal_lb γ (t : nat) (v : ledger) : iProp Σ := ∃ name, is_proposal_name γ t name ∗ - own name (mono_list_lb (A:=stringO) v). + own name (mono_list_lb (A:=byte_stringO) v). (** Type class instances. *) @@ -197,7 +197,7 @@ Section res. iDestruct (big_sepM2_dom with "Hpslm") as %Hdom. assert (Hnamest : names !! t = None). { by rewrite -not_elem_of_dom Hdom not_elem_of_dom. } - iMod (own_alloc (mono_list_auth (A:=stringO) (DfracOwn 1) v)) as (name) "Hl". + iMod (own_alloc (mono_list_auth (A:=byte_stringO) (DfracOwn 1) v)) as (name) "Hl". { apply mono_list_auth_valid. } iMod (ghost_map_insert _ name with "Hauth") as "[Hauth Hfrag]". { apply Hnamest. } @@ -478,11 +478,11 @@ Section res. Definition own_accepted_proposal γ (nid : u64) (t : nat) (v : ledger) : iProp Σ := ∃ name, is_accepted_proposal_name γ nid t name ∗ - own name (mono_list_auth (A:=stringO) (DfracOwn (1 / 2)) v). + own name (mono_list_auth (A:=byte_stringO) (DfracOwn (1 / 2)) v). Definition is_accepted_proposal_lb γ (nid : u64) (t : nat) (v : ledger) : iProp Σ := ∃ name, - is_accepted_proposal_name γ nid t name ∗ own name (mono_list_lb (A:=stringO) v). + is_accepted_proposal_name γ nid t name ∗ own name (mono_list_lb (A:=byte_stringO) v). Definition is_accepted_proposal_length_lb γ (nid : u64) (t n : nat) : iProp Σ := ∃ v, is_accepted_proposal_lb γ nid t v ∗ ⌜(n ≤ length v)%nat⌝. @@ -503,7 +503,7 @@ Section res. Proof. iIntros (Hnotin) "Hauth". iDestruct "Hauth" as (gnames) "(Hauth & Hblts)". - iMod (own_alloc (mono_list_auth (A:=stringO) (DfracOwn 1) v)) as (α) "Hblt". + iMod (own_alloc (mono_list_auth (A:=byte_stringO) (DfracOwn 1) v)) as (α) "Hblt". { apply mono_list_auth_valid. } iDestruct (big_sepM2_dom with "Hblts") as %Hdom. assert (Hgnotin : gnames !! t = None). @@ -875,8 +875,8 @@ Section wal. by destruct Hvalid as [_ ?]. Qed. - Definition is_node_wal_fname γ (nid : u64) (fname : string) : iProp Σ := - own γ.(node_wal_fname) {[ nid := (to_agree (A:=stringO) fname) ]}. + Definition is_node_wal_fname γ (nid : u64) (fname : byte_string) : iProp Σ := + own γ.(node_wal_fname) {[ nid := (to_agree (A:=byte_stringO) fname) ]}. #[global] Instance is_node_wal_fname_persistent γ nid fname : @@ -925,7 +925,7 @@ Section alloc. iMod (own_alloc (mono_list_auth (DfracOwn 1) [])) as (γconsensus_log) "(Hconsensus_log1&Hconsensus_log2)". { econstructor; try econstructor; rewrite //=. } - iMod (ghost_map_alloc_empty (K := string) (V := unit)) as + iMod (ghost_map_alloc_empty (K := byte_string) (V := unit)) as (γconsensus_cpool) "(Hconsensus_cpool1&Hconsensus_cpool2)". iMod (ghost_map_alloc_empty (K := nat) (V := gname)) as (γproposal) "Hproposals". @@ -964,7 +964,7 @@ Section alloc. (γnode_wal) "Hnode_wal". { apply gset_to_gmap_valid. rewrite //=. } - iMod (own_alloc ((to_agree <$> fnames) : gmapR u64 (agreeR stringO))) as + iMod (own_alloc ((to_agree <$> fnames) : gmapR u64 (agreeR byte_stringO))) as (γnode_wal_fname) "Hnode_wal_fname". { intros k. rewrite lookup_fmap; destruct (fnames !! k) eqn:Heq; rewrite Heq //=. } diff --git a/src/program_proof/tulip/program/gcoord/encode.v b/src/program_proof/tulip/program/gcoord/encode.v index aa14d551e..1c7d731ad 100644 --- a/src/program_proof/tulip/program/gcoord/encode.v +++ b/src/program_proof/tulip/program/gcoord/encode.v @@ -8,7 +8,7 @@ Opaque u64_le. Section encode. Context `{!heapGS Σ, !paxos_ghostG Σ}. - Theorem wp_EncodeTxnReadRequest (ts : u64) (key : string) : + Theorem wp_EncodeTxnReadRequest (ts : u64) (key : byte_string) : {{{ True }}} EncodeTxnReadRequest #ts #(LitString key) {{{ (dataP : Slice.t) (data : list u8), RET (to_val dataP); @@ -19,7 +19,7 @@ Section encode. iIntros (Φ) "_ HΦ". wp_rec. - (*@ func EncodeTxnReadRequest(ts uint64, key string) []byte { @*) + (*@ func EncodeTxnReadRequest(ts uint64, key byte_string) []byte { @*) (*@ bs := make([]byte, 0, 32) @*) (*@ bs1 := marshal.WriteInt(bs, MSG_TXN_READ) @*) (*@ bs2 := marshal.WriteInt(bs1, ts) @*) diff --git a/src/program_proof/tulip/program/util/decode_string.v b/src/program_proof/tulip/program/util/decode_string.v index 02bc99713..b1ed29898 100644 --- a/src/program_proof/tulip/program/util/decode_string.v +++ b/src/program_proof/tulip/program/util/decode_string.v @@ -32,7 +32,6 @@ Section program. wp_apply (wp_StringFromBytes with "Hp2"). iIntros "Hp2". wp_pures. - rewrite string_to_bytes_to_string. by iApply "HΦ". Qed. diff --git a/src/program_proof/tulip/program/util/encode_strings.v b/src/program_proof/tulip/program/util/encode_strings.v index 0719efb95..83d49aba1 100644 --- a/src/program_proof/tulip/program/util/encode_strings.v +++ b/src/program_proof/tulip/program/util/encode_strings.v @@ -6,7 +6,7 @@ Section program. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_EncodeStrings - (bsP : Slice.t) (strsP : Slice.t) (bs : list u8) (strs : list string) : + (bsP : Slice.t) (strsP : Slice.t) (bs : list u8) (strs : list byte_string) : {{{ own_slice bsP byteT (DfracOwn 1) bs ∗ own_slice_small strsP stringT (DfracOwn 1) strs }}} diff --git a/src/program_proof/tulip/res_txnsys.v b/src/program_proof/tulip/res_txnsys.v index 920a77d7a..4cf286464 100644 --- a/src/program_proof/tulip/res_txnsys.v +++ b/src/program_proof/tulip/res_txnsys.v @@ -634,10 +634,10 @@ Section res. (** Computes a dbmap from its representation as a GooseLang value. If decoding fails, returns some arbitrary nonsense value. *) - Definition to_dbval (b : bool) (v : string) := + Definition to_dbval (b : bool) (v : byte_string) := if b then Some v else None. - Definition to_dbstring (v : val) : option string := + Definition to_dbstring (v : val) : option byte_string := match v with | (#true, (#(LitString key), _))%V => Some key | (#false, (#(LitString key), _))%V => None @@ -645,7 +645,7 @@ Section res. end. Definition decode_dbmap (v: val) : dbmap := - match @map.map_val _ dbkey (@string_IntoVal grove_op) String.eq_dec String.countable v with + match map.map_val v with | None => ∅ | Some (mv, _) => to_dbstring <$> mv end. diff --git a/src/program_proof/tutorial/kvservice/full_proof.v b/src/program_proof/tutorial/kvservice/full_proof.v index d476d9e52..456e1b57e 100644 --- a/src/program_proof/tutorial/kvservice/full_proof.v +++ b/src/program_proof/tutorial/kvservice/full_proof.v @@ -14,13 +14,13 @@ Module putArgs. Record t := mk { opId: u64 ; - key: string ; - val: string ; + key: byte_string ; + val: byte_string ; }. Definition encodes (x:list u8) (a:t) : Prop := - x = u64_le a.(opId) ++ (u64_le $ length $ string_to_bytes a.(key)) ++ - string_to_bytes a.(key) ++ string_to_bytes a.(val) + x = u64_le a.(opId) ++ (u64_le $ length a.(key)) ++ + a.(key) ++ a.(val) . Section local_defs. @@ -147,7 +147,6 @@ Proof. wp_storeField. iModIntro. iApply "HΦ". - repeat rewrite string_to_bytes_to_string. iFrame. Qed. @@ -158,14 +157,14 @@ Module conditionalPutArgs. Record t := mk { opId: u64 ; - key: string ; - expectedVal: string ; - newVal: string ; + key: byte_string ; + expectedVal: byte_string ; + newVal: byte_string ; }. Definition encodes (x:list u8) (a:t) : Prop := - x = u64_le a.(opId) ++ (u64_le $ length $ string_to_bytes a.(key)) ++ string_to_bytes a.(key) ++ - (u64_le $ length $ string_to_bytes a.(expectedVal)) ++ string_to_bytes a.(expectedVal) ++ string_to_bytes a.(newVal) + x = u64_le a.(opId) ++ (u64_le $ length a.(key)) ++ a.(key) ++ + (u64_le $ length a.(expectedVal)) ++ a.(expectedVal) ++ a.(newVal) . Section local_defs. @@ -324,8 +323,6 @@ Proof. wp_storeField. iModIntro. iApply "HΦ". iFrame. - rewrite ?string_to_bytes_to_string. - iFrame. Qed. End local_defs. @@ -335,11 +332,11 @@ Module getArgs. Record t := mk { opId: u64 ; - key: string ; + key: byte_string ; }. Definition encodes (x:list u8) (a:t) : Prop := - x = u64_le a.(opId) ++ string_to_bytes a.(key) + x = u64_le a.(opId) ++ a.(key) . Section local_defs. @@ -432,8 +429,6 @@ Proof. iModIntro. iApply "HΦ". iFrame. - rewrite string_to_bytes_to_string. - iFrame. Qed. End local_defs. @@ -543,7 +538,7 @@ Record erpc_names := Implicit Types γ:erpc_names. Class erpcG Σ := { - #[global] receiptG :: ghost_mapG Σ u64 string ; + #[global] receiptG :: ghost_mapG Σ u64 byte_string ; #[global] tokenG :: ghost_mapG Σ u64 unit ; #[global] clientTokenG :: inG Σ dfracR ; }. @@ -556,20 +551,20 @@ Definition own_unexecuted_token γ (opId:u64) : iProp Σ := Definition is_executed_witness γ (opId:u64) : iProp Σ := opId ↪[γ.(req_gn)]□ (). -Definition is_request_receipt γ (opId:u64) (r:string) : iProp Σ := +Definition is_request_receipt γ (opId:u64) (r:byte_string) : iProp Σ := opId ↪[γ.(reply_gn)]□ r. Definition own_client_token γcl : iProp Σ := own γcl (DfracOwn 1). -Definition is_request_inv γ γcl (opId:u64) (pre:iProp Σ) (post:string → iProp Σ) : iProp Σ := +Definition is_request_inv γ γcl (opId:u64) (pre:iProp Σ) (post:byte_string → iProp Σ) : iProp Σ := inv reqN (own_unexecuted_token γ opId ∗ pre ∨ is_executed_witness γ opId ∗ (∃ r, is_request_receipt γ opId r ∗ (post r ∨ own_client_token γcl))). -Definition own_erpc_server γ (nextFreshId:u64) (lastReplies:gmap u64 string) : iProp Σ := +Definition own_erpc_server γ (nextFreshId:u64) (lastReplies:gmap u64 byte_string) : iProp Σ := ∃ (usedIds:gset u64), "Htoks" ∷ ghost_map_auth γ.(req_gn) 1 (gset_to_gmap () usedIds) ∗ "Hreplies" ∷ ghost_map_auth γ.(reply_gn) 1 lastReplies ∗ @@ -581,7 +576,7 @@ Lemma alloc_erpc_server : ⊢ |==> ∃ γ, own_erpc_server γ 0 ∅. Proof. iMod (ghost_map_alloc_empty (V:=())) as (γreq) "Htoks". - iMod (ghost_map_alloc_empty (V:=string)) as (γreply) "Hreplies". + iMod (ghost_map_alloc_empty (V:=byte_string)) as (γreply) "Hreplies". iModIntro. iExists {| req_gn := _ ; reply_gn := _ |}. iExists ∅. @@ -642,7 +637,7 @@ Proof. iFrame. Qed. -Lemma server_duplicate_request_step opId r γ (lastReplies:gmap u64 string) nextFreshId: +Lemma server_duplicate_request_step opId r γ (lastReplies:gmap u64 byte_string) nextFreshId: lastReplies !! opId = Some r → own_erpc_server γ nextFreshId lastReplies -∗ is_executed_witness γ opId ∗ @@ -653,7 +648,7 @@ Proof. by iDestruct (big_sepM_lookup_acc with "Hwits") as "[$ HH]". Qed. -Lemma server_execute_step opId γ γcl pre post (lastReplies:gmap u64 string) nextFreshId: +Lemma server_execute_step opId γ γcl pre post (lastReplies:gmap u64 byte_string) nextFreshId: lastReplies !! opId = None → £ 1 -∗ is_request_inv γ γcl opId pre post -∗ @@ -744,7 +739,7 @@ Record kvservice_names := Class kvserviceG Σ := { #[global] erpc_inG :: erpcG Σ ; - #[global] kvs_inG :: ghost_mapG Σ string string ; + #[global] kvs_inG :: ghost_mapG Σ byte_string byte_string ; }. End ghost_proof. @@ -781,7 +776,7 @@ Definition conditionalPut_core_pre (args:conditionalPutArgs.t) : iProp Σ := args.(conditionalPutArgs.newVal) else oldv) ={∅,⊤∖↑reqN}=∗ (Q (bool_decide (oldv = args.(conditionalPutArgs.expectedVal)))))) - (λ r, if decide (r = "ok") then Q true else Q false) + (λ r, if decide (r = "ok"%go) then Q true else Q false) . Definition conditionalPut_core_post (args:conditionalPutArgs.t) r : iProp Σ := @@ -805,15 +800,15 @@ Module server. Record t := mk { nextFreshId : u64 ; - lastReplies : gmap u64 string ; - kvs : gmap string string ; + lastReplies : gmap u64 byte_string ; + kvs : gmap byte_string byte_string ; }. Global Instance etaServer : Settable _ := settable! (mk) . -Definition gauge_eq : relation (gmap string string) := - λ m1 m2, ∀ k, default "" (m1 !! k) = default "" (m2 !! k). +Definition gauge_eq : relation (gmap byte_string byte_string) := + λ m1 m2, ∀ k, default ""%go (m1 !! k) = default ""%go (m2 !! k). Global Instance gauge_eq_Equivalence: Equivalence (gauge_eq). Proof. @@ -831,14 +826,14 @@ Proof. intros ????. destruct (decide (k = k0)). - do 2 (rewrite lookup_insert_ne; last done). done. Qed. -Global Instance gauge_proper_default_lookup (k:string) : - Proper (gauge_eq ==> eq) (λ m, default "" (lookup k m)). +Global Instance gauge_proper_default_lookup (k:byte_string) : + Proper (gauge_eq ==> eq) (λ m, default ""%go (lookup k m)). Proof. intros ???. apply H. Qed. Section local_defns. Context `{!heapGS Σ}. Definition own_mem (s:loc) (st:t) : iProp Σ := - ∃ (lastReplies_loc kvs_loc:loc) (kvs_phys:gmap string string), + ∃ (lastReplies_loc kvs_loc:loc) (kvs_phys:gmap byte_string byte_string), "HnextFreshId" ∷ s ↦[Server :: "nextFreshId"] #st.(nextFreshId) ∗ "HlastReplies" ∷ s ↦[Server :: "lastReplies"] #lastReplies_loc ∗ "Hkvs" ∷ s ↦[Server :: "kvs"] #kvs_loc ∗ @@ -949,7 +944,7 @@ Lemma ghost_put γ st args : put_core_pre γ args -∗ server.own_ghost γ st ={⊤}=∗ server.own_ghost γ - (st <|server.lastReplies := <[args.(putArgs.opId) := ""]> st.(server.lastReplies)|> + (st <|server.lastReplies := <[args.(putArgs.opId) := ""%go]> st.(server.lastReplies)|> <|server.kvs := <[args.(putArgs.key) := args.(putArgs.val)]> st.(server.kvs)|>) ∗ put_core_post γ args. Proof. @@ -1056,19 +1051,19 @@ Qed. Local Definition cond_put_ok st args := (st <|server.lastReplies := - <[args.(conditionalPutArgs.opId) := "ok"]> st.(server.lastReplies)|> + <[args.(conditionalPutArgs.opId) := "ok"%go]> st.(server.lastReplies)|> <|server.kvs := <[args.(conditionalPutArgs.key) := args.(conditionalPutArgs.newVal)]> st.(server.kvs)|>) . Local Definition cond_put_not_ok st args := - (st <|server.lastReplies := <[args.(conditionalPutArgs.opId) := ""]> + (st <|server.lastReplies := <[args.(conditionalPutArgs.opId) := ""%go]> st.(server.lastReplies)|>) . Lemma ghost_conditionalPut_ok γ st args : st.(server.lastReplies) !! args.(conditionalPutArgs.opId) = None → - default "" (st.(server.kvs) !! args.(conditionalPutArgs.key)) = args.(conditionalPutArgs.expectedVal) → + default ""%go (st.(server.kvs) !! args.(conditionalPutArgs.key)) = args.(conditionalPutArgs.expectedVal) → £ 1 -∗ conditionalPut_core_pre γ args -∗ server.own_ghost γ st ={⊤}=∗ @@ -1091,19 +1086,19 @@ Proof. by rewrite H1. } - iMod ("Hclose" $! "ok" with "HQ") as "[Herpc #Hwit]". + iMod ("Hclose" $! "ok"%go with "HQ") as "[Herpc #Hwit]". iModIntro. iFrame "∗#%". iPureIntro. simpl. by f_equiv. Qed. Lemma ghost_conditionalPut_not_ok γ st args : st.(server.lastReplies) !! args.(conditionalPutArgs.opId) = None → - default "" (st.(server.kvs) !! args.(conditionalPutArgs.key)) ≠ args.(conditionalPutArgs.expectedVal) → + default ""%go (st.(server.kvs) !! args.(conditionalPutArgs.key)) ≠ args.(conditionalPutArgs.expectedVal) → £ 1 -∗ conditionalPut_core_pre γ args -∗ server.own_ghost γ st ={⊤}=∗ server.own_ghost γ (cond_put_not_ok st args) ∗ - conditionalPut_core_post γ args "". + conditionalPut_core_post γ args ""%go. Proof. intros. iIntros "Hlc Hspec". iNamed 1. @@ -1119,7 +1114,7 @@ Proof. by rewrite H1. } iMod ("Hau" with "Hptsto") as "HQ". - iMod ("Hclose" $! "" with "HQ") as "[Herpc #Hwit]". + iMod ("Hclose" $! ""%go with "HQ") as "[Herpc #Hwit]". iModIntro. iFrame "∗#%" . Qed. @@ -1275,9 +1270,9 @@ Lemma ghost_get γ st args : server.own_ghost γ st ={⊤}=∗ server.own_ghost γ (st <|server.lastReplies := - <[args.(getArgs.opId) := (default "" (st.(server.kvs) !! args.(getArgs.key)))]> + <[args.(getArgs.opId) := (default ""%go (st.(server.kvs) !! args.(getArgs.key)))]> st.(server.lastReplies)|>) ∗ - get_core_post γ args (default "" (st.(server.kvs) !! args.(getArgs.key))). + get_core_post γ args (default ""%go (st.(server.kvs) !! args.(getArgs.key))). Proof. intros. iIntros "Hlc Hspec". iNamed 1. @@ -1406,7 +1401,7 @@ Proof. wp_apply (wp_new_free_lock). iIntros (mu) "HmuInv". wp_storeField. - wp_apply (wp_NewMap string). + wp_apply (wp_NewMap byte_string). iIntros (kvs_loc) "HkvsM". wp_storeField. wp_apply (wp_NewMap u64). @@ -1451,9 +1446,8 @@ Program Definition conditionalPut_spec γ := spec_ty := conditionalPutArgs.t ; spec_Pre := (λ args enc_args, ⌜ conditionalPutArgs.encodes enc_args args ⌝ ∗ conditionalPut_core_pre γ args)%I; - spec_Post := (λ args enc_args enc_reply, ∃ reply, - ⌜ enc_reply = string_to_bytes reply ⌝ ∗ - conditionalPut_core_post γ args reply)%I; + spec_Post := (λ args enc_args enc_reply, + conditionalPut_core_post γ args enc_reply)%I; |}. Program Definition get_spec γ := @@ -1461,9 +1455,8 @@ Program Definition get_spec γ := spec_ty := getArgs.t ; spec_Pre := (λ args enc_args, ⌜ getArgs.encodes enc_args args ⌝ ∗ get_core_pre γ args)%I; - spec_Post := (λ args enc_args enc_reply, ∃ reply, - ⌜ enc_reply = string_to_bytes reply ⌝ ∗ - get_core_post γ args reply)%I; + spec_Post := (λ args enc_args enc_reply, + get_core_post γ args enc_reply)%I; |}. Definition is_kvserver_host host γ : iProp Σ := @@ -1748,7 +1741,7 @@ Lemma wp_Client__conditionalPutRpc γ cl args args_ptr : }}} Client__conditionalPutRpc #cl #args_ptr {{{ - (s:string) (err:u64), RET (#str s, #err); if decide (err = 0) then + (s:byte_string) (err:u64), RET (#str s, #err); if decide (err = 0) then conditionalPut_core_post γ args s else True }}}. @@ -1776,13 +1769,13 @@ Proof. { destruct err. { destruct c; by exfalso. } - iDestruct "Hpost" as "(? & (% & % & ? & ? & (% & % & ?)))". + iDestruct "Hpost" as "(? & (% & % & ? & ? & ?))". subst. wp_load. wp_apply (wp_StringFromBytes with "[$]"). iIntros "?". wp_pures. iApply "HΦ". - iModIntro. rewrite string_to_bytes_to_string. iFrame. + iModIntro. iFrame. } { wp_pures. iApply "HΦ". rewrite decide_False //. } Qed. @@ -1795,7 +1788,7 @@ Lemma wp_Client__getRpc γ cl args args_ptr : }}} Client__getRpc #cl #args_ptr {{{ - (s:string) (err:u64), RET (#str s, #err); if decide (err = 0) then get_core_post γ args s else True + (s:byte_string) (err:u64), RET (#str s, #err); if decide (err = 0) then get_core_post γ args s else True }}}. Proof. iIntros (Φ) "Hpre HΦ". @@ -1821,13 +1814,13 @@ Proof. { destruct err. { destruct c; by exfalso. } - iDestruct "Hpost" as "(? & (% & % & ? & ? & (% & % & ?)))". + iDestruct "Hpost" as "(? & (% & % & ? & ? & ?))". subst. wp_load. wp_apply (wp_StringFromBytes with "[$]"). iIntros "?". wp_pures. iApply "HΦ". - iModIntro. rewrite string_to_bytes_to_string. iFrame. + iModIntro. iFrame. } { wp_pures. iApply "HΦ". rewrite decide_False //. } Qed. diff --git a/src/program_proof/tutorial/kvservice/proof.v b/src/program_proof/tutorial/kvservice/proof.v index 0bee80249..fe994139f 100644 --- a/src/program_proof/tutorial/kvservice/proof.v +++ b/src/program_proof/tutorial/kvservice/proof.v @@ -14,13 +14,13 @@ Module putArgs. Record t := mk { opId: u64 ; - key: string ; - val: string ; + key: byte_string ; + val: byte_string ; }. Definition encodes (x:list u8) (a:t) : Prop := - x = u64_le a.(opId) ++ (u64_le $ length $ string_to_bytes a.(key)) ++ - string_to_bytes a.(key) ++ string_to_bytes a.(val) + x = u64_le a.(opId) ++ (u64_le $ length a.(key)) ++ + a.(key) ++ a.(val) . Section local_defs. @@ -147,7 +147,6 @@ Proof. wp_storeField. iModIntro. iApply "HΦ". - do 2 rewrite string_to_bytes_to_string. iFrame. Qed. @@ -158,14 +157,14 @@ Module conditionalPutArgs. Record t := mk { opId: u64 ; - key: string ; - expectedVal: string ; - newVal: string ; + key: byte_string ; + expectedVal: byte_string ; + newVal: byte_string ; }. Definition encodes (x:list u8) (a:t) : Prop := - x = u64_le a.(opId) ++ (u64_le $ length $ string_to_bytes a.(key)) ++ string_to_bytes a.(key) ++ - (u64_le $ length $ string_to_bytes a.(expectedVal)) ++ string_to_bytes a.(expectedVal) ++ string_to_bytes a.(newVal) + x = u64_le a.(opId) ++ (u64_le $ length a.(key)) ++ a.(key) ++ + (u64_le $ length a.(expectedVal)) ++ a.(expectedVal) ++ a.(newVal) . Section local_defs. @@ -323,7 +322,6 @@ Proof. iIntros "_". wp_storeField. iModIntro. iApply "HΦ". - repeat rewrite string_to_bytes_to_string. iFrame. Qed. @@ -334,11 +332,11 @@ Module getArgs. Record t := mk { opId: u64 ; - key: string ; + key: byte_string ; }. Definition encodes (x:list u8) (a:t) : Prop := - x = u64_le a.(opId) ++ string_to_bytes a.(key) + x = u64_le a.(opId) ++ a.(key) . Section local_defs. @@ -430,7 +428,6 @@ Proof. wp_storeField. iModIntro. iApply "HΦ". - repeat rewrite string_to_bytes_to_string. iFrame. Qed. @@ -544,14 +541,14 @@ Definition put_core_spec (args:putArgs.t) (Φ:unit → iPropO Σ): iPropO Σ := Global Instance put_core_MonotonicPred args : MonotonicPred (put_core_spec args). Proof. apply _. Qed. -Definition conditionalPut_core_spec (args:conditionalPutArgs.t) (Φ:string → iPropO Σ): iPropO Σ := +Definition conditionalPut_core_spec (args:conditionalPutArgs.t) (Φ:byte_string → iPropO Σ): iPropO Σ := (* TUTORIAL: write a more useful spec *) (∀ status, Φ status)%I. Global Instance conditionalPut_core_MonotonicPred args : MonotonicPred (conditionalPut_core_spec args). Proof. apply _. Qed. -Definition get_core_spec (args:getArgs.t) (Φ:string → iPropO Σ): iPropO Σ := +Definition get_core_spec (args:getArgs.t) (Φ:byte_string → iPropO Σ): iPropO Σ := (* TUTORIAL: write a more useful spec *) (∀ ret, Φ ret)%I. @@ -564,7 +561,7 @@ Section rpc_server_proofs. Context `{!heapGS Σ}. Definition own_Server (s:loc) : iProp Σ := - ∃ (nextFreshId:u64) (lastReplies:gmap u64 string) (kvs:gmap string string) + ∃ (nextFreshId:u64) (lastReplies:gmap u64 byte_string) (kvs:gmap byte_string byte_string) (lastReplies_loc kvs_loc:loc), "HnextFreshId" ∷ s ↦[Server :: "nextFreshId"] #nextFreshId ∗ "HlastReplies" ∷ s ↦[Server :: "lastReplies"] #lastReplies_loc ∗ @@ -772,7 +769,7 @@ Proof. wp_apply (wp_new_free_lock). iIntros (mu) "HmuInv". wp_storeField. - wp_apply (wp_NewMap string). + wp_apply (wp_NewMap byte_string). iIntros (kvs_loc) "HkvsM". wp_storeField. wp_apply (wp_NewMap u64). @@ -818,7 +815,7 @@ Program Definition conditionalPut_spec := λ (enc_args:list u8), λne (Φ : list u8 -d> iPropO Σ) , (∃ args, "%Henc" ∷ ⌜conditionalPutArgs.encodes enc_args args⌝ ∗ - conditionalPut_core_spec args (λ rep, Φ (string_to_bytes rep)) + conditionalPut_core_spec args (λ rep, Φ rep) )%I . Next Obligation. @@ -829,7 +826,7 @@ Program Definition get_spec := λ (enc_args:list u8), λne (Φ : list u8 -d> iPropO Σ) , (∃ args, "%Henc" ∷ ⌜getArgs.encodes enc_args args⌝ ∗ - get_core_spec args (λ rep, Φ (string_to_bytes rep)) + get_core_spec args (λ rep, Φ rep) )%I . Next Obligation. @@ -1148,7 +1145,7 @@ Lemma wp_Client__conditionalPutRpc Post cl args args_ptr : }}} Client__conditionalPutRpc #cl #args_ptr {{{ - (s:string) (err:u64), RET (#str s, #err); if decide (err = 0) then Post s else True + (s:byte_string) (err:u64), RET (#str s, #err); if decide (err = 0) then Post s else True }}} . Proof. @@ -1189,7 +1186,6 @@ Proof. iIntros "_". wp_pures. iModIntro. iApply "HΦ". - repeat rewrite string_to_bytes_to_string. iFrame. } { @@ -1211,7 +1207,7 @@ Lemma wp_Client__getRpc Post cl args args_ptr : }}} Client__getRpc #cl #args_ptr {{{ - (s:string) (err:u64), RET (#str s, #err); if decide (err = 0) then Post s else True + (s:byte_string) (err:u64), RET (#str s, #err); if decide (err = 0) then Post s else True }}} . Proof. @@ -1252,7 +1248,6 @@ Proof. iIntros "_". wp_pures. iModIntro. iApply "HΦ". - repeat rewrite string_to_bytes_to_string. iFrame. } { diff --git a/src/program_proof/txn/twophase_sub_logical_reln_defs.v b/src/program_proof/txn/twophase_sub_logical_reln_defs.v index 765757b07..42d1dca58 100644 --- a/src/program_proof/txn/twophase_sub_logical_reln_defs.v +++ b/src/program_proof/txn/twophase_sub_logical_reln_defs.v @@ -620,7 +620,7 @@ Proof. iSpecialize ("H" $! j _ _ _ Hctx' with "Hj"); clear Hctx'. iApply (wpc_mono' with "[] [] H"); last by auto. iIntros (v1) "H". iDestruct "H" as (vs1) "(Hj&Hv1)". - iAssert (∃ (vres: string), ⌜ un_op_eval ToStringOp v1 = Some #(LitString vres) ∧ + iAssert (∃ (vres: byte_string), ⌜ un_op_eval ToStringOp v1 = Some #(LitString vres) ∧ un_op_eval ToStringOp vs1 = Some #(LitString vres) ⌝)%I with "[Hv1]" as %Hres. { destruct t; try inversion e; diff --git a/src/program_proof/vrsm/apps/vkv/kv_proof.v b/src/program_proof/vrsm/apps/vkv/kv_proof.v index 1b6990bb1..cc3a52ee8 100644 --- a/src/program_proof/vrsm/apps/vkv/kv_proof.v +++ b/src/program_proof/vrsm/apps/vkv/kv_proof.v @@ -14,11 +14,11 @@ From iris.algebra Require Import dfrac_agree mono_list. From Perennial.program_proof.vrsm.apps Require Import vsm proof kv_vsm_proof log. Class kvG Σ := KvG { - #[global] kv_ghostMapG :: ghost_mapG Σ string string ; + #[global] kv_ghostMapG :: ghost_mapG Σ byte_string byte_string ; #[global] kv_logG :: inG Σ (mono_listR (leibnizO kvOp)) ; #[global] kv_vsmG :: vsmG (sm_record:=kv_record) Σ ; }. -Definition kvΣ := #[configΣ; ghost_mapΣ string string; +Definition kvΣ := #[configΣ; ghost_mapΣ byte_string byte_string; GFunctor (mono_listR (leibnizO kvOp)); vsmΣ (sm_record:=kv_record) ]. @@ -74,7 +74,7 @@ Definition stateN := nroot .@ "state". Definition kv_inv γlog γ : iProp Σ := inv stateN ( ∃ ops, own_log γlog ops ∗ own_kvs γ ops). -Definition kv_ptsto γ (k v : string) : iProp Σ := +Definition kv_ptsto γ (k v : byte_string) : iProp Σ := k ↪[γ.(kv_gn)] v. Context {params:ekvParams.t}. @@ -292,7 +292,7 @@ Proof. iApply "HΦ". repeat iExists _. iFrame "∗#". Qed. -Local Lemma helper (m:gmap string string) s k v d : +Local Lemma helper (m:gmap byte_string byte_string) s k v d : (m ∪ gset_to_gmap d s) !! k = Some v → default d (m !! k) = v. Proof. diff --git a/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v b/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v index c6d7c078d..a9e610748 100644 --- a/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v +++ b/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v @@ -15,10 +15,10 @@ Section defns. Inductive kvOp := | putOp : string → string → kvOp | getOp : string → kvOp - | condPutOp : string → string → string → kvOp + | condPutOp : byte_string → byte_string → byte_string → kvOp . -Definition apply_op (state:gmap string string) (op:kvOp) := +Definition apply_op (state:gmap byte_string byte_string) (op:kvOp) := match op with | getOp _ => state | putOp k v => <[k:=v]> state @@ -30,7 +30,7 @@ Definition apply_op (state:gmap string string) (op:kvOp) := end . -Definition compute_state ops : gmap string string := +Definition compute_state ops : gmap byte_string byte_string := foldl apply_op ∅ ops. Definition compute_reply ops op : list u8 := @@ -86,7 +86,7 @@ Existing Instance kv_record. Context `{!heapGS Σ}. -Lemma wp_encodePutArgs (args_ptr:loc) (key val:string) : +Lemma wp_encodePutArgs (args_ptr:loc) (key val:byte_string) : {{{ "Hargs_key" ∷ args_ptr ↦[vkv.PutArgs :: "Key"] #(str key) ∗ "Hargs_val" ∷ args_ptr ↦[vkv.PutArgs :: "Val"] #(str val) @@ -136,7 +136,7 @@ Proof. by rewrite string_bytes_length. Qed. -Lemma wp_decodePutArgs enc_sl enc q (key val:string) : +Lemma wp_decodePutArgs enc_sl enc q (key val:byte_string) : {{{ "%Henc" ∷ ⌜has_op_encoding enc (putOp key val)⌝ ∗ "Hsl" ∷ own_slice_small enc_sl byteT q enc @@ -209,7 +209,7 @@ Proof. iFrame. Qed. -Lemma wp_encodeGetArgs (key:string) : +Lemma wp_encodeGetArgs (key:byte_string) : {{{ True }}} @@ -246,7 +246,7 @@ Proof. done. Qed. -Lemma wp_decodeGetArgs enc_sl enc q (key:string) : +Lemma wp_decodeGetArgs enc_sl enc q (key:byte_string) : {{{ "%Henc" ∷ ⌜has_op_encoding enc (getOp key)⌝ ∗ "Hsl" ∷ own_slice_small enc_sl byteT q enc @@ -272,7 +272,7 @@ Proof. by iApply "HΦ". Qed. -Lemma wp_encodeCondPutArgs (args_ptr:loc) (key expect val:string) : +Lemma wp_encodeCondPutArgs (args_ptr:loc) (key expect val:byte_string) : {{{ "Hargs_key" ∷ args_ptr ↦[vkv.CondPutArgs :: "Key"] #(str key) ∗ "Hargs_expect" ∷ args_ptr ↦[vkv.CondPutArgs :: "Expect"] #(str expect) ∗ @@ -336,7 +336,7 @@ Proof. repeat rewrite -app_assoc. done. Qed. -Lemma wp_decodeCondPutArgs enc_sl enc q (key expect val:string) : +Lemma wp_decodeCondPutArgs enc_sl enc q (key expect val:byte_string) : {{{ "%Henc" ∷ ⌜has_op_encoding enc (condPutOp key expect val)⌝ ∗ "Hsl" ∷ own_slice_small enc_sl byteT q enc @@ -428,18 +428,18 @@ Notation is_state := (is_state (sm_record:=kv_record)). Context `{!vsmG (sm_record:=kv_record) Σ}. Definition own_KVState (s:loc) γst (ops:list OpType) (latestVnum:u64) : iProp Σ := - ∃ (kvs_loc vnums_loc:loc) (vnumsM:gmap string u64) (minVnum:u64), + ∃ (kvs_loc vnums_loc:loc) (vnumsM:gmap byte_string u64) (minVnum:u64), "Hkvs" ∷ s ↦[KVState :: "kvs"] #kvs_loc ∗ "Hvnums" ∷ s ↦[KVState :: "vnums"] #vnums_loc ∗ "HminVnum" ∷ s ↦[KVState :: "minVnum"] #minVnum ∗ "Hkvs_map" ∷ own_map kvs_loc (DfracOwn 1) (compute_state ops) ∗ "Hvnums_map" ∷ own_map vnums_loc (DfracOwn 1) vnumsM ∗ - "#Hst" ∷ □ (∀ (k:string), + "#Hst" ∷ □ (∀ (k:byte_string), (∀ (vnum':u64), ⌜uint.nat vnum' <= uint.nat latestVnum⌝ → ⌜uint.nat (default minVnum (vnumsM !! k)) <= uint.nat vnum'⌝ → ∃ someOps, is_state γst vnum' someOps ∗ ⌜compute_reply someOps (getOp k) = compute_reply ops (getOp k)⌝)) ∗ - "%Hle" ∷ ⌜∀ (k:string), uint.nat (default minVnum (vnumsM !! k)) <= uint.nat latestVnum⌝ + "%Hle" ∷ ⌜∀ (k:byte_string), uint.nat (default minVnum (vnumsM !! k)) <= uint.nat latestVnum⌝ . Implicit Type own_VersionedStateMachine : gname → (list OpType) → u64 → iProp Σ. @@ -922,7 +922,7 @@ Proof. iNamed "Hown". iMod (readonly_load with "Hsnap_sl") as (?) "Hsnap_sl2". wp_storeField. - wp_apply (wp_NewMap string). + wp_apply (wp_NewMap byte_string). iClear "Hvnums_map". iIntros (?) "Hvnums_map". wp_storeField. @@ -993,10 +993,10 @@ Proof. iDestruct (struct_fields_split with "Hs") as "Hs". iNamed "Hs". wp_pures. - wp_apply (wp_NewMap string). + wp_apply (wp_NewMap byte_string). iIntros (?) "Hmap". wp_storeField. - wp_apply (wp_NewMap string). + wp_apply (wp_NewMap byte_string). iIntros (?) "Hvnums_map". wp_storeField. wp_apply (wp_KVState__apply). diff --git a/src/program_proof/vrsm/paxos/start_proof.v b/src/program_proof/vrsm/paxos/start_proof.v index af542a2e2..6f9a9c148 100644 --- a/src/program_proof/vrsm/paxos/start_proof.v +++ b/src/program_proof/vrsm/paxos/start_proof.v @@ -15,7 +15,7 @@ Context `{!paxosG Σ}. Context `{Hparams:!paxosParams.t Σ}. Import paxosParams. -Lemma wp_makeServer γ γsrv (fname:string) data conf_sl (hosts:list u64) init_sl : +Lemma wp_makeServer γ γsrv fname data conf_sl (hosts:list u64) init_sl : {{{ "Hfile" ∷ crash_borrow (own_file_inv γ γsrv data ∗ fname f↦ data) (∃ d : list u8, own_file_inv γ γsrv d ∗ fname f↦d) ∗ @@ -180,7 +180,7 @@ Proof. } Qed. -Lemma wp_StartServer γ γsrv (me:u64) (fname:string) data init_sl conf_sl (hosts:list u64) : +Lemma wp_StartServer γ γsrv (me:u64) fname data init_sl conf_sl (hosts:list u64) : {{{ "Hfile" ∷ crash_borrow (own_file_inv γ γsrv data ∗ fname f↦ data) (∃ d : list u8, own_file_inv γ γsrv d ∗ fname f↦d) ∗ diff --git a/src/program_proof/vrsm/storage/proof.v b/src/program_proof/vrsm/storage/proof.v index 2bae58d95..3be26c9ac 100644 --- a/src/program_proof/vrsm/storage/proof.v +++ b/src/program_proof/vrsm/storage/proof.v @@ -258,7 +258,7 @@ Definition file_inv γ P epoch (contents:list u8) : iProp Σ := . Definition own_StateMachine (s:loc) (epoch:u64) (ops:list OpType) (sealed:bool) P : iProp Σ := - ∃ (fname:string) (aof_ptr:loc) γ γaof (logsize:u64) (smMem_ptr:loc) data + ∃ (fname:byte_string) (aof_ptr:loc) γ γaof (logsize:u64) (smMem_ptr:loc) data own_InMemoryStateMachine (allstates:list (list OpType * bool)), "Hfname" ∷ s ↦[StateMachine :: "fname"] #(LitString fname) ∗ "HlogFile" ∷ s ↦[StateMachine :: "logFile"] #aof_ptr ∗ diff --git a/src/program_proof/wp_auto/experiments.v b/src/program_proof/wp_auto/experiments.v index 9b07d7198..861edc942 100644 --- a/src/program_proof/wp_auto/experiments.v +++ b/src/program_proof/wp_auto/experiments.v @@ -23,7 +23,7 @@ Lemma rename_iprop m n {P:iProp Σ} : . Proof. reflexivity. Qed. -Instance named_proper {A:Type} : Proper ((λ (_ _:string), True) ==> (@eq A) ==> (eq)) named. +Instance named_proper {A:Type} : Proper ((λ (_ _:byte_string), True) ==> (@eq A) ==> (eq)) named. Proof. solve_proper. Qed. Lemma wp_lookupLocked (t : loc) (m : gmap u64 u64) (k : u64) Htracker : From eca15abc82ab65cd2347cb7a71dfc6ac175a5cc7 Mon Sep 17 00:00:00 2001 From: Upamanyu Sharma Date: Thu, 19 Dec 2024 18:32:10 -0500 Subject: [PATCH 5/6] Some more fixes and a FIXME note --- src/program_proof/tulip/inv_group.v | 10 ++++- .../vrsm/apps/vkv/kv_vsm_proof.v | 45 ++++++++----------- 2 files changed, 28 insertions(+), 27 deletions(-) diff --git a/src/program_proof/tulip/inv_group.v b/src/program_proof/tulip/inv_group.v index 1f85bfe8f..90ef49712 100644 --- a/src/program_proof/tulip/inv_group.v +++ b/src/program_proof/tulip/inv_group.v @@ -422,7 +422,7 @@ Section lemma. do 2 iNamed "Hgroup". pose proof (apply_cmds_dom _ _ _ Hrsm) as Hdom. assert (is_Some (hists !! key)) as [h Hh]. - { rewrite -elem_of_dom. set_solver. } + { rewrite -elem_of_dom. rewrite Hdom. set_solver. } iDestruct (txn_log_prefix with "Hlog Hloglb") as %Hprefix. rewrite /hist_from_log in Hhlb. destruct (apply_cmds loglb) as [cmlb histmlb |] eqn:Happly; last done. @@ -467,6 +467,14 @@ Section lemma. iApply (group_inv_witness_repl_hist with "Hloglb Hgroup"). { pose proof (apply_cmds_dom _ _ _ Happly) as Hdom. apply elem_of_dom_2 in Hh. + try fast_done; + intros; setoid_subst; + set_unfold; + intros; setoid_subst; + try match goal with |- _ ∈ _ => apply dec_stable end. + naive_solver eauto. + + naive_solver. set_solver. } { done. } diff --git a/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v b/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v index a9e610748..27bf49cd8 100644 --- a/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v +++ b/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v @@ -13,8 +13,8 @@ From Perennial.algebra Require Import map. Section defns. Inductive kvOp := - | putOp : string → string → kvOp - | getOp : string → kvOp + | putOp : byte_string → byte_string → kvOp + | getOp : byte_string → kvOp | condPutOp : byte_string → byte_string → byte_string → kvOp . @@ -23,7 +23,7 @@ Definition apply_op (state:gmap byte_string byte_string) (op:kvOp) := | getOp _ => state | putOp k v => <[k:=v]> state | condPutOp k e v => - if decide (default "" (state !! k) = e) then + if decide (default ""%go (state !! k) = e) then <[k:=v]> state else state @@ -35,24 +35,24 @@ Definition compute_state ops : gmap byte_string byte_string := Definition compute_reply ops op : list u8 := match op with - | getOp k => string_to_bytes (default "" ((compute_state ops) !! k)) + | getOp k => (default ""%go ((compute_state ops) !! k)) | putOp k v => [] - | condPutOp k e v => if decide (default "" ((compute_state ops) !! k) = e) then - string_to_bytes ("ok") + | condPutOp k e v => if decide (default ""%go ((compute_state ops) !! k) = e) then + ("ok"%go) else [] end . Definition encode_op op : list u8 := match op with - | putOp k v => [W8 0] ++ u64_le (length (string_to_bytes k)) ++ - string_to_bytes k ++ string_to_bytes v - | getOp k => [W8 1] ++ string_to_bytes k - | condPutOp k e v => [W8 2] ++ u64_le (length (string_to_bytes k)) ++ - string_to_bytes k ++ - u64_le (length (string_to_bytes e)) ++ - string_to_bytes e ++ - string_to_bytes v + | putOp k v => [W8 0] ++ u64_le (length k) ++ + k ++ v + | getOp k => [W8 1] ++ k + | condPutOp k e v => [W8 2] ++ u64_le (length k) ++ + k ++ + u64_le (length e) ++ + e ++ + v end . @@ -132,8 +132,7 @@ Proof. wp_store. clear sl. wp_load. iApply "HΦ". iModIntro. iFrame. - iPureIntro. - by rewrite string_bytes_length. + done. Qed. Lemma wp_decodePutArgs enc_sl enc q (key val:byte_string) : @@ -187,13 +186,11 @@ Proof. simpl in Hsl_sz. rewrite length_app in Hkv_sz. wp_apply wp_SliceTake. { word. } - iDestruct (slice_small_split with "Hkv_sl") as "[Hk Hv]". - { shelve. } - replace (uint.nat (length (string_to_bytes key))) with (length (string_to_bytes key)) by word. - Unshelve. - 2:{ rewrite length_app. word. } + iDestruct (slice_small_split _ (length key) with "Hkv_sl") as "[Hk Hv]". + { rewrite length_app. word. } wp_apply (wp_StringFromBytes with "[$Hk]"). iIntros "Hk". + replace (uint.nat (W64 (length key))) with (length key) by word. rewrite take_app_length. wp_storeField. rewrite drop_app_length. @@ -203,7 +200,6 @@ Proof. { word. } wp_apply (wp_StringFromBytes with "[$Hv]"). iIntros "Hv". - do 2 rewrite string_to_bytes_to_string. wp_storeField. iModIntro. iApply "HΦ". iFrame. @@ -268,7 +264,6 @@ Proof. wp_apply (wp_StringFromBytes with "[$]"). iIntros "_". wp_pures. - rewrite string_to_bytes_to_string. by iApply "HΦ". Qed. @@ -385,7 +380,6 @@ Proof. wp_pures. wp_apply (wp_StringFromBytes with "[$Hkey_sl]"). iIntros "_". - rewrite string_to_bytes_to_string. wp_storeField. wp_apply (wp_ReadInt with "[$]"). iIntros (?) "Hsl". @@ -403,7 +397,7 @@ Proof. { word. } iDestruct (slice_small_split with "Hsl") as "[He Hv]". { shelve. } - replace (uint.nat (length (string_to_bytes expect))) with (length (string_to_bytes expect)) by word. + replace (uint.nat (length expect)) with (length expect) by word. Unshelve. 2:{ rewrite length_app. word. } wp_apply (wp_StringFromBytes with "[$He]"). @@ -418,7 +412,6 @@ Proof. wp_apply (wp_StringFromBytes with "[$Hv]"). iIntros "Hv". wp_storeField. - do 2 rewrite string_to_bytes_to_string. iModIntro. iApply "HΦ". iFrame. Qed. From e98b30ce732b3a3977c964a54424f77972e8d087 Mon Sep 17 00:00:00 2001 From: Upamanyu Sharma Date: Fri, 20 Dec 2024 00:32:00 -0500 Subject: [PATCH 6/6] Fix build --- src/program_proof/tulip/base.v | 18 +++-- src/program_proof/tulip/encode.v | 65 ++++++++++++++++++- src/program_proof/tulip/inv_group.v | 10 +-- src/program_proof/tulip/msg.v | 4 +- src/program_proof/tulip/paxos/msg.v | 4 +- .../tulip/program/gcoord/gcoord_read.v | 2 +- .../program/gcoord/gcoord_read_session.v | 2 +- .../tulip/program/gcoord/gcoord_send.v | 2 +- .../gcoord/gcoord_wait_until_value_ready.v | 2 +- .../program/gcoord/greader_clear_versions.v | 2 +- .../gcoord/greader_pick_latest_value.v | 2 +- .../gcoord/greader_process_read_result.v | 2 +- .../tulip/program/gcoord/greader_read.v | 2 +- .../tulip/program/gcoord/greader_reset.v | 4 +- .../tulip/program/gcoord/greader_responded.v | 2 +- src/program_proof/tulip/program/index/index.v | 2 +- src/program_proof/tulip/program/prelude.v | 2 +- .../tulip/program/replica/encode.v | 2 +- .../tulip/program/replica/replica_log.v | 8 +-- .../tulip/program/replica/replica_read.v | 2 +- .../tulip/program/replica/replica_repr.v | 2 +- .../tulip/program/replica/start.v | 4 +- src/program_proof/tulip/program/tuple/res.v | 2 +- src/program_proof/tulip/program/tuple/tuple.v | 2 +- src/program_proof/tulip/program/txn/proph.v | 2 +- .../tulip/program/txn/txn_getwrs.v | 2 +- .../tulip/program/txn/txn_key_to_group.v | 4 +- .../tulip/program/txn/txn_setwrs.v | 2 +- .../tulip/program/txnlog/txnlog.v | 7 +- .../tulip/program/util/decode_string.v | 2 +- .../tulip/program/util/decode_strings.v | 2 +- .../tulip/program/util/encode_string.v | 2 +- src/program_proof/vrsm/apps/closed_proof.v | 14 ++-- src/program_proof/vrsm/apps/closed_wpcs.v | 10 +-- src/program_proof/vrsm/apps/vkv/kv_proof.v | 9 ++- .../vrsm/apps/vkv/kv_vsm_proof.v | 46 +++++++------ 36 files changed, 155 insertions(+), 96 deletions(-) diff --git a/src/program_proof/tulip/base.v b/src/program_proof/tulip/base.v index d31363d8a..415e1ad61 100644 --- a/src/program_proof/tulip/base.v +++ b/src/program_proof/tulip/base.v @@ -22,12 +22,23 @@ Inductive txnres := | ResCommitted (wrs : dbmap) | ResAborted. -Definition fstring := {k : byte_string | (length k < (Z.to_nat (2 ^ 64)%Z))%nat }. +Definition fstring := {k : byte_string | length k < 2 ^ 64 }. #[local] Instance fstring_finite : finite.Finite fstring. -Proof. apply Helpers.finite.list_finite_lt_length. Qed. +Proof. + unfold fstring. + set(x:=2 ^ 64). + generalize x. clear x. intros y. + unshelve refine (finite.surjective_finite (λ x : {k : byte_string | (length k < Z.to_nat y)%nat }, + (proj1_sig x) ↾ _ )). + { abstract (destruct x; simpl; lia). } + { apply Helpers.finite.list_finite_lt_length. } + intros []. + unshelve eexists (exist _ _ _); last rewrite sig_eq_pi /= //. + simpl. lia. +Qed. Definition keys_all : gset byte_string := list_to_set (map proj1_sig (finite.enum fstring)). @@ -300,8 +311,7 @@ Proof. intros Hvk. rewrite /valid_key /keys_all in Hvk. apply elem_of_list_to_set, elem_of_list_fmap_2 in Hvk. - destruct Hvk as ([k Hk] & -> & _). - simpl. lia. + by destruct Hvk as ([k Hk] & -> & _). Qed. Definition valid_ccommand gid (c : ccommand) := diff --git a/src/program_proof/tulip/encode.v b/src/program_proof/tulip/encode.v index f247b87fb..eacdb221d 100644 --- a/src/program_proof/tulip/encode.v +++ b/src/program_proof/tulip/encode.v @@ -1,14 +1,75 @@ From Perennial.program_proof Require Import grove_prelude. From Perennial.program_proof.tulip Require Import base. +Definition encode_string (x : byte_string) : list u8 := + u64_le (U64 (length x)) ++ x. + +Definition encode_strings_step (bs : list u8) (x : byte_string) : list u8 := + bs ++ encode_string x. + +Definition encode_strings_xlen (xs : list byte_string) : list u8 := + foldl encode_strings_step [] xs. + +Definition encode_strings (xs : list byte_string) : list u8 := + u64_le (U64 (length xs)) ++ encode_strings_xlen xs. + +Lemma encode_strings_xlen_snoc xs x : + encode_strings_xlen (xs ++ [x]) = encode_strings_xlen xs ++ encode_string x. +Proof. + by rewrite /encode_strings_xlen foldl_snoc /encode_strings_step. +Qed. + +Lemma foldl_encode_strings_step_app (bs : list u8) (xs : list byte_string) : + foldl encode_strings_step bs xs = bs ++ foldl encode_strings_step [] xs. +Proof. + generalize dependent bs. + induction xs as [| x xs IH]; intros bs. + { by rewrite /= app_nil_r. } + rewrite /= (IH (encode_strings_step bs x)) (IH (encode_strings_step [] x)). + rewrite {1 3}/encode_strings_step. + by rewrite app_nil_l app_assoc. +Qed. + +Lemma encode_strings_xlen_cons xs x : + encode_strings_xlen (x :: xs) = encode_string x ++ encode_strings_xlen xs. +Proof. + rewrite /encode_strings_xlen /= foldl_encode_strings_step_app. + by rewrite {1}/encode_strings_step app_nil_l. +Qed. + +Lemma encode_strings_xlen_length_inv xs n : + (length (encode_strings_xlen xs) ≤ n)%nat -> + (length xs ≤ n)%nat. +Proof. + generalize dependent n. + induction xs as [| x xs IH]; intros n; first done. + rewrite encode_strings_xlen_cons length_app /=. + assert (length (encode_string x) ≠ O). + { by destruct (nil_or_length_pos (encode_string x)). } + intros Hlen. + assert (Hlenxs : (length xs ≤ pred n)%nat). + { apply IH. lia. } + lia. +Qed. + +Lemma encode_strings_length_inv xs n : + (length (encode_strings xs) ≤ n)%nat -> + (length xs ≤ n)%nat. +Proof. + rewrite /encode_strings length_app. + intros Hn. + pose proof (encode_strings_xlen_length_inv xs n) as Hlen. + lia. +Qed. + Definition encode_dbval (x : dbval) : list u8 := match x with - | Some v => [U8 1] ++ v + | Some v => [U8 1] ++ encode_string v | None => [U8 0] end. Definition encode_dbmod (x : dbmod) : list u8 := - x.1 ++ encode_dbval x.2. + encode_string x.1 ++ encode_dbval x.2. Definition encode_dbmods_step (bs : list u8) (x : dbmod) : list u8 := bs ++ encode_dbmod x. diff --git a/src/program_proof/tulip/inv_group.v b/src/program_proof/tulip/inv_group.v index 90ef49712..1f85bfe8f 100644 --- a/src/program_proof/tulip/inv_group.v +++ b/src/program_proof/tulip/inv_group.v @@ -422,7 +422,7 @@ Section lemma. do 2 iNamed "Hgroup". pose proof (apply_cmds_dom _ _ _ Hrsm) as Hdom. assert (is_Some (hists !! key)) as [h Hh]. - { rewrite -elem_of_dom. rewrite Hdom. set_solver. } + { rewrite -elem_of_dom. set_solver. } iDestruct (txn_log_prefix with "Hlog Hloglb") as %Hprefix. rewrite /hist_from_log in Hhlb. destruct (apply_cmds loglb) as [cmlb histmlb |] eqn:Happly; last done. @@ -467,14 +467,6 @@ Section lemma. iApply (group_inv_witness_repl_hist with "Hloglb Hgroup"). { pose proof (apply_cmds_dom _ _ _ Happly) as Hdom. apply elem_of_dom_2 in Hh. - try fast_done; - intros; setoid_subst; - set_unfold; - intros; setoid_subst; - try match goal with |- _ ∈ _ => apply dec_stable end. - naive_solver eauto. - - naive_solver. set_solver. } { done. } diff --git a/src/program_proof/tulip/msg.v b/src/program_proof/tulip/msg.v index a25ad8f17..b4e66ca82 100644 --- a/src/program_proof/tulip/msg.v +++ b/src/program_proof/tulip/msg.v @@ -58,7 +58,7 @@ Proof. Qed. Definition encode_read_req_xkind (ts : u64) (key : byte_string) := - u64_le ts ++ key. + u64_le ts ++ encode_string key. Definition encode_read_req (ts : u64) (key : byte_string) (data : list u8) := data = u64_le (U64 100) ++ encode_read_req_xkind ts key. @@ -215,7 +215,7 @@ Qed. Definition encode_read_resp_xkind (ts rid : u64) (key : byte_string) (ver : dbpver) (slow : bool) := - u64_le ts ++ u64_le rid ++ key ++ + u64_le ts ++ u64_le rid ++ encode_string key ++ encode_dbpver ver ++ [if slow then U8 1 else U8 0]. Definition encode_read_resp diff --git a/src/program_proof/tulip/paxos/msg.v b/src/program_proof/tulip/paxos/msg.v index 33f713340..a3187d26e 100644 --- a/src/program_proof/tulip/paxos/msg.v +++ b/src/program_proof/tulip/paxos/msg.v @@ -36,7 +36,7 @@ Definition encode_request_vote_req (term lsnlc : u64) := Definition encode_append_entries_req_xkind (term lsnlc lsne : u64) (ents : list byte_string) := - u64_le term ++ u64_le lsnlc ++ u64_le lsne ++ concat ents. + u64_le term ++ u64_le lsnlc ++ u64_le lsne ++ encode_strings ents. Definition encode_append_entries_req (term lsnlc lsne : u64) (ents : list byte_string) := @@ -78,7 +78,7 @@ Qed. Definition encode_request_vote_resp_xkind (nid term terme : u64) (ents : list byte_string) := - u64_le nid ++ u64_le term ++ u64_le terme ++ concat ents. + u64_le nid ++ u64_le term ++ u64_le terme ++ encode_strings ents. Definition encode_request_vote_resp (nid term terme : u64) (ents : list byte_string) := diff --git a/src/program_proof/tulip/program/gcoord/gcoord_read.v b/src/program_proof/tulip/program/gcoord/gcoord_read.v index dfadb5a13..6feeb599d 100644 --- a/src/program_proof/tulip/program/gcoord/gcoord_read.v +++ b/src/program_proof/tulip/program/gcoord/gcoord_read.v @@ -7,7 +7,7 @@ Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. Theorem wp_GroupCoordinator__Read - (gcoord : loc) (tsW : u64) (key : string) gid γ : + (gcoord : loc) (tsW : u64) (key : byte_string) gid γ : let ts := uint.nat tsW in safe_read_req gid ts key -> is_gcoord gcoord gid γ -∗ diff --git a/src/program_proof/tulip/program/gcoord/gcoord_read_session.v b/src/program_proof/tulip/program/gcoord/gcoord_read_session.v index c0156aca7..8497d402e 100644 --- a/src/program_proof/tulip/program/gcoord/gcoord_read_session.v +++ b/src/program_proof/tulip/program/gcoord/gcoord_read_session.v @@ -7,7 +7,7 @@ Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. Theorem wp_GroupCoordinator__ReadSession - (gcoord : loc) (rid : u64) (tsW : u64) (key : string) gid γ : + (gcoord : loc) (rid : u64) (tsW : u64) (key : byte_string) gid γ : let ts := uint.nat tsW in rid ∈ rids_all -> safe_read_req gid ts key -> diff --git a/src/program_proof/tulip/program/gcoord/gcoord_send.v b/src/program_proof/tulip/program/gcoord/gcoord_send.v index d935d3eda..df7d6837d 100644 --- a/src/program_proof/tulip/program/gcoord/gcoord_send.v +++ b/src/program_proof/tulip/program/gcoord/gcoord_send.v @@ -74,7 +74,7 @@ Section program. Qed. Theorem wp_GroupCoordinator__SendRead - (gcoord : loc) (rid : u64) (ts : u64) (key : string) addrm gid γ : + (gcoord : loc) (rid : u64) (ts : u64) (key : byte_string) addrm gid γ : safe_read_req gid (uint.nat ts) key -> rid ∈ dom addrm -> is_gcoord_with_addrm gcoord gid addrm γ -∗ diff --git a/src/program_proof/tulip/program/gcoord/gcoord_wait_until_value_ready.v b/src/program_proof/tulip/program/gcoord/gcoord_wait_until_value_ready.v index 90eba3149..4c46b6bb1 100644 --- a/src/program_proof/tulip/program/gcoord/gcoord_wait_until_value_ready.v +++ b/src/program_proof/tulip/program/gcoord/gcoord_wait_until_value_ready.v @@ -7,7 +7,7 @@ Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. Theorem wp_GroupCoordinator__WaitUntilValueReady - (gcoord : loc) (tsW : u64) (key : string) gid γ : + (gcoord : loc) (tsW : u64) (key : byte_string) gid γ : let ts := uint.nat tsW in is_gcoord gcoord gid γ -∗ {{{ True }}} diff --git a/src/program_proof/tulip/program/gcoord/greader_clear_versions.v b/src/program_proof/tulip/program/gcoord/greader_clear_versions.v index b671178b3..c45144c18 100644 --- a/src/program_proof/tulip/program/gcoord/greader_clear_versions.v +++ b/src/program_proof/tulip/program/gcoord/greader_clear_versions.v @@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program.gcoord Require Import greader_repr. Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Theorem wp_GroupReader__clearVersions (grd : loc) (key : string) qreadm ts γ : + Theorem wp_GroupReader__clearVersions (grd : loc) (key : byte_string) qreadm ts γ : {{{ own_greader_qreadm grd qreadm ts γ }}} GroupReader__clearVersions #grd #(LitString key) {{{ RET #(); own_greader_qreadm grd (delete key qreadm) ts γ }}}. diff --git a/src/program_proof/tulip/program/gcoord/greader_pick_latest_value.v b/src/program_proof/tulip/program/gcoord/greader_pick_latest_value.v index a5035b724..22100e8a3 100644 --- a/src/program_proof/tulip/program/gcoord/greader_pick_latest_value.v +++ b/src/program_proof/tulip/program/gcoord/greader_pick_latest_value.v @@ -8,7 +8,7 @@ Local Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations. Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Theorem wp_GroupReader__pickLatestValue (grd : loc) (key : string) qreadm verm ts γ : + Theorem wp_GroupReader__pickLatestValue (grd : loc) (key : byte_string) qreadm verm ts γ : qreadm !! key = Some verm -> cquorum_size rids_all (dom verm) -> {{{ own_greader_qreadm grd qreadm ts γ }}} diff --git a/src/program_proof/tulip/program/gcoord/greader_process_read_result.v b/src/program_proof/tulip/program/gcoord/greader_process_read_result.v index ec81355fa..7cbc997af 100644 --- a/src/program_proof/tulip/program/gcoord/greader_process_read_result.v +++ b/src/program_proof/tulip/program/gcoord/greader_process_read_result.v @@ -10,7 +10,7 @@ Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. Theorem wp_GroupReader__processReadResult - grd (rid : u64) (key : string) (ver : dbpver) (slow : bool) ts γ : + grd (rid : u64) (key : byte_string) (ver : dbpver) (slow : bool) ts γ : rid ∈ rids_all -> fast_or_slow_read γ rid key (uint.nat ver.1) ts ver.2 slow -∗ {{{ own_greader grd ts γ }}} diff --git a/src/program_proof/tulip/program/gcoord/greader_read.v b/src/program_proof/tulip/program/gcoord/greader_read.v index 16f5e0ffe..a81980f20 100644 --- a/src/program_proof/tulip/program/gcoord/greader_read.v +++ b/src/program_proof/tulip/program/gcoord/greader_read.v @@ -5,7 +5,7 @@ From Perennial.program_proof.tulip.program.gcoord Require Import greader_repr. Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Theorem wp_GroupReader__read (grd : loc) (key : string) ts γ : + Theorem wp_GroupReader__read (grd : loc) (key : byte_string) ts γ : {{{ own_greader grd ts γ }}} GroupReader__read #grd #(LitString key) {{{ (v : dbval) (ok : bool), RET (dbval_to_val v, #ok); diff --git a/src/program_proof/tulip/program/gcoord/greader_reset.v b/src/program_proof/tulip/program/gcoord/greader_reset.v index 9cfc4455b..74ce26521 100644 --- a/src/program_proof/tulip/program/gcoord/greader_reset.v +++ b/src/program_proof/tulip/program/gcoord/greader_reset.v @@ -17,10 +17,10 @@ Section program. (*@ grd.qreadm = make(map[string]map[uint64]tulip.Version) @*) (*@ } @*) iNamed "Hgrd". - wp_apply (wp_NewMap string dbval). + wp_apply (wp_NewMap byte_string dbval). iIntros (valuemP') "Hvaluem". wp_storeField. - wp_apply (wp_NewMap string loc). + wp_apply (wp_NewMap byte_string loc). iIntros (qreadmP') "Hqreadm". wp_storeField. iApply "HΦ". diff --git a/src/program_proof/tulip/program/gcoord/greader_responded.v b/src/program_proof/tulip/program/gcoord/greader_responded.v index 1a2addc7f..dac9ccede 100644 --- a/src/program_proof/tulip/program/gcoord/greader_responded.v +++ b/src/program_proof/tulip/program/gcoord/greader_responded.v @@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program.gcoord Require Import greader_repr. Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Theorem wp_GroupReader__responded (grd : loc) (rid : u64) (key : string) ts γ : + Theorem wp_GroupReader__responded (grd : loc) (rid : u64) (key : byte_string) ts γ : {{{ own_greader grd ts γ }}} GroupReader__responded #grd #rid #(LitString key) {{{ (responded : bool), RET #responded; own_greader grd ts γ }}}. diff --git a/src/program_proof/tulip/program/index/index.v b/src/program_proof/tulip/program/index/index.v index 4c78921b8..e48b20855 100644 --- a/src/program_proof/tulip/program/index/index.v +++ b/src/program_proof/tulip/program/index/index.v @@ -22,7 +22,7 @@ Section program. "#HmuP" ∷ readonly (idx ↦[Index :: "mu"] #muP) ∗ "#Hmu" ∷ is_lock tulipNS #muP (own_index idx γ α). - Theorem wp_Index__GetTuple (idx : loc) (key : string) γ α : + Theorem wp_Index__GetTuple (idx : loc) (key : byte_string) γ α : key ∈ keys_all -> is_index idx γ α -∗ {{{ True }}} diff --git a/src/program_proof/tulip/program/prelude.v b/src/program_proof/tulip/program/prelude.v index bc9df88bb..cde056671 100644 --- a/src/program_proof/tulip/program/prelude.v +++ b/src/program_proof/tulip/program/prelude.v @@ -49,7 +49,7 @@ Proof. refine {| to_val := dbmod_to_val; from_val := dbmod_from_val; - IntoVal_def := ("", None); + IntoVal_def := (""%go, None); |}. intros [k v]. by destruct v. diff --git a/src/program_proof/tulip/program/replica/encode.v b/src/program_proof/tulip/program/replica/encode.v index a0079574f..ea1856aba 100644 --- a/src/program_proof/tulip/program/replica/encode.v +++ b/src/program_proof/tulip/program/replica/encode.v @@ -7,7 +7,7 @@ Section encode. Context `{!heapGS Σ, !paxos_ghostG Σ}. Theorem wp_EncodeTxnReadResponse - (rid : u64) (ts : u64) (key : string) (ver : dbpver) (slow : bool) : + (rid : u64) (ts : u64) (key : byte_string) (ver : dbpver) (slow : bool) : {{{ True }}} EncodeTxnReadResponse #ts #rid #(LitString key) (dbpver_to_val ver) #slow {{{ (dataP : Slice.t) (data : list u8), RET (to_val dataP); diff --git a/src/program_proof/tulip/program/replica/replica_log.v b/src/program_proof/tulip/program/replica/replica_log.v index 2ebb1a75d..949952d80 100644 --- a/src/program_proof/tulip/program/replica/replica_log.v +++ b/src/program_proof/tulip/program/replica/replica_log.v @@ -6,7 +6,7 @@ From Perennial.program_proof.tulip.program.util Require Import Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Theorem wp_logRead (fname : string) (ts : u64) (key : string) (bs : list u8) : + Theorem wp_logRead (fname : byte_string) (ts : u64) (key : byte_string) (bs : list u8) : {{{ fname f↦ bs }}} logRead #(LitString fname) #ts #(LitString key) {{{ (bs' : list u8), RET #(); fname f↦ bs' }}}. @@ -52,7 +52,7 @@ Section program. Qed. Theorem wp_logValidate - (fname : string) (ts : u64) (pwrsP : Slice.t) (pwrs : dbmap) (bs : list u8) : + (fname : byte_string) (ts : u64) (pwrsP : Slice.t) (pwrs : dbmap) (bs : list u8) : {{{ fname f↦ bs ∗ own_dbmap_in_slice pwrsP pwrs }}} logValidate #(LitString fname) #ts (to_val pwrsP) slice.nil {{{ (bs' : list u8), RET #(); fname f↦ bs' ∗ own_dbmap_in_slice pwrsP pwrs }}}. @@ -99,7 +99,7 @@ Section program. Qed. Theorem wp_logFastPrepare - (fname : string) (ts : u64) (pwrsP : Slice.t) (pwrs : dbmap) (bs : list u8) : + (fname : byte_string) (ts : u64) (pwrsP : Slice.t) (pwrs : dbmap) (bs : list u8) : {{{ fname f↦ bs ∗ own_dbmap_in_slice pwrsP pwrs }}} logFastPrepare #(LitString fname) #ts (to_val pwrsP) slice.nil {{{ (bs' : list u8), RET #(); fname f↦ bs' ∗ own_dbmap_in_slice pwrsP pwrs }}}. @@ -145,7 +145,7 @@ Section program. by iFrame. Qed. - Theorem wp_logAccept (fname : string) (ts : u64) (rank : u64) (dec : bool) (bs : list u8) : + Theorem wp_logAccept (fname : byte_string) (ts : u64) (rank : u64) (dec : bool) (bs : list u8) : {{{ fname f↦ bs }}} logAccept #(LitString fname) #ts #rank #dec {{{ (bs' : list u8), RET #(); fname f↦ bs' }}}. diff --git a/src/program_proof/tulip/program/replica/replica_read.v b/src/program_proof/tulip/program/replica/replica_read.v index fae667528..38033183e 100644 --- a/src/program_proof/tulip/program/replica/replica_read.v +++ b/src/program_proof/tulip/program/replica/replica_read.v @@ -9,7 +9,7 @@ From Perennial.program_proof.tulip.program.index Require Import index. Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Theorem wp_Replica__Read (rp : loc) (tsW : u64) (key : string) gid rid γ : + Theorem wp_Replica__Read (rp : loc) (tsW : u64) (key : byte_string) gid rid γ : let ts := uint.nat tsW in ts ≠ O -> key ∈ keys_all -> diff --git a/src/program_proof/tulip/program/replica/replica_repr.v b/src/program_proof/tulip/program/replica/replica_repr.v index 071337743..cdb58c3a7 100644 --- a/src/program_proof/tulip/program/replica/replica_repr.v +++ b/src/program_proof/tulip/program/replica/replica_repr.v @@ -126,7 +126,7 @@ Section repr. "%Hexec" ∷ ⌜execute_cmds log = LocalState cm histm cpm ptgsm sptsm ptsm psm rkm⌝. Definition own_replica (rp : loc) (gid rid : u64) γ α : iProp Σ := - ∃ (cloga : dblog) (lsna : u64) (fname : string) (bs : list u8), + ∃ (cloga : dblog) (lsna : u64) (fname : byte_string) (bs : list u8), "Hrp" ∷ own_replica_with_cloga_no_lsna rp cloga gid rid γ α ∗ "Hlsna" ∷ rp ↦[Replica :: "lsna"] #lsna ∗ "HfnameP" ∷ rp ↦[Replica :: "fname"] #(LitString fname) ∗ diff --git a/src/program_proof/tulip/program/replica/start.v b/src/program_proof/tulip/program/replica/start.v index 55e7b30eb..ac7400d00 100644 --- a/src/program_proof/tulip/program/replica/start.v +++ b/src/program_proof/tulip/program/replica/start.v @@ -12,8 +12,8 @@ Section program. Context `{!heapGS Σ, !tulip_ghostG Σ, !paxos_ghostG Σ}. Theorem wp_Start - (rid : u64) (addr : chan) (fname : string) (addrmpxP : loc) (fnamepx : string) - (termc : u64) (terml : u64) (lsnc : u64) (log : list string) (addrmpx : gmap u64 chan) + (rid : u64) (addr : chan) (fname : byte_string) (addrmpxP : loc) (fnamepx : byte_string) + (termc : u64) (terml : u64) (lsnc : u64) (log : list byte_string) (addrmpx : gmap u64 chan) (addrm : gmap u64 chan) gid γ π : termc = (W64 0) -> terml = (W64 0) -> diff --git a/src/program_proof/tulip/program/tuple/res.v b/src/program_proof/tulip/program/tuple/res.v index 3a894250f..d0a64f574 100644 --- a/src/program_proof/tulip/program/tuple/res.v +++ b/src/program_proof/tulip/program/tuple/res.v @@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program Require Import prelude. Section res. Context `{!tulip_ghostG Σ}. - Definition own_phys_hist_half α (key : string) (hist : dbhist) : iProp Σ := + Definition own_phys_hist_half α (key : byte_string) (hist : dbhist) : iProp Σ := own α {[ key := (to_dfrac_agree (DfracOwn (1 / 2)) hist) ]}. Lemma phys_hist_update {α k h1 h2} h : diff --git a/src/program_proof/tulip/program/tuple/tuple.v b/src/program_proof/tulip/program/tuple/tuple.v index 962f52ae7..a99fc88bc 100644 --- a/src/program_proof/tulip/program/tuple/tuple.v +++ b/src/program_proof/tulip/program/tuple/tuple.v @@ -174,7 +174,7 @@ Section program. "#Hmu" ∷ readonly (tuple ↦[Tuple :: "mu"] #muP) ∗ "#Hlock" ∷ is_lock tulipNS #muP (own_tuple tuple key γ α). - Theorem wp_Tuple__AppendVersion (tuple : loc) (tsW : u64) (value : string) key hist γ α : + Theorem wp_Tuple__AppendVersion (tuple : loc) (tsW : u64) (value : byte_string) key hist γ α : let ts := uint.nat tsW in let hist' := last_extend ts hist ++ [Some value] in (length hist ≤ ts)%nat -> diff --git a/src/program_proof/tulip/program/txn/proph.v b/src/program_proof/tulip/program/txn/proph.v index c9b1769ed..fab41d503 100644 --- a/src/program_proof/tulip/program/txn/proph.v +++ b/src/program_proof/tulip/program/txn/proph.v @@ -4,7 +4,7 @@ From Perennial.goose_lang.trusted.github_com.mit_pdos.tulip Require Import trust Section proph. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Lemma wp_ResolveRead p (tid : u64) (key : string) (ts : nat) : + Lemma wp_ResolveRead p (tid : u64) (key : byte_string) (ts : nat) : ⊢ {{{ ⌜uint.nat tid = ts⌝ }}} <<< ∀∀ acs, own_txn_proph p acs >>> diff --git a/src/program_proof/tulip/program/txn/txn_getwrs.v b/src/program_proof/tulip/program/txn/txn_getwrs.v index 69be52b1f..831e20658 100644 --- a/src/program_proof/tulip/program/txn/txn_getwrs.v +++ b/src/program_proof/tulip/program/txn/txn_getwrs.v @@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program.txn Require Import txn_repr txn_key_t Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Theorem wp_Txn__getwrs (txn : loc) (key : string) q wrs : + Theorem wp_Txn__getwrs (txn : loc) (key : byte_string) q wrs : valid_key key -> {{{ own_txn_wrs txn q wrs }}} Txn__getwrs #txn #(LitString key) diff --git a/src/program_proof/tulip/program/txn/txn_key_to_group.v b/src/program_proof/tulip/program/txn/txn_key_to_group.v index 2a5b9a121..8f14a1719 100644 --- a/src/program_proof/tulip/program/txn/txn_key_to_group.v +++ b/src/program_proof/tulip/program/txn/txn_key_to_group.v @@ -6,7 +6,7 @@ Local Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations. Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Theorem wp_Txn__keyToGroup (txn : loc) (key : string) q wrs : + Theorem wp_Txn__keyToGroup (txn : loc) (key : byte_string) q wrs : valid_key key -> {{{ own_txn_wrs txn q wrs }}} Txn__keyToGroup #txn #(LitString key) @@ -30,7 +30,7 @@ Section program. rewrite /key_to_group. rewrite -size_dom Hdomwrs. pose proof size_gids_all as Hszall. - set x := String.length key. + set x := length key. set y := size gids_all. apply valid_key_length in Hvk. word. diff --git a/src/program_proof/tulip/program/txn/txn_setwrs.v b/src/program_proof/tulip/program/txn/txn_setwrs.v index 62d8a4489..e0cab4949 100644 --- a/src/program_proof/tulip/program/txn/txn_setwrs.v +++ b/src/program_proof/tulip/program/txn/txn_setwrs.v @@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program.txn Require Import txn_repr txn_key_t Section program. Context `{!heapGS Σ, !tulip_ghostG Σ}. - Theorem wp_Txn__setwrs (txn : loc) (key : string) (value : dbval) wrs : + Theorem wp_Txn__setwrs (txn : loc) (key : byte_string) (value : dbval) wrs : valid_key key -> {{{ own_txn_wrs txn (DfracOwn 1) wrs }}} Txn__setwrs #txn #(LitString key) (dbval_to_val value) diff --git a/src/program_proof/tulip/program/txnlog/txnlog.v b/src/program_proof/tulip/program/txnlog/txnlog.v index f93815f05..4e9b8fc52 100644 --- a/src/program_proof/tulip/program/txnlog/txnlog.v +++ b/src/program_proof/tulip/program/txnlog/txnlog.v @@ -252,7 +252,6 @@ Section program. exists (CmdAbort (uint.nat ts)). split; first set_solver. simpl. - rewrite bytes_to_string_to_bytes. rewrite /encode_abort_cmd. by rewrite w64_to_nat_id. } @@ -335,7 +334,7 @@ Section program. apply set_Forall_singleton. exists (CmdCommit (uint.nat ts) pwrs). split; first set_solver. - rewrite /= bytes_to_string_to_bytes -app_assoc. + rewrite /= -app_assoc. exists (u64_le ts ++ mdata). split; first done. exists mdata. @@ -369,8 +368,8 @@ Section program. Qed. Theorem wp_Start - (nidme : u64) (termc : u64) (terml : u64) (lsnc : u64) (log : list string) - (addrmP : loc) (addrm : gmap u64 chan) (fname : string) gid γ π : + (nidme : u64) (termc : u64) (terml : u64) (lsnc : u64) (log : list byte_string) + (addrmP : loc) (addrm : gmap u64 chan) (fname : byte_string) gid γ π : termc = (W64 0) -> terml = (W64 0) -> lsnc = (W64 0) -> diff --git a/src/program_proof/tulip/program/util/decode_string.v b/src/program_proof/tulip/program/util/decode_string.v index b1ed29898..37a97a36b 100644 --- a/src/program_proof/tulip/program/util/decode_string.v +++ b/src/program_proof/tulip/program/util/decode_string.v @@ -4,7 +4,7 @@ From Perennial.program_proof Require Import marshal_stateless_proof. Section program. Context `{!heapGS Σ, !paxos_ghostG Σ}. - Theorem wp_DecodeString (bsP : Slice.t) (s : string) (bstail : list u8) : + Theorem wp_DecodeString (bsP : Slice.t) (s : byte_string) (bstail : list u8) : {{{ own_slice_small bsP byteT (DfracOwn 1) (encode_string s ++ bstail) }}} DecodeString (to_val bsP) {{{ (dataP : Slice.t), RET (#(LitString s), (to_val dataP)); diff --git a/src/program_proof/tulip/program/util/decode_strings.v b/src/program_proof/tulip/program/util/decode_strings.v index c73e79b38..3e0ad2e9a 100644 --- a/src/program_proof/tulip/program/util/decode_strings.v +++ b/src/program_proof/tulip/program/util/decode_strings.v @@ -5,7 +5,7 @@ From Perennial.program_proof Require Import marshal_stateless_proof. Section program. Context `{!heapGS Σ, !paxos_ghostG Σ}. - Theorem wp_DecodeStrings (bsP : Slice.t) (strs : list string) (bstail : list u8) : + Theorem wp_DecodeStrings (bsP : Slice.t) (strs : list byte_string) (bstail : list u8) : {{{ own_slice_small bsP byteT (DfracOwn 1) (encode_strings strs ++ bstail) }}} DecodeStrings (to_val bsP) {{{ (strsP : Slice.t) (dataP : Slice.t), RET (to_val strsP, to_val dataP); diff --git a/src/program_proof/tulip/program/util/encode_string.v b/src/program_proof/tulip/program/util/encode_string.v index a05cf49f8..82e464120 100644 --- a/src/program_proof/tulip/program/util/encode_string.v +++ b/src/program_proof/tulip/program/util/encode_string.v @@ -29,7 +29,7 @@ Section program. wp_pures. iApply "HΦ". iFrame. - by rewrite -app_assoc /encode_string string_bytes_length. + by rewrite -app_assoc /encode_string. Qed. End program. diff --git a/src/program_proof/vrsm/apps/closed_proof.v b/src/program_proof/vrsm/apps/closed_proof.v index 66ec2bb64..ebad04cd5 100644 --- a/src/program_proof/vrsm/apps/closed_proof.v +++ b/src/program_proof/vrsm/apps/closed_proof.v @@ -58,7 +58,7 @@ Qed. Local Instance subG_ekvΣ {Σ} : subG kv_pbΣ Σ → ekvG Σ. Proof. intros. solve_inG. Qed. -Definition replica_fname := "kv.data". +Definition replica_fname := "kv.data"%go. (* FIXME: put this in the file that defines ekvΣ? *) Opaque ekvΣ. @@ -147,7 +147,7 @@ Proof. (* Allocate the kv system used for storing data *) iMod (alloc_vkv (ekvParams.mk [dr1Host ; dr2Host ]) [(dconfigHost, dconfigHostPaxos)] - {[ "init"; "a1"; "a2" ]} with "[Hd1 Hd2]") as "[Hdkv Hdconf]"; try (simpl; lia). + {[ "init"; "a1"; "a2" ]}%go with "[Hd1 Hd2]") as "[Hdkv Hdconf]"; try (simpl; lia). { rewrite /own_chans /=. repeat iDestruct (wand_refl (_ ∗ _) with "[$]") as "[? ?]". @@ -158,7 +158,7 @@ Proof. (* Allocate the kv system used as a lockservice *) iMod (alloc_vkv (ekvParams.mk [lr1Host ; lr2Host ]) [(lconfigHost, lconfigHostPaxos)] - {[ "init"; "a1"; "a2" ]} with "[Hl1 Hl2]") as "[Hlkv Hlconf]"; try (simpl; lia). + {[ "init"; "a1"; "a2" ]}%go with "[Hl1 Hl2]") as "[Hlkv Hlconf]"; try (simpl; lia). { rewrite /own_chans /=. repeat iDestruct (wand_refl (_ ∗ _) with "[$]") as "[? ?]". @@ -168,21 +168,21 @@ Proof. iSimpl in "Hlhost". (* set up bank *) - iAssert (|={⊤}=> is_bank "init" _ _ {[ "a1" ; "a2" ]})%I with "[Hlkvs Hkvs]" as ">#Hbank". + iAssert (|={⊤}=> is_bank "init"%go _ _ {[ "a1"%go ; "a2"%go ]})%I with "[Hlkvs Hkvs]" as ">#Hbank". { - iDestruct (big_sepS_delete _ _ "init" with "Hlkvs") as "(Hinit&Hlkvs)". + iDestruct (big_sepS_delete _ _ "init"%go with "Hlkvs") as "(Hinit&Hlkvs)". { set_solver. } instantiate (2:=Build_lock_names (kv_ptsto γl)). rewrite /is_bank. iMod (lock_alloc lockN {| kvptsto_lock := kv_ptsto γl |} _ "init" with "[Hinit] [-]") as "$"; last done. { iFrame. } - iDestruct (big_sepS_delete _ _ "init" with "Hkvs") as "(Hinit&Hkvs)". + iDestruct (big_sepS_delete _ _ "init"%go with "Hkvs") as "(Hinit&Hkvs)". { set_solver. } iLeft. instantiate (1:=kv_ptsto γd). iFrame. iApply (big_sepS_sep). - eassert (_ ∖ _ = {[ "a1"; "a2" ]}) as ->. + eassert (_ ∖ _ = {[ "a1"; "a2" ]}%go) as ->. { set_solver. } iFrame. } diff --git a/src/program_proof/vrsm/apps/closed_wpcs.v b/src/program_proof/vrsm/apps/closed_wpcs.v index ffa63b86a..e53316a12 100644 --- a/src/program_proof/vrsm/apps/closed_wpcs.v +++ b/src/program_proof/vrsm/apps/closed_wpcs.v @@ -321,11 +321,11 @@ Lemma wp_makeBankClerk γlk γkv (kvParams1 kvParams2:ekvParams.t): {{{ "#Hhost1" ∷ is_kv_config_hosts (params:=kvParams1) [dconfigHost] γkv ∗ "#Hhost2" ∷ is_kv_config_hosts (params:=kvParams2) [lconfigHost] γlk ∗ - "#Hbank" ∷ is_bank "init" (Build_lock_names (kv_ptsto γlk)) (kv_ptsto γkv) {[ "a1"; "a2" ]} + "#Hbank" ∷ is_bank "init"%go (Build_lock_names (kv_ptsto γlk)) (kv_ptsto γkv) {[ "a1"%go; "a2"%go ]} }}} makeBankClerk #() {{{ - (b:loc), RET #b; own_bank_clerk b {[ "a1" ; "a2" ]} + (b:loc), RET #b; own_bank_clerk b {[ "a1"%go ; "a2"%go ]} }}} . Proof. @@ -364,7 +364,7 @@ Definition bank_pre : iProp Σ := ∃ γkv γlk (p1 p2:ekvParams.t), "#Hhost1" ∷ is_kv_config_hosts (params:=p1)[dconfigHost] γkv ∗ "#Hhost2" ∷ is_kv_config_hosts (params:=p2) [lconfigHost] γlk ∗ - "#Hbank" ∷ is_bank "init" (Build_lock_names (kv_ptsto γlk)) (kv_ptsto γkv) {[ "a1"; "a2" ]} + "#Hbank" ∷ is_bank "init"%go (Build_lock_names (kv_ptsto γlk)) (kv_ptsto γkv) {[ "a1"%go; "a2"%go ]} . Lemma wp_bank_transferer_main : @@ -703,7 +703,7 @@ Lemma alloc_vkv (params:ekvParams.t) configHostPairs allocated `{!ekvG Σ}: ={⊤}=∗ (∃ γ, (* system-wide: allows clients to connect to the system, and gives them ownership of keys *) - ([∗ set] k ∈ allocated, kv_ptsto γ k "") ∗ + ([∗ set] k ∈ allocated, kv_ptsto γ k ""%go) ∗ is_kv_config_hosts (configHostPairs.*1) γ ∗ (* for each kv replica server: *) @@ -729,7 +729,7 @@ Proof. iMod (alloc_simplepb_system configHostPairs with "[$Hchan] [$HconfChan]") as (?) "H"; try done. iDestruct "H" as "(Hlog & #Hhosts & Hsrvs & HconfSrvs)". iFrame "HconfSrvs". - iMod (ghost_map_alloc (gset_to_gmap "" allocated)) as (γkv_gn) "[Hauth Hkvs]". + iMod (ghost_map_alloc (gset_to_gmap ""%go allocated)) as (γkv_gn) "[Hauth Hkvs]". iExists (Build_kv_names _ _). rewrite big_sepM_gset_to_gmap. iFrame "Hkvs". diff --git a/src/program_proof/vrsm/apps/vkv/kv_proof.v b/src/program_proof/vrsm/apps/vkv/kv_proof.v index cc3a52ee8..ccdfc21ee 100644 --- a/src/program_proof/vrsm/apps/vkv/kv_proof.v +++ b/src/program_proof/vrsm/apps/vkv/kv_proof.v @@ -66,7 +66,7 @@ Context `{!ekvG Σ}. [getOp] doing [default []]. *) Definition own_kvs γ ops : iProp Σ := ∃ allocatedKeys, - ghost_map_auth γ.(kv_gn) 1 (compute_state ops ∪ gset_to_gmap "" allocatedKeys) + ghost_map_auth γ.(kv_gn) 1 (compute_state ops ∪ gset_to_gmap ""%go allocatedKeys) . Definition stateN := nroot .@ "state". @@ -280,14 +280,13 @@ Proof. iIntros (?) "Hck Hsl". wp_apply (wp_StringFromBytes with "[$]"). iIntros "_". - simpl. rewrite string_to_bytes_to_string /=. rewrite lookup_union in Hlook. + simpl. destruct (compute_state ops !! key) as [x|]; simpl. - simpl in Hlook. rewrite union_Some_l in Hlook. injection Hlook as <-. iApply "HΦ". repeat iExists _. iFrame "∗#". - - - rewrite left_id lookup_gset_to_gmap_Some in Hlook. + - rewrite left_id lookup_gset_to_gmap_Some in Hlook. destruct Hlook as [? ?]; subst. iApply "HΦ". repeat iExists _. iFrame "∗#". Qed. @@ -307,7 +306,7 @@ Lemma wp_Clerk__CondPut ck γkv key expect val : <<< ∀∀ old_value, kv_ptsto γkv key old_value >>> Clerk__CondPut #ck #(str key) #(str expect) #(str val) @ (↑pbN ∪ ↑prophReadN ∪ ↑esmN ∪ ↑stateN) <<< kv_ptsto γkv key (if bool_decide (expect = old_value) then val else old_value) >>> - {{{ RET #(str (if bool_decide (expect = old_value) then "ok" else "")); own_Clerk ck γkv }}}. + {{{ RET #(str (if bool_decide (expect = old_value) then "ok"%go else ""%go)); own_Clerk ck γkv }}}. Proof. iIntros "%Φ !# Hck Hupd". wp_rec. diff --git a/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v b/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v index 27bf49cd8..b93f884da 100644 --- a/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v +++ b/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v @@ -13,9 +13,9 @@ From Perennial.algebra Require Import map. Section defns. Inductive kvOp := - | putOp : byte_string → byte_string → kvOp - | getOp : byte_string → kvOp - | condPutOp : byte_string → byte_string → byte_string → kvOp + | putOp (k : byte_string) (v : byte_string) : kvOp + | getOp (k : byte_string) : kvOp + | condPutOp (k : byte_string) (e : byte_string) (v : byte_string) : kvOp . Definition apply_op (state:gmap byte_string byte_string) (op:kvOp) := @@ -504,17 +504,17 @@ Proof. iModIntro. iIntros. rewrite /typed_map.map_insert /= in H0. - destruct (decide (k = s0)). + destruct (decide (k = k0)). { subst. rewrite lookup_insert /= in H0. replace (vnum) with (vnum') by word. iExists _. by iDestruct "Hintermediate" as "[_ $]". } - assert (compute_reply (ops ++ [putOp s0 s1]) (getOp k) = - compute_reply (ops) (getOp k)) as Heq; last setoid_rewrite Heq. + assert (compute_reply (ops ++ [putOp k v]) (getOp k0) = + compute_reply (ops) (getOp k0)) as Heq; last setoid_rewrite Heq. { rewrite /compute_reply /= /compute_state. rewrite foldl_snoc /=. - by rewrite lookup_insert_ne. + rewrite lookup_insert_ne //. } rewrite lookup_insert_ne in H0; last done. destruct (decide (uint.nat vnum' <= uint.nat latestVnum)). @@ -536,7 +536,7 @@ Proof. } { iPureIntro. intros. - destruct (decide (k = s0)). + destruct (decide (k = k0)). { subst. by rewrite /typed_map.map_insert lookup_insert /=. } @@ -590,7 +590,7 @@ Proof. iSplitL. 2: { iPureIntro. intros. - destruct (decide (k = s0)). + destruct (decide (k = k0)). { subst. by rewrite /typed_map.map_insert lookup_insert /=. } { rewrite /typed_map.map_insert lookup_insert_ne /=; last done. @@ -601,13 +601,13 @@ Proof. iModIntro. iIntros. rewrite /typed_map.map_insert /= in H0. - destruct (decide (k = s0)). + destruct (decide (k = k0)). { subst. rewrite lookup_insert /= in H0. replace (vnum) with (vnum') by word. iExists _. by iDestruct "Hintermediate" as "[_ $]". } - eassert (compute_reply (ops ++ [_]) (getOp k) = - compute_reply (ops) (getOp k)) as Heq; last setoid_rewrite Heq. + eassert (compute_reply (ops ++ [_]) (getOp k0) = + compute_reply (ops) (getOp k0)) as Heq; last setoid_rewrite Heq. { rewrite /compute_reply /= /compute_state. rewrite foldl_snoc /=. done. @@ -690,13 +690,13 @@ Proof. iModIntro. iIntros. rewrite /typed_map.map_insert /= in H0. - destruct (decide (k = s0)). + destruct (decide (k = k0)). { subst. rewrite lookup_insert /= in H1. replace (vnum) with (vnum') by word. iExists _. by iDestruct "Hintermediate" as "[_ $]". } - eassert (compute_reply (ops ++ [condPutOp s0 _ s2]) (getOp k) = - compute_reply (ops) (getOp k)) as Heq; last setoid_rewrite Heq. + eassert (compute_reply (ops ++ [condPutOp k _ _]) (getOp k0) = + compute_reply (ops) (getOp k0)) as Heq; last setoid_rewrite Heq. { rewrite /compute_reply /= /compute_state. rewrite foldl_snoc /=. @@ -726,7 +726,7 @@ Proof. } { iPureIntro. intros. - destruct (decide (k = s0)). + destruct (decide (k = k0)). { subst. by rewrite /typed_map.map_insert lookup_insert /=. } @@ -746,8 +746,6 @@ Proof. wp_apply wp_StringToBytes. injection Hlookup as <-. iIntros (?) "Hreply_sl". - assert (default "" (foldl apply_op ∅ ops !! s0) ≠ s1) as Hnot. - { intros x. apply Heqb. repeat f_equal. done. } iApply "HΦ". iSplitL "Hkvs Hkvs_map Hvnums HminVnum Hvnums_map". { @@ -762,7 +760,7 @@ Proof. iModIntro. iIntros. iDestruct "Hintermediate" as "[Hintermediate Hcurst]". - assert (compute_state (ops ++ [condPutOp s0 s1 s2]) + assert (compute_state (ops ++ [condPutOp k e v]) = (compute_state ops)) as Heq. { rewrite /compute_state foldl_snoc /=. rewrite decide_False; done. @@ -787,7 +785,7 @@ Proof. } { iPureIntro. intros. - specialize (Hle k). + specialize (Hle k0). word. } } @@ -850,7 +848,7 @@ Proof. { wp_pures. iApply "HΦ". iModIntro. apply map_get_true in Hlookup. - pose proof (Hle s0) as Hle2. + pose proof (Hle k) as Hle2. rewrite Hlookup /= in Hle2. iSplitR. { word. } injection Hkv_lookup as <- ?. @@ -858,7 +856,7 @@ Proof. rewrite /kv_record /compute_reply /= /compute_state /=. iSplitL. { repeat iExists _; iFrame "∗#%". } - iSpecialize ("Hst" $! s0). + iSpecialize ("Hst" $! k). rewrite Hlookup /=. iModIntro. iIntros. iApply "Hst". @@ -869,7 +867,7 @@ Proof. wp_loadField. wp_pures. iApply "HΦ". iModIntro. apply map_get_false in Hlookup as [Hlookup Hv]. subst. - pose proof (Hle s0) as Hle2. + pose proof (Hle k) as Hle2. rewrite Hlookup /= in Hle2. iSplitR. { word. } injection Hkv_lookup as <- ?. @@ -877,7 +875,7 @@ Proof. rewrite /kv_record /compute_reply /= /compute_state /=. iSplitL. { repeat iExists _; iFrame "∗#%". } - iSpecialize ("Hst" $! s0). + iSpecialize ("Hst" $! k). rewrite Hlookup /=. iModIntro. iIntros. iApply "Hst".