diff --git a/external/Goose/github_com/mit_pdos/tulip/gcoord.v b/external/Goose/github_com/mit_pdos/tulip/gcoord.v index 9b8395ab0..62cf798d0 100644 --- a/external/Goose/github_com/mit_pdos/tulip/gcoord.v +++ b/external/Goose/github_com/mit_pdos/tulip/gcoord.v @@ -799,6 +799,12 @@ Definition GroupCoordinator__GetLeader: val := Mutex__Unlock (struct.loadF GroupCoordinator "mu" "gcoord");; SliceGet uint64T (struct.loadF GroupCoordinator "rps" "gcoord") "idxleader". +Definition GroupCoordinator__SendCommit: val := + rec: "GroupCoordinator__SendCommit" "gcoord" "rid" "ts" "pwrs" := + let: "data" := message.EncodeTxnCommitRequest "ts" "pwrs" in + GroupCoordinator__Send "gcoord" "rid" "data";; + #(). + Definition GroupCoordinator__Finalized: val := rec: "GroupCoordinator__Finalized" "gcoord" "ts" := Mutex__Lock (struct.loadF GroupCoordinator "mu" "gcoord");; @@ -806,12 +812,6 @@ Definition GroupCoordinator__Finalized: val := Mutex__Unlock (struct.loadF GroupCoordinator "mu" "gcoord");; (~ "ok"). -Definition GroupCoordinator__SendCommit: val := - rec: "GroupCoordinator__SendCommit" "gcoord" "rid" "ts" "pwrs" := - let: "data" := message.EncodeTxnCommitRequest "ts" "pwrs" in - GroupCoordinator__Send "gcoord" "rid" "data";; - #(). - Definition GroupCoordinator__ChangeLeader: val := rec: "GroupCoordinator__ChangeLeader" "gcoord" := Mutex__Lock (struct.loadF GroupCoordinator "mu" "gcoord");; @@ -824,11 +824,13 @@ Definition GroupCoordinator__Commit: val := rec: "GroupCoordinator__Commit" "gcoord" "ts" "pwrs" := GroupCoordinator__RegisterFinalization "gcoord" "ts";; let: "leader" := ref_to uint64T (GroupCoordinator__GetLeader "gcoord") in + GroupCoordinator__SendCommit "gcoord" (![uint64T] "leader") "ts" "pwrs";; + time.Sleep params.NS_RESEND_COMMIT;; Skip;; (for: (λ: <>, (~ (GroupCoordinator__Finalized "gcoord" "ts"))); (λ: <>, Skip) := λ: <>, + "leader" <-[uint64T] (GroupCoordinator__ChangeLeader "gcoord");; GroupCoordinator__SendCommit "gcoord" (![uint64T] "leader") "ts" "pwrs";; time.Sleep params.NS_RESEND_COMMIT;; - "leader" <-[uint64T] (GroupCoordinator__ChangeLeader "gcoord");; Continue);; #(). @@ -842,10 +844,12 @@ Definition GroupCoordinator__Abort: val := rec: "GroupCoordinator__Abort" "gcoord" "ts" := GroupCoordinator__RegisterFinalization "gcoord" "ts";; let: "leader" := ref_to uint64T (GroupCoordinator__GetLeader "gcoord") in + GroupCoordinator__SendAbort "gcoord" (![uint64T] "leader") "ts";; + time.Sleep params.NS_RESEND_ABORT;; Skip;; (for: (λ: <>, (~ (GroupCoordinator__Finalized "gcoord" "ts"))); (λ: <>, Skip) := λ: <>, + "leader" <-[uint64T] (GroupCoordinator__ChangeLeader "gcoord");; GroupCoordinator__SendAbort "gcoord" (![uint64T] "leader") "ts";; time.Sleep params.NS_RESEND_ABORT;; - "leader" <-[uint64T] (GroupCoordinator__ChangeLeader "gcoord");; Continue);; #(). diff --git a/external/Goose/github_com/mit_pdos/tulip/message.v b/external/Goose/github_com/mit_pdos/tulip/message.v index 3e01560ba..485d6c3b7 100644 --- a/external/Goose/github_com/mit_pdos/tulip/message.v +++ b/external/Goose/github_com/mit_pdos/tulip/message.v @@ -50,6 +50,10 @@ Definition MSG_TXN_COMMIT : expr := #300. Definition MSG_TXN_ABORT : expr := #301. +Definition MSG_DUMP_STATE : expr := #10000. + +Definition MSG_FORCE_ELECTION : expr := #10001. + Definition EncodeTxnReadRequest: val := rec: "EncodeTxnReadRequest" "ts" "key" := let: "bs" := NewSliceWithCap byteT #0 #32 in @@ -332,6 +336,33 @@ Definition DecodeTxnCommitRequest: val := "PartialWrites" ::= "pwrs" ]. +Definition EncodeDumpStateRequest: val := + rec: "EncodeDumpStateRequest" "gid" := + let: "bs" := NewSliceWithCap byteT #0 #16 in + let: "bs1" := marshal.WriteInt "bs" MSG_DUMP_STATE in + let: "data" := marshal.WriteInt "bs1" "gid" in + "data". + +Definition DecodeDumpStateRequest: val := + rec: "DecodeDumpStateRequest" "bs" := + let: ("gid", <>) := marshal.ReadInt "bs" in + struct.mk TxnRequest [ + "Kind" ::= MSG_DUMP_STATE; + "Timestamp" ::= "gid" + ]. + +Definition EncodeForceElectionRequest: val := + rec: "EncodeForceElectionRequest" <> := + let: "bs" := NewSliceWithCap byteT #0 #8 in + let: "data" := marshal.WriteInt "bs" MSG_FORCE_ELECTION in + "data". + +Definition DecodeForceElectionRequest: val := + rec: "DecodeForceElectionRequest" <> := + struct.mk TxnRequest [ + "Kind" ::= MSG_FORCE_ELECTION + ]. + Definition EncodeTxnCommitResponse: val := rec: "EncodeTxnCommitResponse" "ts" "res" := let: "bs" := NewSliceWithCap byteT #0 #24 in @@ -413,8 +444,14 @@ Definition DecodeTxnRequest: val := (if: "kind" = MSG_TXN_ABORT then DecodeTxnAbortRequest "bs1" else - struct.mk TxnRequest [ - ]))))))))). + (if: "kind" = MSG_DUMP_STATE + then DecodeDumpStateRequest "bs1" + else + (if: "kind" = MSG_FORCE_ELECTION + then DecodeForceElectionRequest #() + else + struct.mk TxnRequest [ + ]))))))))))). Definition DecodeTxnResponse: val := rec: "DecodeTxnResponse" "bs" := diff --git a/external/Goose/github_com/mit_pdos/tulip/params.v b/external/Goose/github_com/mit_pdos/tulip/params.v index dae80165f..f6136a664 100644 --- a/external/Goose/github_com/mit_pdos/tulip/params.v +++ b/external/Goose/github_com/mit_pdos/tulip/params.v @@ -6,15 +6,15 @@ Context `{ext_ty: ext_types}. Definition N_SHARDS : expr := #2. -Definition NS_RECONNECT : expr := #10000000. +Definition NS_RECONNECT : expr := #100000000. Definition NS_RESEND_PREPARE : expr := #500000000. -Definition NS_RESEND_READ : expr := #20000000. +Definition NS_RESEND_READ : expr := #400000000. -Definition NS_RESEND_COMMIT : expr := #40000000. +Definition NS_RESEND_COMMIT : expr := #400000000. -Definition NS_RESEND_ABORT : expr := #40000000. +Definition NS_RESEND_ABORT : expr := #400000000. Definition NS_SPAWN_BACKUP_BASE : expr := #5000000000. @@ -30,10 +30,10 @@ Definition NS_ELECTION_TIMEOUT_BASE : expr := #2000000000. Definition NS_ELECTION_TIMEOUT_DELTA : expr := #1000000000. -Definition N_RETRY_REPLICATED : expr := #10. +Definition N_RETRY_REPLICATED : expr := #500. -Definition NS_REPLICATED_INTERVAL : expr := #1000000. +Definition NS_REPLICATED_INTERVAL : expr := #10000. -Definition N_TXN_SITES : expr := #64. +Definition N_TXN_SITES : expr := #1024. End code. diff --git a/external/Goose/github_com/mit_pdos/tulip/paxos.v b/external/Goose/github_com/mit_pdos/tulip/paxos.v index 511eedb77..dbb644c55 100644 --- a/external/Goose/github_com/mit_pdos/tulip/paxos.v +++ b/external/Goose/github_com/mit_pdos/tulip/paxos.v @@ -750,6 +750,44 @@ Definition Paxos__ConnectAll: val := (Paxos__Connect "px" "nid");; #(). +Definition Paxos__DumpState: val := + rec: "Paxos__DumpState" "px" := + Mutex__Lock (struct.loadF Paxos "mu" "px");; + (* fmt.Printf("Current term: %d\n", px.termc) *) + (* fmt.Printf("Ledger term: %d\n", px.terml) *) + (* fmt.Printf("Number of log entries: %d\n", uint64(len(px.log))) *) + (* fmt.Printf("Committed LSN: %d\n", px.lsnc) *) + (* fmt.Printf("Is candidate / leader: %t / %t\n", px.iscand, px.isleader) *) + (if: struct.loadF Paxos "iscand" "px" + then + (* fmt.Printf("Candidate state:\n") *) + (* fmt.Printf("Largest term seen in prepare: %d\n", px.termp) *) + (* fmt.Printf("Longest log after committed LSN in prepare: %d\n", px.termp) *) + (* fmt.Printf("Number of votes granted: %d\n", uint64(len(px.respp))) *) + #() + else #());; + (if: struct.loadF Paxos "isleader" "px" + then + (* fmt.Printf("Leader state:\n") *) + (* fmt.Printf("Match LSN for each peer:\n") *) + MapIter (struct.loadF Paxos "lsnpeers" "px") (λ: "nid" "lsnpeer", + (* fmt.Printf("Peer %d -> %d\n", nid, lsnpeer) *) + #()) + else #());; + Mutex__Unlock (struct.loadF Paxos "mu" "px");; + #(). + +Definition Paxos__ForceElection: val := + rec: "Paxos__ForceElection" "px" := + Mutex__Lock (struct.loadF Paxos "mu" "px");; + let: ("termc", "lsnc") := Paxos__nominate "px" in + Mutex__Unlock (struct.loadF Paxos "mu" "px");; + ForSlice uint64T <> "nidloop" (struct.loadF Paxos "peers" "px") + (let: "nid" := "nidloop" in + Fork (let: "data" := EncodePrepareRequest "termc" "lsnc" in + Paxos__Send "px" "nid" "data"));; + #(). + Definition mkPaxos: val := rec: "mkPaxos" "nidme" "termc" "terml" "lsnc" "log" "addrm" "fname" := let: "sc" := MapLen "addrm" in diff --git a/external/Goose/github_com/mit_pdos/tulip/replica.v b/external/Goose/github_com/mit_pdos/tulip/replica.v index dc3cbac83..f5e25fc7e 100644 --- a/external/Goose/github_com/mit_pdos/tulip/replica.v +++ b/external/Goose/github_com/mit_pdos/tulip/replica.v @@ -64,7 +64,7 @@ Definition Replica__Commit: val := then #true else let: ("lsn", "term") := txnlog.TxnLog__SubmitCommit (struct.loadF Replica "txnlog" "rp") "ts" "pwrs" in - (if: "lsn" = #0 + (if: "term" = #0 then #false else let: "safe" := txnlog.TxnLog__WaitUntilSafe (struct.loadF Replica "txnlog" "rp") "lsn" "term" in @@ -84,7 +84,7 @@ Definition Replica__Abort: val := then #true else let: ("lsn", "term") := txnlog.TxnLog__SubmitAbort (struct.loadF Replica "txnlog" "rp") "ts" in - (if: "lsn" = #0 + (if: "term" = #0 then #false else let: "safe" := txnlog.TxnLog__WaitUntilSafe (struct.loadF Replica "txnlog" "rp") "lsn" "term" in @@ -547,6 +547,29 @@ Definition Replica__StartBackupTxnCoordinator: val := backup.BackupTxnCoordinator__Finalize "tcoord";; #(). +(* For debugging and evaluation purpose. *) +Definition Replica__DumpState: val := + rec: "Replica__DumpState" "rp" "gid" := + Mutex__Lock (struct.loadF Replica "mu" "rp");; + (* fmt.Printf("@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@\n") *) + (* fmt.Printf("[G %d / R %d] Dumping replica state:\n", gid, rp.rid) *) + (* fmt.Printf("-------------------------------------------------------------\n") *) + (* fmt.Printf("Number of finalized txns: %d\n", uint64(len(rp.txntbl))) *) + (* fmt.Printf("Number of prepared txns: %d\n", uint64(len(rp.prepm))) *) + (* fmt.Printf("Number of acquired keys: %d\n", uint64(len(rp.ptsm))) *) + (* fmt.Printf("Applied LSN: %d\n\n", rp.lsna) *) + (* fmt.Printf("[G %d / R %d] Dumping paxos state:\n", gid, rp.rid) *) + (* fmt.Printf("-------------------------------------------------------------\n") *) + txnlog.TxnLog__DumpState (struct.loadF Replica "txnlog" "rp");; + (* fmt.Printf("@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@\n") *) + Mutex__Unlock (struct.loadF Replica "mu" "rp");; + #(). + +Definition Replica__ForceElection: val := + rec: "Replica__ForceElection" "rp" := + txnlog.TxnLog__ForceElection (struct.loadF Replica "txnlog" "rp");; + #(). + Definition Replica__RequestSession: val := rec: "Replica__RequestSession" "rp" "conn" := Skip;; @@ -636,7 +659,18 @@ Definition Replica__RequestSession: val := let: "data" := message.EncodeTxnAbortResponse "ts" tulip.REPLICA_WRONG_LEADER in grove_ffi.Send "conn" "data";; Continue) - else Continue))))))))));; + else + (if: "kind" = message.MSG_DUMP_STATE + then + let: "gid" := struct.get message.TxnRequest "Timestamp" "req" in + Replica__DumpState "rp" "gid";; + Continue + else + (if: "kind" = message.MSG_FORCE_ELECTION + then + Replica__ForceElection "rp";; + Continue + else Continue))))))))))));; #(). Definition Replica__Serve: val := diff --git a/external/Goose/github_com/mit_pdos/tulip/txnlog.v b/external/Goose/github_com/mit_pdos/tulip/txnlog.v index a4bfa146b..4b74f07c9 100644 --- a/external/Goose/github_com/mit_pdos/tulip/txnlog.v +++ b/external/Goose/github_com/mit_pdos/tulip/txnlog.v @@ -43,7 +43,7 @@ Definition TXNLOG_COMMIT : expr := #1. be done in a general way, without relying on the content. *) Definition TxnLog__SubmitCommit: val := rec: "TxnLog__SubmitCommit" "log" "ts" "pwrs" := - let: "bs" := NewSliceWithCap byteT #0 #32 in + let: "bs" := NewSliceWithCap byteT #0 #64 in let: "bs1" := marshal.WriteInt "bs" TXNLOG_COMMIT in let: "bs2" := marshal.WriteInt "bs1" "ts" in let: "data" := util.EncodeKVMapFromSlice "bs2" "pwrs" in @@ -110,6 +110,16 @@ Definition TxnLog__Lookup: val := (struct.mk Cmd [ ], #false)))). +Definition TxnLog__DumpState: val := + rec: "TxnLog__DumpState" "log" := + paxos.Paxos__DumpState (struct.loadF TxnLog "px" "log");; + #(). + +Definition TxnLog__ForceElection: val := + rec: "TxnLog__ForceElection" "log" := + paxos.Paxos__ForceElection (struct.loadF TxnLog "px" "log");; + #(). + Definition Start: val := rec: "Start" "nidme" "addrm" "fname" := let: "px" := paxos.Start "nidme" "addrm" "fname" in diff --git a/src/program_proof/tulip/inv_txnsys.v b/src/program_proof/tulip/inv_txnsys.v index 906dd27dd..77665e6cc 100644 --- a/src/program_proof/tulip/inv_txnsys.v +++ b/src/program_proof/tulip/inv_txnsys.v @@ -388,7 +388,7 @@ Section tidinv. Context `{!heapGS Σ}. Context `{!tulip_ghostG Σ}. - Definition zN_TXN_SITES : Z := 64. + Definition zN_TXN_SITES : Z := 1024. Definition sid_of (ts: u64) : u64 := word.modu ts (W64 zN_TXN_SITES). diff --git a/src/program_proof/tulip/program/gcoord/gcoord_abort.v b/src/program_proof/tulip/program/gcoord/gcoord_abort.v index caf1e552f..2af2c8e2c 100644 --- a/src/program_proof/tulip/program/gcoord/gcoord_abort.v +++ b/src/program_proof/tulip/program/gcoord/gcoord_abort.v @@ -23,13 +23,29 @@ Section program. (*@ @*) wp_apply (wp_GroupCoordinator__RegisterFinalization with "Hgcoord"). iNamed "Hgcoord". + + (*@ var leader = gcoord.GetLeader() @*) + (*@ gcoord.SendAbort(leader, ts) @*) + (*@ primitive.Sleep(params.NS_RESEND_ABORT) @*) + (*@ @*) wp_apply (wp_GroupCoordinator__GetLeader with "Hgcoord"). iIntros (leader Hleader). wp_apply wp_ref_to; first by auto. iIntros (leaderP) "HleaderP". - wp_pures. + wp_load. + wp_apply (wp_GroupCoordinator__SendAbort with "Habted Hgcoord"). + { apply Hleader. } + wp_apply wp_Sleep. + + (*@ for !gcoord.Finalized(ts) { @*) + (*@ // Retry with different leaders until success. @*) + (*@ leader = gcoord.ChangeLeader() @*) + (*@ gcoord.SendAbort(leader, ts) @*) + (*@ primitive.Sleep(params.NS_RESEND_ABORT) @*) + (*@ } @*) + (*@ } @*) + - (*@ var leader = gcoord.GetLeader() @*) (*@ for !gcoord.Finalized(ts) { @*) (*@ gcoord.SendAbort(leader, ts) @*) (*@ primitive.Sleep(params.NS_RESEND_ABORT) @*) @@ -49,15 +65,14 @@ Section program. destruct finalized; wp_pures. { by iApply "HΦ". } iDestruct "HP" as (leader') "[HleaderP %Hin]". - wp_load. - wp_apply (wp_GroupCoordinator__SendAbort with "Habted"). - { apply Hin. } - { iFrame "Hgcoord". } - wp_apply wp_Sleep. - wp_apply (wp_GroupCoordinator__ChangeLeader). - { iFrame "Hgcoord". } + wp_apply (wp_GroupCoordinator__ChangeLeader with "Hgcoord"). iIntros (leadernew Hleadernew). wp_store. + wp_load. + wp_apply (wp_GroupCoordinator__SendAbort with "Habted Hgcoord"). + { apply Hleadernew. } + wp_apply wp_Sleep. + wp_pures. iApply "HΦ". by iFrame. } diff --git a/src/program_proof/tulip/program/gcoord/gcoord_commit.v b/src/program_proof/tulip/program/gcoord/gcoord_commit.v index 6be97b995..dc2897b2e 100644 --- a/src/program_proof/tulip/program/gcoord/gcoord_commit.v +++ b/src/program_proof/tulip/program/gcoord/gcoord_commit.v @@ -23,19 +23,27 @@ Section program. (*@ gcoord.RegisterFinalization(ts) @*) (*@ @*) wp_apply (wp_GroupCoordinator__RegisterFinalization with "Hgcoord"). + + (*@ var leader = gcoord.GetLeader() @*) + (*@ gcoord.SendCommit(leader, ts, pwrs) @*) + (*@ primitive.Sleep(params.NS_RESEND_COMMIT) @*) + (*@ @*) iNamed "Hgcoord". wp_apply (wp_GroupCoordinator__GetLeader with "Hgcoord"). iIntros (leader Hleader). wp_apply wp_ref_to; first by auto. iIntros (leaderP) "HleaderP". - wp_pures. + wp_load. + wp_apply (wp_GroupCoordinator__SendCommit with "Hcmted Hgcoord Hpwrs"). + { apply Hleader. } + iIntros "Hpwrs". + wp_apply wp_Sleep. - (*@ var leader = gcoord.GetLeader() @*) (*@ for !gcoord.Finalized(ts) { @*) - (*@ gcoord.SendCommit(leader, ts, pwrs) @*) - (*@ primitive.Sleep(params.NS_RESEND_COMMIT) @*) (*@ // Retry with different leaders until success. @*) (*@ leader = gcoord.ChangeLeader() @*) + (*@ gcoord.SendCommit(leader, ts, pwrs) @*) + (*@ primitive.Sleep(params.NS_RESEND_COMMIT) @*) (*@ } @*) (*@ } @*) set P := (λ _ : bool, ∃ leader' : u64, @@ -53,16 +61,15 @@ Section program. destruct finalized; wp_pures. { by iApply "HΦ". } iNamed "HP". + wp_apply (wp_GroupCoordinator__ChangeLeader with "Hgcoord"). + iIntros (leadernew Hleadernew). + wp_store. wp_load. - wp_apply (wp_GroupCoordinator__SendCommit with "Hcmted [] Hpwrs"). - { apply Hinaddrm. } - { iFrame "Hgcoord". } + wp_apply (wp_GroupCoordinator__SendCommit with "Hcmted Hgcoord Hpwrs"). + { apply Hleadernew. } iIntros "Hpwrs". wp_apply wp_Sleep. - wp_apply (wp_GroupCoordinator__ChangeLeader). - { iFrame "Hgcoord". } - iIntros (leadernew Hleadernew). - wp_store. + wp_pures. iApply "HΦ". by iFrame. } diff --git a/src/program_proof/tulip/program/txn/txn_begin.v b/src/program_proof/tulip/program/txn/txn_begin.v index 150a50102..bf9f3c427 100644 --- a/src/program_proof/tulip/program/txn/txn_begin.v +++ b/src/program_proof/tulip/program/txn/txn_begin.v @@ -24,6 +24,7 @@ Section program. (*@ func getTimestamp(sid uint64) uint64 { @*) (*@ ts := trusted_time.GetTime() @*) + (*@ @*) wp_apply (wp_GetTSC). iInv "Hinv" as "Hgentid" "Hclose". iMod (lc_fupd_elim_later with "LC Hgentid") as (clock) "Hgentid". @@ -34,21 +35,24 @@ Section program. iExists _. iFrame "Hclock". iIntros (clock2) "[%Hclock Hclock2]". iMod "Hclose2" as "_". - set inbounds := bool_decide (uint.Z clock2 + 64 < 2^64). + set inbounds := bool_decide (uint.Z clock2 + zN_TXN_SITES < 2^64). set clock2_boundsafe := if inbounds then clock2 else 0. - opose proof (u64_round_up_spec clock2_boundsafe (W64 64) _ _) as H. - { subst clock2_boundsafe inbounds. case_bool_decide; word. } + opose proof (u64_round_up_spec clock2_boundsafe (W64 zN_TXN_SITES) _ _) as H. + { subst clock2_boundsafe inbounds. rewrite /zN_TXN_SITES. case_bool_decide; word. } { word. } move:H. - set rounded_ts := u64_round_up clock2_boundsafe (W64 64). + rewrite /zN_TXN_SITES. + set rounded_ts := u64_round_up clock2_boundsafe (W64 zN_TXN_SITES). intros (Hmod & Hbound1 & Hbound2). set reserved_ts := word.add rounded_ts sid. - assert ((uint.Z rounded_ts + uint.Z sid) `mod` 64 = uint.Z sid) as Hsidmod. - { rewrite Z.add_mod. 2:lia. + assert ((uint.Z rounded_ts + uint.Z sid) `mod` zN_TXN_SITES = uint.Z sid) as Hsidmod. + { rewrite /zN_TXN_SITES. rewrite Z.add_mod. 2:lia. rewrite Hmod. rewrite [uint.Z sid `mod` _]Z.mod_small. 2:split;[word|done]. rewrite Z.mod_small. 1:lia. split;[word|done]. } + rewrite /zN_TXN_SITES in Hsidmod. assert (uint.Z (sid_of reserved_ts) = uint.Z sid) as Hsid_of. { rewrite /sid_of /reserved_ts. + rewrite /zN_TXN_SITES. rewrite word.unsigned_modu. 2:done. rewrite word.unsigned_add. rewrite (wrap_small (_+_)). 2:word. rewrite wrap_small. 1:done. @@ -63,28 +67,24 @@ Section program. iIntros "!> _". (*@ n := params.N_TXN_SITES @*) - wp_pures. - (*@ tid := std.SumAssumeNoOverflow(ts, n) / n * n + sid @*) - + (*@ @*) wp_pures. wp_apply std_proof.wp_SumAssumeNoOverflow. iIntros (Hoverflow). assert (inbounds = true) as ->. - { subst inbounds. rewrite bool_decide_true; first done. word. } + { subst inbounds. rewrite bool_decide_true; first done. rewrite /zN_TXN_SITES. word. } subst clock2_boundsafe. rewrite u64_Z_through_nat in Hclock. rewrite bool_decide_true. - 2:{ subst reserved_ts. word. } + 2:{ subst reserved_ts rounded_ts. rewrite /zN_TXN_SITES in Hmod Hsidmod Hbound1 *. word. } iDestruct "Hreserved" as (γr) "Hreserved". wp_pures. - set tid := (word.add _ _). assert (tid = reserved_ts) as -> by done. - (*@ @*) - (*@ @*) + (*@ for trusted_time.GetTime() <= tid { @*) (*@ } @*) - + (*@ @*) set P := λ (b : bool), (if b then True else tsc_lb (uint.nat reserved_ts))%I. wp_apply (wp_forBreak_cond P with "[] []"). { clear Φ. iIntros "!> %Φ _ HΦ". @@ -111,9 +111,9 @@ Section program. { eauto. } iModIntro. - (*@ @*) - (*@ return tid @*) - (*@ } @*) + (*@ @*) + (*@ return tid @*) + (*@ } @*) iApply "HΦ". Qed.