From 5cd40c1be6420dc5ff9b088c4e6428532585a312 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sat, 21 Oct 2023 22:18:11 +0200 Subject: [PATCH] consistently use annotations --- raft-proofs/AllEntriesCandidateEntriesProof.v | 2 +- raft-proofs/AllEntriesIndicesGt0Proof.v | 2 +- raft-proofs/AllEntriesLeaderLogsProof.v | 2 +- raft-proofs/AllEntriesLeaderLogsTermProof.v | 2 +- raft-proofs/AllEntriesLeaderSublogProof.v | 2 +- raft-proofs/AllEntriesLogMatchingProof.v | 2 +- raft-proofs/AllEntriesLogProof.v | 2 +- raft-proofs/AllEntriesTermSanityProof.v | 2 +- raft-proofs/AllEntriesVotesWithLogProof.v | 2 +- raft-proofs/AppendEntriesLeaderProof.v | 2 +- raft-proofs/AppendEntriesReplySublogProof.v | 2 +- raft-proofs/AppendEntriesRequestLeaderLogsProof.v | 2 +- ...AppendEntriesRequestReplyCorrespondenceProof.v | 2 +- .../AppendEntriesRequestsCameFromLeadersProof.v | 2 +- raft-proofs/AppliedEntriesMonotonicProof.v | 2 +- raft-proofs/AppliedImpliesInputProof.v | 2 +- raft-proofs/CandidateEntriesProof.v | 2 +- raft-proofs/CandidateTermGtLogProof.v | 2 +- raft-proofs/CausalOrderPreservedProof.v | 2 +- raft-proofs/CroniesTermProof.v | 2 +- raft-proofs/CurrentTermGtZeroProof.v | 2 +- raft-proofs/EveryEntryWasCreatedProof.v | 2 +- raft-proofs/GhostLogAllEntriesProof.v | 2 +- raft-proofs/GhostLogCorrectProof.v | 2 +- raft-proofs/GhostLogLogMatchingProof.v | 2 +- raft-proofs/GhostLogsLogPropertiesProof.v | 2 +- raft-proofs/InLogInAllEntriesProof.v | 2 +- raft-proofs/InputBeforeOutputProof.v | 2 +- raft-proofs/LastAppliedLeCommitIndexProof.v | 2 +- raft-proofs/LeaderLogsCandidateEntriesProof.v | 2 +- raft-proofs/LeaderLogsContiguousProof.v | 2 +- raft-proofs/LeaderLogsLogMatchingProof.v | 2 +- raft-proofs/LeaderLogsLogPropertiesProof.v | 2 +- raft-proofs/LeaderLogsPreservedProof.v | 2 +- raft-proofs/LeaderLogsSortedProof.v | 2 +- raft-proofs/LeaderLogsSublogProof.v | 2 +- raft-proofs/LeaderLogsTermSanityProof.v | 2 +- raft-proofs/LeaderLogsVotesWithLogProof.v | 2 +- raft-proofs/LeadersHaveLeaderLogsProof.v | 2 +- raft-proofs/LeadersHaveLeaderLogsStrongProof.v | 2 +- raft-proofs/LogAllEntriesProof.v | 2 +- raft-proofs/LogsLeaderLogsProof.v | 2 +- raft-proofs/MatchIndexAllEntriesProof.v | 2 +- raft-proofs/MatchIndexLeaderProof.v | 2 +- raft-proofs/MatchIndexSanityProof.v | 2 +- raft-proofs/NextIndexSafetyProof.v | 2 +- raft-proofs/OneLeaderLogPerTermProof.v | 2 +- raft-proofs/OutputCorrectProof.v | 2 +- raft-proofs/OutputGreatestIdProof.v | 2 +- raft-proofs/OutputImpliesAppliedProof.v | 2 +- raft-proofs/PrefixWithinTermProof.v | 2 +- raft-proofs/PrevLogCandidateEntriesTermProof.v | 2 +- raft-proofs/RequestVoteMaxIndexMaxTermProof.v | 2 +- raft-proofs/RequestVoteReplyMoreUpToDateProof.v | 2 +- raft-proofs/RequestVoteReplyTermSanityProof.v | 2 +- raft-proofs/RequestVoteTermSanityProof.v | 2 +- raft-proofs/StateMachineCorrectProof.v | 2 +- raft-proofs/StateMachineSafetyPrimeProof.v | 2 +- raft-proofs/StateMachineSafetyProof.v | 2 +- raft-proofs/TermsAndIndicesFromOneLogProof.v | 12 +++++------- raft-proofs/TermsAndIndicesFromOneProof.v | 15 ++++++--------- raft-proofs/VotedForMoreUpToDateProof.v | 2 +- raft-proofs/VotedForTermSanityProof.v | 2 +- raft-proofs/VotesCorrectProof.v | 2 +- raft-proofs/VotesLeCurrentTermProof.v | 2 +- raft-proofs/VotesReceivedMoreUpToDateProof.v | 2 +- raft-proofs/VotesVotesWithLogCorrespondProof.v | 2 +- raft-proofs/VotesWithLogSortedProof.v | 2 +- raft-proofs/VotesWithLogTermSanityProof.v | 2 +- ...ppendEntriesRequestsCameFromLeadersInterface.v | 3 +-- raft/CommonTheorems.v | 2 +- raft/RefinementCommonTheorems.v | 2 +- raft/TermsAndIndicesFromOneInterface.v | 5 ++--- raft/TermsAndIndicesFromOneLogInterface.v | 4 +--- systems/VarDRaftSerializers.v | 8 ++++---- 75 files changed, 88 insertions(+), 97 deletions(-) diff --git a/raft-proofs/AllEntriesCandidateEntriesProof.v b/raft-proofs/AllEntriesCandidateEntriesProof.v index b2f0b39c..e5ba7608 100644 --- a/raft-proofs/AllEntriesCandidateEntriesProof.v +++ b/raft-proofs/AllEntriesCandidateEntriesProof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import CroniesCorrectInterface CroniesTermInterface. From VerdiRaft Require Import AllEntriesTermSanityInterface SpecLemmas. From VerdiRaft Require Import RefinementSpecLemmas AllEntriesCandidateEntriesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AllEntriesCandidateEntries. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AllEntriesIndicesGt0Proof.v b/raft-proofs/AllEntriesIndicesGt0Proof.v index 86b0eefd..bd55956b 100644 --- a/raft-proofs/AllEntriesIndicesGt0Proof.v +++ b/raft-proofs/AllEntriesIndicesGt0Proof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import CommonDefinitions RefinementSpecLemmas. From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface. From VerdiRaft Require Import AllEntriesIndicesGt0Interface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AllEntriesIndicesGt0. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AllEntriesLeaderLogsProof.v b/raft-proofs/AllEntriesLeaderLogsProof.v index db8bf9a3..2ad413b6 100644 --- a/raft-proofs/AllEntriesLeaderLogsProof.v +++ b/raft-proofs/AllEntriesLeaderLogsProof.v @@ -7,7 +7,7 @@ From VerdiRaft Require Import AllEntriesLogInterface LeaderSublogInterface. From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface. From VerdiRaft Require Import AllEntriesLeaderLogsInterface. -Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never. Section AllEntriesLeaderLogs. diff --git a/raft-proofs/AllEntriesLeaderLogsTermProof.v b/raft-proofs/AllEntriesLeaderLogsTermProof.v index e6062886..30dbf8ba 100644 --- a/raft-proofs/AllEntriesLeaderLogsTermProof.v +++ b/raft-proofs/AllEntriesLeaderLogsTermProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import RefinementSpecLemmas SpecLemmas. From VerdiRaft Require Import AllEntriesLeaderLogsTermInterface. From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AllEntriesLeaderLogsTerm. diff --git a/raft-proofs/AllEntriesLeaderSublogProof.v b/raft-proofs/AllEntriesLeaderSublogProof.v index 77d9d032..3f04c301 100644 --- a/raft-proofs/AllEntriesLeaderSublogProof.v +++ b/raft-proofs/AllEntriesLeaderSublogProof.v @@ -8,7 +8,7 @@ From VerdiRaft Require Import AllEntriesCandidateEntriesInterface. From VerdiRaft Require Import VotesCorrectInterface CroniesCorrectInterface. From VerdiRaft Require Import LeaderSublogInterface OneLeaderPerTermInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AllEntriesLeaderSublog. diff --git a/raft-proofs/AllEntriesLogMatchingProof.v b/raft-proofs/AllEntriesLogMatchingProof.v index a18ee5be..d34e4ef7 100644 --- a/raft-proofs/AllEntriesLogMatchingProof.v +++ b/raft-proofs/AllEntriesLogMatchingProof.v @@ -5,7 +5,7 @@ From VerdiRaft Require Import AllEntriesLeaderSublogInterface. From VerdiRaft Require Import LeaderSublogInterface RefinedLogMatchingLemmasInterface. From VerdiRaft Require Import AllEntriesLogMatchingInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AllEntriesLogMatching. diff --git a/raft-proofs/AllEntriesLogProof.v b/raft-proofs/AllEntriesLogProof.v index 4f6d234c..062e560b 100644 --- a/raft-proofs/AllEntriesLogProof.v +++ b/raft-proofs/AllEntriesLogProof.v @@ -10,7 +10,7 @@ From VerdiRaft Require Import OneLeaderLogPerTermInterface. From VerdiRaft Require Import LeaderLogsSortedInterface TermSanityInterface. From VerdiRaft Require Import AllEntriesTermSanityInterface AllEntriesLogInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AllEntriesLog. diff --git a/raft-proofs/AllEntriesTermSanityProof.v b/raft-proofs/AllEntriesTermSanityProof.v index 3a1cae5c..b435fa2f 100644 --- a/raft-proofs/AllEntriesTermSanityProof.v +++ b/raft-proofs/AllEntriesTermSanityProof.v @@ -1,7 +1,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface SpecLemmas. From VerdiRaft Require Import RefinementSpecLemmas AllEntriesTermSanityInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AllEntriesTermSanity. diff --git a/raft-proofs/AllEntriesVotesWithLogProof.v b/raft-proofs/AllEntriesVotesWithLogProof.v index e32fb88c..2c441bdd 100644 --- a/raft-proofs/AllEntriesVotesWithLogProof.v +++ b/raft-proofs/AllEntriesVotesWithLogProof.v @@ -5,7 +5,7 @@ From VerdiRaft Require Import AllEntriesVotesWithLogInterface AllEntriesLogInter From VerdiRaft Require Import VotesWithLogTermSanityInterface VotesCorrectInterface. From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AllEntriesVotesWithLog. diff --git a/raft-proofs/AppendEntriesLeaderProof.v b/raft-proofs/AppendEntriesLeaderProof.v index 0475f4f3..399f8bb1 100644 --- a/raft-proofs/AppendEntriesLeaderProof.v +++ b/raft-proofs/AppendEntriesLeaderProof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersInterface. From VerdiRaft Require Import OneLeaderLogPerTermInterface LeaderLogsTermSanityInterface. From VerdiRaft Require Import OneLeaderPerTermInterface AppendEntriesLeaderInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AppendEntriesLeader. diff --git a/raft-proofs/AppendEntriesReplySublogProof.v b/raft-proofs/AppendEntriesReplySublogProof.v index 6731bec1..f7e27ae9 100644 --- a/raft-proofs/AppendEntriesReplySublogProof.v +++ b/raft-proofs/AppendEntriesReplySublogProof.v @@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft AppendEntriesReplySublogInterface. From VerdiRaft Require Import AppendEntriesRequestReplyCorrespondenceInterface. From VerdiRaft Require Import RaftRefinementInterface AppendEntriesLeaderInterface. -Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never. Section AppendEntriesReplySublog. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AppendEntriesRequestLeaderLogsProof.v b/raft-proofs/AppendEntriesRequestLeaderLogsProof.v index 552782ab..2c2e97a9 100644 --- a/raft-proofs/AppendEntriesRequestLeaderLogsProof.v +++ b/raft-proofs/AppendEntriesRequestLeaderLogsProof.v @@ -5,7 +5,7 @@ From VerdiRaft Require Import SortedInterface LogMatchingInterface. From VerdiRaft Require Import AppendEntriesRequestLeaderLogsInterface. From VerdiRaft Require Import NextIndexSafetyInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AppendEntriesRequestLeaderLogs. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v b/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v index fe8b1195..227e69e2 100644 --- a/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v +++ b/raft-proofs/AppendEntriesRequestReplyCorrespondenceProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import Raft SpecLemmas. From VerdiRaft Require Import AppendEntriesRequestReplyCorrespondenceInterface. From Verdi Require Import DupDropReordering. -Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never. Section AppendEntriesRequestReplyCorrespondence. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v b/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v index b06467c9..a2906990 100644 --- a/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v +++ b/raft-proofs/AppendEntriesRequestsCameFromLeadersProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import LeadersHaveLeaderLogsInterface. From VerdiRaft Require Import AppendEntriesRequestsCameFromLeadersInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AppendEntriesRequestsCameFromLeaders. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AppliedEntriesMonotonicProof.v b/raft-proofs/AppliedEntriesMonotonicProof.v index 81b1eeee..8439863f 100644 --- a/raft-proofs/AppliedEntriesMonotonicProof.v +++ b/raft-proofs/AppliedEntriesMonotonicProof.v @@ -8,7 +8,7 @@ From VerdiRaft Require Import LeaderCompletenessInterface. From VerdiRaft Require Import LastAppliedCommitIndexMatchingInterface. From VerdiRaft Require Import SpecLemmas AppliedEntriesMonotonicInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AppliedEntriesMonotonicProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/AppliedImpliesInputProof.v b/raft-proofs/AppliedImpliesInputProof.v index 61bcc80f..9e5623c7 100644 --- a/raft-proofs/AppliedImpliesInputProof.v +++ b/raft-proofs/AppliedImpliesInputProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import Raft CommonTheorems. From VerdiRaft Require Import TraceUtil OutputImpliesAppliedInterface. From VerdiRaft Require Import SpecLemmas AppliedImpliesInputInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section AppliedImpliesInputProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/CandidateEntriesProof.v b/raft-proofs/CandidateEntriesProof.v index 2a42ae7e..90f8f575 100644 --- a/raft-proofs/CandidateEntriesProof.v +++ b/raft-proofs/CandidateEntriesProof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import VotesCorrectInterface TermSanityInterface. From VerdiRaft Require Import CroniesTermInterface RefinementCommonTheorems. From VerdiRaft Require Import SpecLemmas CandidateEntriesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section CandidateEntriesProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/CandidateTermGtLogProof.v b/raft-proofs/CandidateTermGtLogProof.v index a96730be..c9070d1c 100644 --- a/raft-proofs/CandidateTermGtLogProof.v +++ b/raft-proofs/CandidateTermGtLogProof.v @@ -1,7 +1,7 @@ From VerdiRaft Require Import Raft SpecLemmas TermSanityInterface. From VerdiRaft Require Import CandidateTermGtLogInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section CandidateTermGtLog. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/CausalOrderPreservedProof.v b/raft-proofs/CausalOrderPreservedProof.v index 1e829618..e60b66d0 100644 --- a/raft-proofs/CausalOrderPreservedProof.v +++ b/raft-proofs/CausalOrderPreservedProof.v @@ -5,7 +5,7 @@ From VerdiRaft Require Import OutputImpliesAppliedInterface. From VerdiRaft Require Import AppliedImpliesInputInterface. From VerdiRaft Require Import AppliedEntriesMonotonicInterface. -Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never. Section CausalOrderPreserved. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/CroniesTermProof.v b/raft-proofs/CroniesTermProof.v index 3f4beee2..d1c98f9b 100644 --- a/raft-proofs/CroniesTermProof.v +++ b/raft-proofs/CroniesTermProof.v @@ -1,7 +1,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface. From VerdiRaft Require Import CommonTheorems CroniesTermInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section CroniesTermProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/CurrentTermGtZeroProof.v b/raft-proofs/CurrentTermGtZeroProof.v index 37610375..31c61098 100644 --- a/raft-proofs/CurrentTermGtZeroProof.v +++ b/raft-proofs/CurrentTermGtZeroProof.v @@ -1,6 +1,6 @@ From VerdiRaft Require Import Raft SpecLemmas CurrentTermGtZeroInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section CurrentTermGtZero. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/EveryEntryWasCreatedProof.v b/raft-proofs/EveryEntryWasCreatedProof.v index d3524ae5..f22080a0 100644 --- a/raft-proofs/EveryEntryWasCreatedProof.v +++ b/raft-proofs/EveryEntryWasCreatedProof.v @@ -5,7 +5,7 @@ From VerdiRaft Require Import EveryEntryWasCreatedInterface. From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import CommonTheorems. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section EveryEntryWasCreated. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/GhostLogAllEntriesProof.v b/raft-proofs/GhostLogAllEntriesProof.v index a5c55249..57ad97e9 100644 --- a/raft-proofs/GhostLogAllEntriesProof.v +++ b/raft-proofs/GhostLogAllEntriesProof.v @@ -5,7 +5,7 @@ From VerdiRaft Require Import RaftMsgRefinementInterface. From VerdiRaft Require Import InLogInAllEntriesInterface. From VerdiRaft Require Import GhostLogAllEntriesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section GhostLogAllEntriesProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/GhostLogCorrectProof.v b/raft-proofs/GhostLogCorrectProof.v index a786da1d..a0d8339d 100644 --- a/raft-proofs/GhostLogCorrectProof.v +++ b/raft-proofs/GhostLogCorrectProof.v @@ -5,7 +5,7 @@ From VerdiRaft Require Import NextIndexSafetyInterface. From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. From VerdiRaft Require Import GhostLogCorrectInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section GhostLogCorrectProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/GhostLogLogMatchingProof.v b/raft-proofs/GhostLogLogMatchingProof.v index 32f8f26e..e55a9b36 100644 --- a/raft-proofs/GhostLogLogMatchingProof.v +++ b/raft-proofs/GhostLogLogMatchingProof.v @@ -10,7 +10,7 @@ From VerdiRaft Require Import AllEntriesLeaderSublogInterface. From VerdiRaft Require Import GhostLogAllEntriesInterface. From VerdiRaft Require Import GhostLogLogMatchingInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section GhostLogLogMatching. diff --git a/raft-proofs/GhostLogsLogPropertiesProof.v b/raft-proofs/GhostLogsLogPropertiesProof.v index 12c2502a..cd37b359 100644 --- a/raft-proofs/GhostLogsLogPropertiesProof.v +++ b/raft-proofs/GhostLogsLogPropertiesProof.v @@ -2,7 +2,7 @@ From Verdi Require Import GhostSimulations. From VerdiRaft Require Import Raft RaftMsgRefinementInterface. From VerdiRaft Require Import GhostLogsLogPropertiesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section GhostLogsLogProperties. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/InLogInAllEntriesProof.v b/raft-proofs/InLogInAllEntriesProof.v index 91f731e6..ab78971f 100644 --- a/raft-proofs/InLogInAllEntriesProof.v +++ b/raft-proofs/InLogInAllEntriesProof.v @@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface. From VerdiRaft Require Import CommonTheorems SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import InLogInAllEntriesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section InLogInAllEntries. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/InputBeforeOutputProof.v b/raft-proofs/InputBeforeOutputProof.v index fe0df412..60495c01 100644 --- a/raft-proofs/InputBeforeOutputProof.v +++ b/raft-proofs/InputBeforeOutputProof.v @@ -8,7 +8,7 @@ From VerdiRaft Require Import SortedInterface LogMatchingInterface. From VerdiRaft Require Import StateMachineSafetyInterface MaxIndexSanityInterface. From VerdiRaft Require Import UniqueIndicesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section InputBeforeOutput. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LastAppliedLeCommitIndexProof.v b/raft-proofs/LastAppliedLeCommitIndexProof.v index b4a391f9..80b0accf 100644 --- a/raft-proofs/LastAppliedLeCommitIndexProof.v +++ b/raft-proofs/LastAppliedLeCommitIndexProof.v @@ -1,7 +1,7 @@ From VerdiRaft Require Import Raft LastAppliedLeCommitIndexInterface. From VerdiRaft Require Import SpecLemmas CommonTheorems. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LastAppliedLeCommitIndex. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderLogsCandidateEntriesProof.v b/raft-proofs/LeaderLogsCandidateEntriesProof.v index 922c9040..dc4589d2 100644 --- a/raft-proofs/LeaderLogsCandidateEntriesProof.v +++ b/raft-proofs/LeaderLogsCandidateEntriesProof.v @@ -7,7 +7,7 @@ From VerdiRaft Require Import LeaderLogsTermSanityInterface. From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import LeaderLogsCandidateEntriesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section CandidateEntriesInterface. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderLogsContiguousProof.v b/raft-proofs/LeaderLogsContiguousProof.v index aa24476c..9a5e0d55 100644 --- a/raft-proofs/LeaderLogsContiguousProof.v +++ b/raft-proofs/LeaderLogsContiguousProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface CommonTheorems. From VerdiRaft Require Import LeaderLogsContiguousInterface. From VerdiRaft Require Import LogMatchingInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsContiguous. diff --git a/raft-proofs/LeaderLogsLogMatchingProof.v b/raft-proofs/LeaderLogsLogMatchingProof.v index 6b4b035a..a1160955 100644 --- a/raft-proofs/LeaderLogsLogMatchingProof.v +++ b/raft-proofs/LeaderLogsLogMatchingProof.v @@ -10,7 +10,7 @@ From VerdiRaft Require Import LeaderLogsContiguousInterface. From VerdiRaft Require Import TermsAndIndicesFromOneInterface. From VerdiRaft Require Import LeaderLogsLogMatchingInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsLogMatching. diff --git a/raft-proofs/LeaderLogsLogPropertiesProof.v b/raft-proofs/LeaderLogsLogPropertiesProof.v index e0850d5c..d5bb9cb7 100644 --- a/raft-proofs/LeaderLogsLogPropertiesProof.v +++ b/raft-proofs/LeaderLogsLogPropertiesProof.v @@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface SpecLemmas. From VerdiRaft Require Import LeaderLogsLogPropertiesInterface. From VerdiRaft Require Import RefinementSpecLemmas. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsLogProperties. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderLogsPreservedProof.v b/raft-proofs/LeaderLogsPreservedProof.v index 709274e6..73925e81 100644 --- a/raft-proofs/LeaderLogsPreservedProof.v +++ b/raft-proofs/LeaderLogsPreservedProof.v @@ -8,7 +8,7 @@ From VerdiRaft Require Import OneLeaderLogPerTermInterface. From VerdiRaft Require Import VotesCorrectInterface. From VerdiRaft Require Import CroniesCorrectInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsPreserved. diff --git a/raft-proofs/LeaderLogsSortedProof.v b/raft-proofs/LeaderLogsSortedProof.v index ecd861fa..eacee280 100644 --- a/raft-proofs/LeaderLogsSortedProof.v +++ b/raft-proofs/LeaderLogsSortedProof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import CommonDefinitions SpecLemmas. From VerdiRaft Require Import LeaderLogsSortedInterface. From VerdiRaft Require Import SortedInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsSorted. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderLogsSublogProof.v b/raft-proofs/LeaderLogsSublogProof.v index 662721f1..282527ad 100644 --- a/raft-proofs/LeaderLogsSublogProof.v +++ b/raft-proofs/LeaderLogsSublogProof.v @@ -10,7 +10,7 @@ From VerdiRaft Require Import VotesCorrectInterface. From VerdiRaft Require Import RefinementCommonTheorems. From VerdiRaft Require Import LeaderLogsSublogInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsSublog. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeaderLogsTermSanityProof.v b/raft-proofs/LeaderLogsTermSanityProof.v index 699fefdc..fac9ccde 100644 --- a/raft-proofs/LeaderLogsTermSanityProof.v +++ b/raft-proofs/LeaderLogsTermSanityProof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import CandidateTermGtLogInterface. From VerdiRaft Require Import LeaderLogsTermSanityInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsTermSanity. diff --git a/raft-proofs/LeaderLogsVotesWithLogProof.v b/raft-proofs/LeaderLogsVotesWithLogProof.v index 7974e743..84c2adbb 100644 --- a/raft-proofs/LeaderLogsVotesWithLogProof.v +++ b/raft-proofs/LeaderLogsVotesWithLogProof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import VotesReceivedMoreUpToDateInterface. From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface. From VerdiRaft Require Import LeaderLogsVotesWithLogInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeaderLogsVotesWithLog. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeadersHaveLeaderLogsProof.v b/raft-proofs/LeadersHaveLeaderLogsProof.v index b5503079..adf83a66 100644 --- a/raft-proofs/LeadersHaveLeaderLogsProof.v +++ b/raft-proofs/LeadersHaveLeaderLogsProof.v @@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface. From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import LeadersHaveLeaderLogsInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeadersHaveLeaderLogs. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LeadersHaveLeaderLogsStrongProof.v b/raft-proofs/LeadersHaveLeaderLogsStrongProof.v index 0cd675a3..68df9430 100644 --- a/raft-proofs/LeadersHaveLeaderLogsStrongProof.v +++ b/raft-proofs/LeadersHaveLeaderLogsStrongProof.v @@ -1,7 +1,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface CommonTheorems. From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LeadersHaveLeaderLogsStrong. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LogAllEntriesProof.v b/raft-proofs/LogAllEntriesProof.v index 7a4f306a..0071ca4b 100644 --- a/raft-proofs/LogAllEntriesProof.v +++ b/raft-proofs/LogAllEntriesProof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import RefinementSpecLemmas. From VerdiRaft Require Import TermSanityInterface. From VerdiRaft Require Import LogAllEntriesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LogAllEntries. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/LogsLeaderLogsProof.v b/raft-proofs/LogsLeaderLogsProof.v index 12a15c35..30deb6c9 100644 --- a/raft-proofs/LogsLeaderLogsProof.v +++ b/raft-proofs/LogsLeaderLogsProof.v @@ -10,7 +10,7 @@ From VerdiRaft Require Import LeadersHaveLeaderLogsStrongInterface. From VerdiRaft Require Import NextIndexSafetyInterface. From VerdiRaft Require Import SortedInterface LeaderLogsLogPropertiesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section LogsLeaderLogs. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/MatchIndexAllEntriesProof.v b/raft-proofs/MatchIndexAllEntriesProof.v index 0db4fbb9..0b15d32b 100644 --- a/raft-proofs/MatchIndexAllEntriesProof.v +++ b/raft-proofs/MatchIndexAllEntriesProof.v @@ -18,7 +18,7 @@ From VerdiRaft Require Import VotesCorrectInterface. From VerdiRaft Require Import CroniesCorrectInterface. From VerdiRaft Require Import MatchIndexAllEntriesInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section MatchIndexAllEntries. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/MatchIndexLeaderProof.v b/raft-proofs/MatchIndexLeaderProof.v index ea2b6563..459f052d 100644 --- a/raft-proofs/MatchIndexLeaderProof.v +++ b/raft-proofs/MatchIndexLeaderProof.v @@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft SpecLemmas. From VerdiRaft Require Import NoAppendEntriesRepliesToSelfInterface. From VerdiRaft Require Import MatchIndexLeaderInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section MatchIndexLeader. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/MatchIndexSanityProof.v b/raft-proofs/MatchIndexSanityProof.v index 165b9c16..be89013d 100644 --- a/raft-proofs/MatchIndexSanityProof.v +++ b/raft-proofs/MatchIndexSanityProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import AppendEntriesReplySublogInterface. From VerdiRaft Require Import MatchIndexSanityInterface. From VerdiRaft Require Import SortedInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section MatchIndexSanity. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/NextIndexSafetyProof.v b/raft-proofs/NextIndexSafetyProof.v index e5d0a0db..b44a4a48 100644 --- a/raft-proofs/NextIndexSafetyProof.v +++ b/raft-proofs/NextIndexSafetyProof.v @@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft CommonTheorems SpecLemmas. From VerdiRaft Require Import AppendEntriesReplySublogInterface. From VerdiRaft Require Import SortedInterface NextIndexSafetyInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section NextIndexSafety. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/OneLeaderLogPerTermProof.v b/raft-proofs/OneLeaderLogPerTermProof.v index 28c50c3c..cac7b9f7 100644 --- a/raft-proofs/OneLeaderLogPerTermProof.v +++ b/raft-proofs/OneLeaderLogPerTermProof.v @@ -10,7 +10,7 @@ From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface. From VerdiRaft Require Import LeaderLogsTermSanityInterface. From VerdiRaft Require Import OneLeaderLogPerTermInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section OneLeaderLogPerTerm. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/OutputCorrectProof.v b/raft-proofs/OutputCorrectProof.v index edf65018..f75f812a 100644 --- a/raft-proofs/OutputCorrectProof.v +++ b/raft-proofs/OutputCorrectProof.v @@ -6,7 +6,7 @@ From VerdiRaft Require Import TraceUtil StateMachineCorrectInterface. From VerdiRaft Require Import SortedInterface LastAppliedCommitIndexMatchingInterface. From VerdiRaft Require Import LogMatchingInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section OutputCorrect. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/OutputGreatestIdProof.v b/raft-proofs/OutputGreatestIdProof.v index 43d05573..07f20a2e 100644 --- a/raft-proofs/OutputGreatestIdProof.v +++ b/raft-proofs/OutputGreatestIdProof.v @@ -8,7 +8,7 @@ From VerdiRaft Require Import LastAppliedCommitIndexMatchingInterface. From VerdiRaft Require Import TraceUtil SortedInterface. From VerdiRaft Require Import OutputGreatestIdInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section OutputGreatestId. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/OutputImpliesAppliedProof.v b/raft-proofs/OutputImpliesAppliedProof.v index ea72539e..e5892d24 100644 --- a/raft-proofs/OutputImpliesAppliedProof.v +++ b/raft-proofs/OutputImpliesAppliedProof.v @@ -6,7 +6,7 @@ From VerdiRaft Require Import MaxIndexSanityInterface. From VerdiRaft Require Import TraceUtil SortedInterface. From VerdiRaft Require Import OutputImpliesAppliedInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section OutputImpliesApplied. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/PrefixWithinTermProof.v b/raft-proofs/PrefixWithinTermProof.v index 72b26003..81046152 100644 --- a/raft-proofs/PrefixWithinTermProof.v +++ b/raft-proofs/PrefixWithinTermProof.v @@ -14,7 +14,7 @@ From VerdiRaft Require Import AllEntriesLogMatchingInterface. From VerdiRaft Require Import AppendEntriesRequestTermSanityInterface. From VerdiRaft Require Import AllEntriesLeaderSublogInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section PrefixWithinTerm. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/PrevLogCandidateEntriesTermProof.v b/raft-proofs/PrevLogCandidateEntriesTermProof.v index 08491d35..3957fda9 100644 --- a/raft-proofs/PrevLogCandidateEntriesTermProof.v +++ b/raft-proofs/PrevLogCandidateEntriesTermProof.v @@ -7,7 +7,7 @@ From VerdiRaft Require Import RefinementSpecLemmas. From VerdiRaft Require Import RefinementCommonTheorems. From VerdiRaft Require Import PrevLogCandidateEntriesTermInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section PrevLogCandidateEntriesTerm. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/RequestVoteMaxIndexMaxTermProof.v b/raft-proofs/RequestVoteMaxIndexMaxTermProof.v index 36b79855..6cc78491 100644 --- a/raft-proofs/RequestVoteMaxIndexMaxTermProof.v +++ b/raft-proofs/RequestVoteMaxIndexMaxTermProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import RequestVoteMaxIndexMaxTermInterface. From VerdiRaft Require Import RequestVoteTermSanityInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section RequestVoteMaxIndexMaxTerm. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/RequestVoteReplyMoreUpToDateProof.v b/raft-proofs/RequestVoteReplyMoreUpToDateProof.v index b362f7d6..9119d276 100644 --- a/raft-proofs/RequestVoteReplyMoreUpToDateProof.v +++ b/raft-proofs/RequestVoteReplyMoreUpToDateProof.v @@ -5,7 +5,7 @@ From VerdiRaft Require Import RequestVoteReplyTermSanityInterface. From VerdiRaft Require Import VotedForMoreUpToDateInterface. From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section RequestVoteReplyMoreUpToDate. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/RequestVoteReplyTermSanityProof.v b/raft-proofs/RequestVoteReplyTermSanityProof.v index 9112892c..dc688ebe 100644 --- a/raft-proofs/RequestVoteReplyTermSanityProof.v +++ b/raft-proofs/RequestVoteReplyTermSanityProof.v @@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface. From VerdiRaft Require Import SpecLemmas RequestVoteTermSanityInterface. From VerdiRaft Require Import RequestVoteReplyTermSanityInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section RequestVoteReplyTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/RequestVoteTermSanityProof.v b/raft-proofs/RequestVoteTermSanityProof.v index ac1922ff..cc095f38 100644 --- a/raft-proofs/RequestVoteTermSanityProof.v +++ b/raft-proofs/RequestVoteTermSanityProof.v @@ -1,7 +1,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface. From VerdiRaft Require Import SpecLemmas RequestVoteTermSanityInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section RequestVoteTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/StateMachineCorrectProof.v b/raft-proofs/StateMachineCorrectProof.v index c46c8b88..b7042c3b 100644 --- a/raft-proofs/StateMachineCorrectProof.v +++ b/raft-proofs/StateMachineCorrectProof.v @@ -6,7 +6,7 @@ From VerdiRaft Require Import LogMatchingInterface. From VerdiRaft Require Import StateMachineCorrectInterface. From Coq Require Import ZArith. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section StateMachineCorrect. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/StateMachineSafetyPrimeProof.v b/raft-proofs/StateMachineSafetyPrimeProof.v index ad05c63f..fff41b68 100644 --- a/raft-proofs/StateMachineSafetyPrimeProof.v +++ b/raft-proofs/StateMachineSafetyPrimeProof.v @@ -14,7 +14,7 @@ From VerdiRaft Require Import LogsLeaderLogsInterface. From VerdiRaft Require Import OneLeaderLogPerTermInterface. From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. -Local Arguments update {_} {_} {_} _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} {_} _ _ _ _ : simpl never. Section StateMachineSafety'. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/StateMachineSafetyProof.v b/raft-proofs/StateMachineSafetyProof.v index aadbe940..fe763b57 100644 --- a/raft-proofs/StateMachineSafetyProof.v +++ b/raft-proofs/StateMachineSafetyProof.v @@ -24,7 +24,7 @@ From VerdiRaft Require Import RefinedLogMatchingLemmasInterface. From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import RaftMsgRefinementInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section StateMachineSafetyProof. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/TermsAndIndicesFromOneLogProof.v b/raft-proofs/TermsAndIndicesFromOneLogProof.v index 54b605ea..a249ed5c 100644 --- a/raft-proofs/TermsAndIndicesFromOneLogProof.v +++ b/raft-proofs/TermsAndIndicesFromOneLogProof.v @@ -1,16 +1,14 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.CommonTheorems. -Require Import VerdiRaft.SpecLemmas. +From VerdiRaft Require Import Raft CommonTheorems SpecLemmas. +From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface. +From VerdiRaft Require Import CurrentTermGtZeroInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.TermsAndIndicesFromOneLogInterface. -Require Import VerdiRaft.CurrentTermGtZeroInterface. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section TermsAndIndicesFromOneLog. Context {orig_base_params : BaseParams}. Context {one_node_params : OneNodeParams orig_base_params}. Context {raft_params : RaftParams orig_base_params}. + Context {ctgzi : current_term_gt_zero_interface}. Definition terms_and_indices_from_one_log_ind (net : network) : Prop := diff --git a/raft-proofs/TermsAndIndicesFromOneProof.v b/raft-proofs/TermsAndIndicesFromOneProof.v index 8d61a567..053d8284 100644 --- a/raft-proofs/TermsAndIndicesFromOneProof.v +++ b/raft-proofs/TermsAndIndicesFromOneProof.v @@ -1,13 +1,10 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. -Require Import VerdiRaft.SpecLemmas. -Require Import VerdiRaft.RefinementSpecLemmas. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions SpecLemmas. +From VerdiRaft Require Import RefinementSpecLemmas. +From VerdiRaft Require Import TermsAndIndicesFromOneInterface. +From VerdiRaft Require Import TermsAndIndicesFromOneLogInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. - -Require Import VerdiRaft.TermsAndIndicesFromOneInterface. -Require Import VerdiRaft.TermsAndIndicesFromOneLogInterface. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section TermsAndIndicesFromOne. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotedForMoreUpToDateProof.v b/raft-proofs/VotedForMoreUpToDateProof.v index 38e19efd..a762731f 100644 --- a/raft-proofs/VotedForMoreUpToDateProof.v +++ b/raft-proofs/VotedForMoreUpToDateProof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import RequestVoteMaxIndexMaxTermInterface. From VerdiRaft Require Import VotedForTermSanityInterface. From VerdiRaft Require Import VotedForMoreUpToDateInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotedForMoreUpToDate. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotedForTermSanityProof.v b/raft-proofs/VotedForTermSanityProof.v index 98b32297..e1151cb4 100644 --- a/raft-proofs/VotedForTermSanityProof.v +++ b/raft-proofs/VotedForTermSanityProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import RequestVoteTermSanityInterface. From VerdiRaft Require Import VotedForTermSanityInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotedForTermSanity. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotesCorrectProof.v b/raft-proofs/VotesCorrectProof.v index e1004dd9..1e932d7d 100644 --- a/raft-proofs/VotesCorrectProof.v +++ b/raft-proofs/VotesCorrectProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import VotesCorrectInterface. From VerdiRaft Require Import VotesLeCurrentTermInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotesCorrect. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotesLeCurrentTermProof.v b/raft-proofs/VotesLeCurrentTermProof.v index 0ba7413b..71c78964 100644 --- a/raft-proofs/VotesLeCurrentTermProof.v +++ b/raft-proofs/VotesLeCurrentTermProof.v @@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface. From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import VotesLeCurrentTermInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotesLeCurrentTerm. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotesReceivedMoreUpToDateProof.v b/raft-proofs/VotesReceivedMoreUpToDateProof.v index 42511f8d..05b82a80 100644 --- a/raft-proofs/VotesReceivedMoreUpToDateProof.v +++ b/raft-proofs/VotesReceivedMoreUpToDateProof.v @@ -3,7 +3,7 @@ From VerdiRaft Require Import RefinementSpecLemmas CommonTheorems. From VerdiRaft Require Import RequestVoteReplyMoreUpToDateInterface. From VerdiRaft Require Import VotesReceivedMoreUpToDateInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotesReceivedMoreUpToDate. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotesVotesWithLogCorrespondProof.v b/raft-proofs/VotesVotesWithLogCorrespondProof.v index 099313ca..26d4a85f 100644 --- a/raft-proofs/VotesVotesWithLogCorrespondProof.v +++ b/raft-proofs/VotesVotesWithLogCorrespondProof.v @@ -1,7 +1,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface. From VerdiRaft Require Import VotesVotesWithLogCorrespondInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotesVotesWithLogCorrespond. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotesWithLogSortedProof.v b/raft-proofs/VotesWithLogSortedProof.v index 07489abf..74ac0d29 100644 --- a/raft-proofs/VotesWithLogSortedProof.v +++ b/raft-proofs/VotesWithLogSortedProof.v @@ -4,7 +4,7 @@ From VerdiRaft Require Import CommonDefinitions SpecLemmas. From VerdiRaft Require Import VotesWithLogSortedInterface. From VerdiRaft Require Import SortedInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotesWithLogSorted. Context {orig_base_params : BaseParams}. diff --git a/raft-proofs/VotesWithLogTermSanityProof.v b/raft-proofs/VotesWithLogTermSanityProof.v index 987899eb..3d4b59cd 100644 --- a/raft-proofs/VotesWithLogTermSanityProof.v +++ b/raft-proofs/VotesWithLogTermSanityProof.v @@ -2,7 +2,7 @@ From VerdiRaft Require Import Raft RaftRefinementInterface. From VerdiRaft Require Import SpecLemmas RefinementSpecLemmas. From VerdiRaft Require Import VotesWithLogTermSanityInterface. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section VotesWithLogTermSanity. diff --git a/raft/AppendEntriesRequestsCameFromLeadersInterface.v b/raft/AppendEntriesRequestsCameFromLeadersInterface.v index dadb6939..9433b9da 100644 --- a/raft/AppendEntriesRequestsCameFromLeadersInterface.v +++ b/raft/AppendEntriesRequestsCameFromLeadersInterface.v @@ -1,5 +1,4 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. +From VerdiRaft Require Import Raft RaftRefinementInterface. Section AppendEntriesRequestsCameFromLeaders. Context {orig_base_params : BaseParams}. diff --git a/raft/CommonTheorems.v b/raft/CommonTheorems.v index 6c408254..850e6c94 100644 --- a/raft/CommonTheorems.v +++ b/raft/CommonTheorems.v @@ -2,7 +2,7 @@ From Coq Require Import PeanoNat FunInd. From VerdiRaft Require Import RaftState Raft. From VerdiRaft Require Export CommonDefinitions. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section CommonTheorems. Context {orig_base_params : BaseParams}. diff --git a/raft/RefinementCommonTheorems.v b/raft/RefinementCommonTheorems.v index c49f48b6..247af702 100644 --- a/raft/RefinementCommonTheorems.v +++ b/raft/RefinementCommonTheorems.v @@ -6,7 +6,7 @@ From VerdiRaft Require Import CommonTheorems. From VerdiRaft Require Export RefinementCommonDefinitions. From VerdiRaft Require Import SpecLemmas. -Local Arguments update {_} {_} _ _ _ _ _ : simpl never. +#[local] Arguments update {_} {_} _ _ _ _ _ : simpl never. Section CommonTheorems. Context {orig_base_params : BaseParams}. diff --git a/raft/TermsAndIndicesFromOneInterface.v b/raft/TermsAndIndicesFromOneInterface.v index 6807348f..4bf7f006 100644 --- a/raft/TermsAndIndicesFromOneInterface.v +++ b/raft/TermsAndIndicesFromOneInterface.v @@ -1,6 +1,5 @@ -Require Import VerdiRaft.Raft. -Require Import VerdiRaft.RaftRefinementInterface. -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft RaftRefinementInterface. +From VerdiRaft Require Import CommonDefinitions. Section TermsAndIndicesFromOne. Context {orig_base_params : BaseParams}. diff --git a/raft/TermsAndIndicesFromOneLogInterface.v b/raft/TermsAndIndicesFromOneLogInterface.v index 820f6457..936847d7 100644 --- a/raft/TermsAndIndicesFromOneLogInterface.v +++ b/raft/TermsAndIndicesFromOneLogInterface.v @@ -1,6 +1,4 @@ -Require Import VerdiRaft.Raft. - -Require Import VerdiRaft.CommonDefinitions. +From VerdiRaft Require Import Raft CommonDefinitions. Section TermsAndIndicesFromOneLogInterface. Context {orig_base_params : BaseParams}. diff --git a/systems/VarDRaftSerializers.v b/systems/VarDRaftSerializers.v index e81388eb..dae39968 100644 --- a/systems/VarDRaftSerializers.v +++ b/systems/VarDRaftSerializers.v @@ -161,7 +161,7 @@ Section Serializers. cheerios_crush. Qed. - Global Instance msg_Serializer : Serializer msg := + #[global] Instance msg_Serializer : Serializer msg := {| serialize := msg_serialize; deserialize := msg_deserialize; serialize_deserialize_id := msg_serialize_deserialize_id |}. @@ -217,7 +217,7 @@ Section Serializers. repeat (cheerios_crush; simpl). Qed. - Global Instance output_Serializer : Serializer output := + #[global] Instance output_Serializer : Serializer output := {| serialize := serialize_output; deserialize := deserialize_output; serialize_deserialize_id := output_serialize_deserialize_id |}. @@ -265,7 +265,7 @@ Section Serializers. reflexivity. Qed. - Global Instance raft_data_Serializer : Serializer raft_data := + #[global] Instance raft_data_Serializer : Serializer raft_data := {| serialize := serialize_raft_data; deserialize := deserialize_raft_data; serialize_deserialize_id := raft_data_serialize_deserialize_id |}. @@ -302,7 +302,7 @@ Section Serializers. destruct i; repeat (cheerios_crush; simpl). Qed. - Global Instance raft_input_Serializer : Serializer raft_input := + #[global] Instance raft_input_Serializer : Serializer raft_input := {| serialize := serialize_raft_input; deserialize := deserialize_raft_input; serialize_deserialize_id := raft_input_serialize_deserialize_id |}.