- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.dfy files (475): ironclad-apps/src/Checked/Libraries/DafnyCC/Base.dfy ironclad-apps/src/Checked/Libraries/DafnyCC/Seq.dfy ironclad-apps/src/Dafny/Apps/AddPerf/Main.i.dfy ironclad-apps/src/Dafny/Apps/AppLoader/Main.i.dfy ironclad-apps/src/Dafny/Apps/BenchmarkApp/Main.i.dfy ironclad-apps/src/Dafny/Apps/BenchmarkService/BenchmarkCore.i.dfy ironclad-apps/src/Dafny/Apps/BenchmarkService/BenchmarkList.i.dfy ironclad-apps/src/Dafny/Apps/BenchmarkService/Main.i.dfy ironclad-apps/src/Dafny/Apps/BenchmarkService/Protocol.i.dfy ironclad-apps/src/Dafny/Apps/Common/CommonState.i.dfy ironclad-apps/src/Dafny/Apps/Common/CommonState.s.dfy ironclad-apps/src/Dafny/Apps/DafnyCCTest/Main.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/Database.s.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/DiffPriv.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/DiffPriv.s.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/DiffPrivPerformQuery.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/ErrorCodes.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/Main.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/Mapper.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/Mapper.s.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/Math.s.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/Noise.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/Noise.s.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/PacketParsing.c.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/PacketParsing.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/RelationalProperties.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/StateMachine.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/StateMachine.s.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/StateMachine2.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/SumReducer.i.dfy ironclad-apps/src/Dafny/Apps/DiffPriv/SumReducer.s.dfy ironclad-apps/src/Dafny/Apps/EtherTest/EtherTest.i.dfy ironclad-apps/src/Dafny/Apps/Notary/Main.i.dfy ironclad-apps/src/Dafny/Apps/Notary/MainOneStep.i.dfy ironclad-apps/src/Dafny/Apps/Notary/Notary.i.dfy ironclad-apps/src/Dafny/Apps/Notary/Notary.s.dfy ironclad-apps/src/Dafny/Apps/Notary/PacketParsing.c.dfy ironclad-apps/src/Dafny/Apps/Notary/PacketParsing.i.dfy ironclad-apps/src/Dafny/Apps/Notary/StateMachine.i.dfy ironclad-apps/src/Dafny/Apps/Notary/StateMachine.s.dfy ironclad-apps/src/Dafny/Apps/PassHash/Main.i.dfy ironclad-apps/src/Dafny/Apps/PassHash/PacketParsing.c.dfy ironclad-apps/src/Dafny/Apps/PassHash/PacketParsing.i.dfy ironclad-apps/src/Dafny/Apps/PassHash/PassHash.i.dfy ironclad-apps/src/Dafny/Apps/PassHash/PassHash.s.dfy ironclad-apps/src/Dafny/Apps/PassHash/StateMachine.s.dfy ironclad-apps/src/Dafny/Apps/TPMTest/TPMTest.i.dfy ironclad-apps/src/Dafny/Apps/TrInc/Main.i.dfy ironclad-apps/src/Dafny/Apps/TrInc/PacketParsing.c.dfy ironclad-apps/src/Dafny/Apps/TrInc/PacketParsing.i.dfy ironclad-apps/src/Dafny/Apps/TrInc/StateMachine.i.dfy ironclad-apps/src/Dafny/Apps/TrInc/StateMachine.s.dfy ironclad-apps/src/Dafny/Apps/TrInc/TrInc.i.dfy ironclad-apps/src/Dafny/Apps/TrInc/TrInc.s.dfy ironclad-apps/src/Dafny/Apps/UdpEchoService/UdpEchoService.i.dfy ironclad-apps/src/Dafny/Drivers/CPU/assembly.i.dfy ironclad-apps/src/Dafny/Drivers/CPU/assembly.s.dfy ironclad-apps/src/Dafny/Drivers/CPU/assembly_premium.i.dfy ironclad-apps/src/Dafny/Drivers/IO/io_mem.i.dfy ironclad-apps/src/Dafny/Drivers/IO/io_mem.s.dfy ironclad-apps/src/Dafny/Drivers/IO/pci.i.dfy ironclad-apps/src/Dafny/Drivers/Network/Intel/driver.i.dfy ironclad-apps/src/Dafny/Drivers/TPM/tpm-device.s.dfy ironclad-apps/src/Dafny/Drivers/TPM/tpm-driver.i.dfy ironclad-apps/src/Dafny/Drivers/TPM/tpm-wrapper-randoms.i.dfy ironclad-apps/src/Dafny/Drivers/TPM/tpm-wrapper.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatAdd.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatBitCount.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatBitwise.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatCompare.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatCore.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatDiv.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatMod.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatMul.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatPartial.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatRandom.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatSub.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatTestLib.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNatX86Shim.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNum.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigNumBEAdaptor.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/BigRat.i.dfy ironclad-apps/src/Dafny/Libraries/BigNum/Word32.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/Digest.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/Digest.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/hmac_common.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/hmac_common.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha1.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha1.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha1_hmac.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha256.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha256.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha256_hmac.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha256common.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha256opt.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha256opt2.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha_common.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha_common.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha_padding.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/Hash/sha_test.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/BlockEncoding.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/ByteSequences.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/Extended_GCD.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/KeyGen.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/KeyGen.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/KeyImpl.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/KeybitsLength.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/MillerRabin.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/MillerRabin.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/MultiplicativeInverse.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/OAEP.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/OAEP.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/PSS.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/RSA.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/RSADigestedSign.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/RSAOps.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/RSAPublicWrapper.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/RSASpec.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/RSA_Decrypt.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/division.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/rfc4251.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/rfc4251decode.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RSA/rfc4251impl.i.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RandomNumberGen.s.dfy ironclad-apps/src/Dafny/Libraries/Crypto/RandomTracing.s.dfy ironclad-apps/src/Dafny/Libraries/FatNat/BigNatToFatNatAdaptor.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/Bitwise.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/CanonicalArrays.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatInt.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatAdd.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatAddLemmas.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatAddUnrolled.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatCommon.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatCompare.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatDiv.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatDivDefs.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatDivEstDiv32.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatDivEstTrivial.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatMod.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatModesty.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatMul.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatRandom.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatReciprocal.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatSub.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatX86.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/FatNatX86big.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/Transforms.i.dfy ironclad-apps/src/Dafny/Libraries/FatNat/WordBoundHack.i.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/Bizarre.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/FleetNatAdd.i.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/FleetNatCommon.i.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/FleetNatMul.i.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/FleetNatMulLemmas.i.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/FleetNatMulLoopOpt.i.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/FleetNatMulLoopOptLemmas.i.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/FleetNatMulOpt.i.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/FleetNatSub.i.dfy ironclad-apps/src/Dafny/Libraries/FleetNat/FleetNatSubOpt.i.dfy ironclad-apps/src/Dafny/Libraries/Math/BitwiseOperations.i.dfy ironclad-apps/src/Dafny/Libraries/Math/GCD.s.dfy ironclad-apps/src/Dafny/Libraries/Math/bit_vector_lemmas.i.dfy ironclad-apps/src/Dafny/Libraries/Math/bit_vector_lemmas_premium.i.dfy ironclad-apps/src/Dafny/Libraries/Math/div.i.dfy ironclad-apps/src/Dafny/Libraries/Math/div_boogie.i.dfy ironclad-apps/src/Dafny/Libraries/Math/div_def.i.dfy ironclad-apps/src/Dafny/Libraries/Math/div_nonlinear.i.dfy ironclad-apps/src/Dafny/Libraries/Math/evenodd.i.dfy ironclad-apps/src/Dafny/Libraries/Math/mul.i.dfy ironclad-apps/src/Dafny/Libraries/Math/mul_nonlinear.i.dfy ironclad-apps/src/Dafny/Libraries/Math/power.i.dfy ironclad-apps/src/Dafny/Libraries/Math/power.s.dfy ironclad-apps/src/Dafny/Libraries/Math/power2.i.dfy ironclad-apps/src/Dafny/Libraries/Math/power2.s.dfy ironclad-apps/src/Dafny/Libraries/Math/power2methods.i.dfy ironclad-apps/src/Dafny/Libraries/Math/round.i.dfy ironclad-apps/src/Dafny/Libraries/Math/round.s.dfy ironclad-apps/src/Dafny/Libraries/Net/IPv4.i.dfy ironclad-apps/src/Dafny/Libraries/Net/InternetChecksum.i.dfy ironclad-apps/src/Dafny/Libraries/Net/Udp.i.dfy ironclad-apps/src/Dafny/Libraries/Net/ethernet.i.dfy ironclad-apps/src/Dafny/Libraries/Util/DebugPrint.i.dfy ironclad-apps/src/Dafny/Libraries/Util/Halter.i.dfy ironclad-apps/src/Dafny/Libraries/Util/ProfileIfc.i.dfy ironclad-apps/src/Dafny/Libraries/Util/arrays.i.dfy ironclad-apps/src/Dafny/Libraries/Util/arrays_2.i.dfy ironclad-apps/src/Dafny/Libraries/Util/arrays_and_seqs.i.dfy ironclad-apps/src/Dafny/Libraries/Util/be_sequences.s.dfy ironclad-apps/src/Dafny/Libraries/Util/beseqs_simple.i.dfy ironclad-apps/src/Dafny/Libraries/Util/bytes_and_words.s.dfy ironclad-apps/src/Dafny/Libraries/Util/insecure_prng.i.dfy ironclad-apps/src/Dafny/Libraries/Util/integer_sequences.i.dfy ironclad-apps/src/Dafny/Libraries/Util/integer_sequences.s.dfy ironclad-apps/src/Dafny/Libraries/Util/integer_sequences_premium.i.dfy ironclad-apps/src/Dafny/Libraries/Util/relational.i.dfy ironclad-apps/src/Dafny/Libraries/Util/relational.s.dfy ironclad-apps/src/Dafny/Libraries/Util/repeat_digit.i.dfy ironclad-apps/src/Dafny/Libraries/Util/seq_blocking.i.dfy ironclad-apps/src/Dafny/Libraries/Util/seq_blocking.s.dfy ironclad-apps/src/Dafny/Libraries/Util/seqs_and_ints.i.dfy ironclad-apps/src/Dafny/Libraries/Util/seqs_canonical.i.dfy ironclad-apps/src/Dafny/Libraries/Util/seqs_common.i.dfy ironclad-apps/src/Dafny/Libraries/Util/seqs_reverse.i.dfy ironclad-apps/src/Dafny/Libraries/Util/seqs_simple.i.dfy ironclad-apps/src/Dafny/Libraries/Util/seqs_transforms.i.dfy ironclad-apps/src/Dafny/Libraries/Util/word_bits.i.dfy ironclad-apps/src/Dafny/Libraries/base.s.dfy ironclad-apps/src/Trusted/DafnySpec/Seq.s.dfy ironclad-apps/tools/DafnySpec/DafnyPrelude.dfy ironfleet/src/Dafny/Distributed/Common/Collections/CountMatches.i.dfy ironfleet/src/Dafny/Distributed/Common/Collections/Maps.i.dfy ironfleet/src/Dafny/Distributed/Common/Collections/Maps2.i.dfy ironfleet/src/Dafny/Distributed/Common/Collections/Maps2.s.dfy ironfleet/src/Dafny/Distributed/Common/Collections/Multisets.s.dfy ironfleet/src/Dafny/Distributed/Common/Collections/Seqs.i.dfy ironfleet/src/Dafny/Distributed/Common/Collections/Seqs.s.dfy ironfleet/src/Dafny/Distributed/Common/Collections/Sets.i.dfy ironfleet/src/Dafny/Distributed/Common/Framework/AbstractService.s.dfy ironfleet/src/Dafny/Distributed/Common/Framework/DistributedSystem.s.dfy ironfleet/src/Dafny/Distributed/Common/Framework/Environment.s.dfy ironfleet/src/Dafny/Distributed/Common/Framework/EnvironmentSynchrony.s.dfy ironfleet/src/Dafny/Distributed/Common/Framework/EnvironmentSynchronyLemmas.i.dfy ironfleet/src/Dafny/Distributed/Common/Framework/Host.s.dfy ironfleet/src/Dafny/Distributed/Common/Framework/HostQueueLemmas.i.dfy ironfleet/src/Dafny/Distributed/Common/Framework/Main.s.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Option.i.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/Heuristics.i.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/Induction.i.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/LeadsTo.i.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/Monotonicity.i.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/Rules.i.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/Sets.i.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/Temporal.s.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/Time.i.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/Time.s.dfy ironfleet/src/Dafny/Distributed/Common/Logic/Temporal/WF1.i.dfy ironfleet/src/Dafny/Distributed/Common/Native/Io.s.dfy ironfleet/src/Dafny/Distributed/Common/Native/IoLemmas.i.dfy ironfleet/src/Dafny/Distributed/Common/Native/NativeTypes.i.dfy ironfleet/src/Dafny/Distributed/Common/Native/NativeTypes.s.dfy ironfleet/src/Dafny/Distributed/Impl/Common/CmdLineParser.i.dfy ironfleet/src/Dafny/Distributed/Impl/Common/GenericMarshalling.i.dfy ironfleet/src/Dafny/Distributed/Impl/Common/GenericRefinement.i.dfy ironfleet/src/Dafny/Distributed/Impl/Common/MarshallInt.i.dfy ironfleet/src/Dafny/Distributed/Impl/Common/NetClient.i.dfy ironfleet/src/Dafny/Distributed/Impl/Common/NodeIdentity.i.dfy ironfleet/src/Dafny/Distributed/Impl/Common/SeqIsUnique.i.dfy ironfleet/src/Dafny/Distributed/Impl/Common/SeqIsUniqueDef.i.dfy ironfleet/src/Dafny/Distributed/Impl/Common/UpperBound.i.dfy ironfleet/src/Dafny/Distributed/Impl/Common/Util.i.dfy ironfleet/src/Dafny/Distributed/Impl/LiveSHT/CmdLineParser.i.dfy ironfleet/src/Dafny/Distributed/Impl/LiveSHT/Host.i.dfy ironfleet/src/Dafny/Distributed/Impl/LiveSHT/NetSHT.i.dfy ironfleet/src/Dafny/Distributed/Impl/LiveSHT/SchedulerImpl.i.dfy ironfleet/src/Dafny/Distributed/Impl/LiveSHT/SchedulerModel.i.dfy ironfleet/src/Dafny/Distributed/Impl/LiveSHT/Unsendable.i.dfy ironfleet/src/Dafny/Distributed/Impl/Lock/CmdLineParser.i.dfy ironfleet/src/Dafny/Distributed/Impl/Lock/Host.i.dfy ironfleet/src/Dafny/Distributed/Impl/Lock/Message.i.dfy ironfleet/src/Dafny/Distributed/Impl/Lock/NetLock.i.dfy ironfleet/src/Dafny/Distributed/Impl/Lock/Node.i.dfy ironfleet/src/Dafny/Distributed/Impl/Lock/NodeImpl.i.dfy ironfleet/src/Dafny/Distributed/Impl/Lock/PacketParsing.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/AcceptorModel.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/AcceptorState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/AppInterface.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/Broadcast.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/CClockReading.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/CLastCheckpointedMap.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/CMessage.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/CMessageRefinements.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/COperationNumberSort.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/CPaxosConfiguration.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/CTypes.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/CmdLineParser.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ConstantsState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ElectionModel.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ElectionState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ExecutorModel.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ExecutorState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/Host.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/LearnerModel.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/LearnerState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/MinCQuorumSize.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/NetRSL.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/PacketParsing.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ParametersState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/PaxosWorldState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ProposerLemmas.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ProposerModel.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ProposerState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/QRelations.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaConstantsState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaImplClass.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaImplDelivery.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaImplLemmas.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaImplMain.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaImplNoReceiveClock.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaImplNoReceiveNoClock.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaImplProcessPacketNoClock.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaImplProcessPacketX.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaImplReadClock.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaModel-Part1.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaModel-Part2.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaModel-Part3.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaModel-Part4.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaModel-Part5.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaModel.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/ReplicaState.i.dfy ironfleet/src/Dafny/Distributed/Impl/RSL/Unsendable.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/AppInterface.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/AppInterfaceConcrete.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/CMessage.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/ConstantsState.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/DelegationLookup.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/Delegations.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/HostModel.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/HostState.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/PacketParsing.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/Parameters.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/SHTConcreteConfiguration.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/SingleDeliveryModel.i.dfy ironfleet/src/Dafny/Distributed/Impl/SHT/SingleDeliveryState.i.dfy ironfleet/src/Dafny/Distributed/Protocol/Common/Liveness/RTSchedule.i.dfy ironfleet/src/Dafny/Distributed/Protocol/Common/NodeIdentity.i.dfy ironfleet/src/Dafny/Distributed/Protocol/Common/NodeIdentity.s.dfy ironfleet/src/Dafny/Distributed/Protocol/Common/UpperBound.s.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/Acks.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/Actions.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/Assumptions.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/Constants.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/Environment.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/InfiniteSends.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/Invariants.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/LivenessProof.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/PacketReceipt.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/PacketSending.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/RefinementInvariants.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/RoundRobin.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/LivenessProof/Seqno.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/RefinementProof/Environment.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/RefinementProof/EnvironmentLemmas.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/RefinementProof/EnvironmentRefinement.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/RefinementProof/SHT.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/RefinementProof/SHTLemmas.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/RefinementProof/SHTRefinement.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/RefinementProof/SchedulerLemmas.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/RefinementProof/SchedulerRefinement.i.dfy ironfleet/src/Dafny/Distributed/Protocol/LiveSHT/Scheduler.i.dfy ironfleet/src/Dafny/Distributed/Protocol/Lock/Node.i.dfy ironfleet/src/Dafny/Distributed/Protocol/Lock/RefinementProof/DistributedSystem.i.dfy ironfleet/src/Dafny/Distributed/Protocol/Lock/RefinementProof/Refinement.i.dfy ironfleet/src/Dafny/Distributed/Protocol/Lock/RefinementProof/RefinementProof.i.dfy ironfleet/src/Dafny/Distributed/Protocol/Lock/Types.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Acceptor.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Broadcast.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/ClockReading.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Actions.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Assumptions.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/CanonicalizeBallot.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Chosen.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Constants.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Environment.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/LearnerState.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/LogTruncationPoint.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/MaxBallot.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/MaxBallotISent1a.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Message1b.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Message2a.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Message2b.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/PacketSending.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Quorum.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Received1b.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/ReplyCache.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/CommonProof/Requests.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Configuration.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Constants.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/DistributedSystem.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Election.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Environment.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Executor.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Learner.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Assumptions.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Catchup.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Environment.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/EpochLength.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Execution.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/GenericInvariants.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Invariants.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/LivenessProof.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/MaxBalReflected.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/MaxBallot.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/MaxBallotISent1a.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/NextOp.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/PacketHandling.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Phase1a.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Phase1b.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Phase1bCont.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Phase2Conclusion.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Phase2Invariants.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Phase2Start.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Phase2a.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Phase2b.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Phase2c.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/RealTime.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/RequestQueue.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/RequestsReceived.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/RoundRobin.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/Seqno.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/StablePeriod.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/StateTransfer.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/ViewAdvance.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/ViewChange.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/ViewPersistence.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/ViewPropagation.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/ViewPropagation2.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/ViewSuspicion.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/LivenessProof/WF1.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Message.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Parameters.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Proposer.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/RefinementProof/Chosen.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/RefinementProof/Execution.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/RefinementProof/HandleRequestBatch.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/RefinementProof/Refinement.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/RefinementProof/Requests.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/RefinementProof/StateMachine.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Replica.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/StateMachine.i.dfy ironfleet/src/Dafny/Distributed/Protocol/RSL/Types.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/Configuration.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/Delegations.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/Host.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/Keys.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/Message.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/Network.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/Parameters.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/RefinementProof/InvDefs.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/RefinementProof/InvProof.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/RefinementProof/Refinement.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/RefinementProof/RefinementProof.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/RefinementProof/SHT.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/SingleDelivery.i.dfy ironfleet/src/Dafny/Distributed/Protocol/SHT/SingleMessage.i.dfy ironfleet/src/Dafny/Distributed/Services/Lock/AbstractService.s.dfy ironfleet/src/Dafny/Distributed/Services/Lock/LockDistributedSystem.i.dfy ironfleet/src/Dafny/Distributed/Services/Lock/Main.i.dfy ironfleet/src/Dafny/Distributed/Services/Lock/Marshall.i.dfy ironfleet/src/Dafny/Distributed/Services/RSL/AbstractService.s.dfy ironfleet/src/Dafny/Distributed/Services/RSL/AppStateMachine.s.dfy ironfleet/src/Dafny/Distributed/Services/RSL/Main.i.dfy ironfleet/src/Dafny/Distributed/Services/RSL/Marshall.i.dfy ironfleet/src/Dafny/Distributed/Services/RSL/RSLDistributedSystem.i.dfy ironfleet/src/Dafny/Distributed/Services/SHT/AbstractService.s.dfy ironfleet/src/Dafny/Distributed/Services/SHT/AppInterface.i.dfy ironfleet/src/Dafny/Distributed/Services/SHT/AppInterface.s.dfy ironfleet/src/Dafny/Distributed/Services/SHT/Bytes.s.dfy ironfleet/src/Dafny/Distributed/Services/SHT/HT.s.dfy ironfleet/src/Dafny/Distributed/Services/SHT/Main.i.dfy ironfleet/src/Dafny/Distributed/Services/SHT/Marshall.i.dfy ironfleet/src/Dafny/Distributed/Services/SHT/SHTDistributedSystem.i.dfy ironfleet/src/Dafny/Libraries/Math/div.i.dfy ironfleet/src/Dafny/Libraries/Math/div_auto.i.dfy ironfleet/src/Dafny/Libraries/Math/div_auto_proofs.i.dfy ironfleet/src/Dafny/Libraries/Math/div_def.i.dfy ironfleet/src/Dafny/Libraries/Math/div_nonlinear.i.dfy ironfleet/src/Dafny/Libraries/Math/mod_auto.i.dfy ironfleet/src/Dafny/Libraries/Math/mod_auto_proofs.i.dfy ironfleet/src/Dafny/Libraries/Math/mul.i.dfy ironfleet/src/Dafny/Libraries/Math/mul_auto.i.dfy ironfleet/src/Dafny/Libraries/Math/mul_auto_proofs.i.dfy ironfleet/src/Dafny/Libraries/Math/mul_nonlinear.i.dfy ironfleet/src/Dafny/Libraries/Math/power.i.dfy ironfleet/src/Dafny/Libraries/Math/power2.i.dfy ironfleet/src/Dafny/Libraries/Math/power2s.i.dfy ironfleet/src/Dafny/Libraries/Math/powers.i.dfy - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.beat files (58): ironclad-apps/src/Checked/Nucleus/Base/BitVectorLemmasBase.ifc.beat ironclad-apps/src/Checked/Nucleus/Base/BitVectorLemmasBase.imp.beat ironclad-apps/src/Checked/Nucleus/Base/Core.ifc.beat ironclad-apps/src/Checked/Nucleus/Base/Core.imp.beat ironclad-apps/src/Checked/Nucleus/Base/Instructions.ifc.beat ironclad-apps/src/Checked/Nucleus/Base/Instructions.imp.beat ironclad-apps/src/Checked/Nucleus/Base/IntLemmasBase.ifc.beat ironclad-apps/src/Checked/Nucleus/Base/IntLemmasBase.imp.beat ironclad-apps/src/Checked/Nucleus/Base/LogicalAddressing.ifc.beat ironclad-apps/src/Checked/Nucleus/Base/LogicalAddressing.imp.beat ironclad-apps/src/Checked/Nucleus/Base/Overflow.imp.beat ironclad-apps/src/Checked/Nucleus/Base/Partition.ifc.beat ironclad-apps/src/Checked/Nucleus/Base/Partition.imp.beat ironclad-apps/src/Checked/Nucleus/Base/Separation.ifc.beat ironclad-apps/src/Checked/Nucleus/Base/Separation.imp.beat ironclad-apps/src/Checked/Nucleus/Base/Stacks.ifc.beat ironclad-apps/src/Checked/Nucleus/Base/Stacks.imp.beat ironclad-apps/src/Checked/Nucleus/Base/Util.ifc.beat ironclad-apps/src/Checked/Nucleus/Base/Util.imp.beat ironclad-apps/src/Checked/Nucleus/Devices/BitVectorLemmasDevices.ifc.beat ironclad-apps/src/Checked/Nucleus/Devices/BitVectorLemmasDevices.imp.beat ironclad-apps/src/Checked/Nucleus/Devices/IntLemmasDevices.ifc.beat ironclad-apps/src/Checked/Nucleus/Devices/IntLemmasDevices.imp.beat ironclad-apps/src/Checked/Nucleus/Devices/IntelNIC.ifc.beat ironclad-apps/src/Checked/Nucleus/Devices/IntelNIC.imp.beat ironclad-apps/src/Checked/Nucleus/Devices/IoMain.ifc.beat ironclad-apps/src/Checked/Nucleus/Devices/IoMain.imp.beat ironclad-apps/src/Checked/Nucleus/Devices/PCI.ifc.beat ironclad-apps/src/Checked/Nucleus/Devices/PCI.imp.beat ironclad-apps/src/Checked/Nucleus/GC/BitVectorLemmasGc.ifc.beat ironclad-apps/src/Checked/Nucleus/GC/BitVectorLemmasGc.imp.beat ironclad-apps/src/Checked/Nucleus/GC/IntLemmasGc.ifc.beat ironclad-apps/src/Checked/Nucleus/GC/IntLemmasGc.imp.beat ironclad-apps/src/Checked/Nucleus/GC/SimpleCollector.ifc.beat ironclad-apps/src/Checked/Nucleus/GC/SimpleCollector.imp.beat ironclad-apps/src/Checked/Nucleus/GC/SimpleCommon.ifc.beat ironclad-apps/src/Checked/Nucleus/GC/SimpleCommon.imp.beat ironclad-apps/src/Checked/Nucleus/GC/SimpleGc.ifc.beat ironclad-apps/src/Checked/Nucleus/GC/SimpleGcMemory.ifc.beat ironclad-apps/src/Checked/Nucleus/GC/SimpleGcMemory.imp.beat ironclad-apps/src/Checked/Nucleus/Main/BitVectorLemmasMain.ifc.beat ironclad-apps/src/Checked/Nucleus/Main/BitVectorLemmasMain.imp.beat ironclad-apps/src/Checked/Nucleus/Main/Cube.ifc.beat ironclad-apps/src/Checked/Nucleus/Main/DafnyAssembly.ifc.beat ironclad-apps/src/Checked/Nucleus/Main/DafnyAssembly.imp.beat ironclad-apps/src/Checked/Nucleus/Main/Entry.imp.beat ironclad-apps/src/Checked/Nucleus/Main/IntLemmasMain.ifc.beat ironclad-apps/src/Checked/Nucleus/Main/IntLemmasMain.imp.beat ironclad-apps/src/Checked/Nucleus/Main/Main.ifc.beat ironclad-apps/src/Checked/Nucleus/Main/dafny_FatNatX86_i.imp.beat ironclad-apps/src/Checked/Nucleus/Main/dafny_FatNatX86big_i.imp.beat ironclad-apps/src/Checked/Nucleus/Main/dafny_FleetNatMulLoopOpt_i.imp.beat ironclad-apps/src/Checked/Nucleus/Main/dafny_FleetNatMulOpt_i.imp.beat ironclad-apps/src/Checked/Nucleus/Main/dafny_assembly_i.imp.beat ironclad-apps/src/Checked/Nucleus/Main/dafny_bit_vector_lemmas_i.imp.beat ironclad-apps/src/Checked/Nucleus/Main/dafny_io_mem_i.imp.beat ironclad-apps/src/Checked/Nucleus/Main/dafny_pci_i.imp.beat ironclad-apps/src/Checked/Nucleus/Main/dafny_sha256opt2_i.imp.beat - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.pdb files (41): ironclad-apps/boot/bootd.pdb ironclad-apps/tools/Dafny/AbsInt.pdb ironclad-apps/tools/Dafny/BVD.pdb ironclad-apps/tools/Dafny/Basetypes.pdb ironclad-apps/tools/Dafny/Boogie.pdb ironclad-apps/tools/Dafny/CodeContracts/Dafny.Contracts.pdb ironclad-apps/tools/Dafny/CodeContractsExtender.pdb ironclad-apps/tools/Dafny/Concurrency.pdb ironclad-apps/tools/Dafny/Core.pdb ironclad-apps/tools/Dafny/Dafny.pdb ironclad-apps/tools/Dafny/DafnyLanguageService.pdb ironclad-apps/tools/Dafny/DafnyMenu.pdb ironclad-apps/tools/Dafny/DafnyPipeline.pdb ironclad-apps/tools/Dafny/Doomed.pdb ironclad-apps/tools/Dafny/ExecutionEngine.pdb ironclad-apps/tools/Dafny/Graph.pdb ironclad-apps/tools/Dafny/Houdini.pdb ironclad-apps/tools/Dafny/Model.pdb ironclad-apps/tools/Dafny/ModelViewer.pdb ironclad-apps/tools/Dafny/ParserHelper.pdb ironclad-apps/tools/Dafny/Predication.pdb ironclad-apps/tools/Dafny/Provers.SMTLib.pdb ironclad-apps/tools/Dafny/VCExpr.pdb ironclad-apps/tools/Dafny/VCGeneration.pdb ironclad-apps/tools/SymDiff/AIFramework.pdb ironclad-apps/tools/SymDiff/AbsInt.pdb ironclad-apps/tools/SymDiff/Basetypes.pdb ironclad-apps/tools/SymDiff/CodeContractsExtender.pdb ironclad-apps/tools/SymDiff/Core.pdb ironclad-apps/tools/SymDiff/Graph.pdb ironclad-apps/tools/SymDiff/Model.pdb ironclad-apps/tools/SymDiff/ParserHelper.pdb ironclad-apps/tools/SymDiff/Provers.SMTLib.pdb ironclad-apps/tools/SymDiff/SymDiff.pdb ironclad-apps/tools/SymDiff/VCExpr.pdb ironclad-apps/tools/SymDiff/VCGeneration.pdb ironclad-apps/tools/fsharp/FSharp.Core.pdb ironclad-apps/tools/fsharp/FSharp.PowerPack.Build.Tasks.pdb ironclad-apps/tools/fsharp/FSharp.PowerPack.Linq.pdb ironclad-apps/tools/fsharp/FSharp.PowerPack.Metadata.pdb ironclad-apps/tools/fsharp/FSharp.PowerPack.pdb - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.config files (35): ironclad-apps/src/Clients/Benchmark/BenchmarkRequestCmd/App.config ironclad-apps/src/Clients/Benchmark/BenchmarkRequestGui/App.config ironclad-apps/src/Clients/DiffPriv/App.config ironclad-apps/src/Clients/DiffPrivSrv/App.config ironclad-apps/src/Clients/DotNetSHABench/App.config ironclad-apps/src/Clients/Notary/App.config ironclad-apps/src/Clients/NotarySrv/App.config ironclad-apps/src/Clients/PassHash/App.config ironclad-apps/src/Clients/PassHashSrv/App.config ironclad-apps/src/Clients/TrInc/App.config ironclad-apps/src/Clients/TrIncSrv/App.config ironclad-apps/src/Clients/UdpEchoClient/App.config ironclad-apps/src/DafnyTestDriver/DafnyTestDriver/App.config ironclad-apps/tools/Dafny/BVD.exe.config ironclad-apps/tools/Dafny/Dafny.exe.config ironclad-apps/tools/Dafny/Dafny.vshost.exe.config ironclad-apps/tools/NuBuild/AzureManager/App.config ironclad-apps/tools/NuBuild/CloudExecutionEngine/App.config ironclad-apps/tools/NuBuild/CloudExecutionWorker/app.config ironclad-apps/tools/NuBuild/CloudQueueTool/App.config ironclad-apps/tools/NuBuild/ItemCacheTool/App.config ironclad-apps/tools/NuBuild/NuBuild/App.config ironclad-apps/tools/NuBuild2/AzureManager/App.config ironclad-apps/tools/NuBuild2/CloudExecutionEngine/App.config ironclad-apps/tools/NuBuild2/CloudExecutionWorker/app.config ironclad-apps/tools/NuBuild2/CloudQueueTool/App.config ironclad-apps/tools/NuBuild2/ItemCacheTool/App.config ironclad-apps/tools/NuBuild2/NuBuild/App.config ironclad-apps/tools/NuBuild2/NuBuildExecutionService/csx/Release/roles/CloudExecutionWorker/base/x64/WaHostBootstrapper.exe.config ironclad-apps/tools/SymDiff/SymDiff.exe.config ironclad-apps/tools/SymDiff/SymDiff.vshost.exe.config ironclad-apps/tools/build/x86_x86/cl.exe.config ironclad-apps/tools/build/x86_x86/link.exe.config ironfleet/src/RedisClient/IronfleetShtClient/App.config ironfleet/src/RedisClient/IronfleetShtClient/packages.config - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.sln files (22): ironclad-apps/src/Clients/Benchmark.sln ironclad-apps/src/Clients/Clients.sln ironclad-apps/src/Clients/UdpEchoClient.sln ironclad-apps/src/DafnyTestDriver/DafnyTestDriver.sln ironclad-apps/tools/DafnyCC/DafnyCC.sln ironclad-apps/tools/DafnySpec/DafnySpec.sln ironclad-apps/tools/NuBuild/NuBuild.sln ironclad-apps/tools/NuBuild2/NuBuild.sln ironclad-apps/tools/standalone/StandAloneSupport.sln ironfleet/src/CreateIronServiceCerts/CreateIronServiceCerts.sln ironfleet/src/IronLockServer/IronLockServer.sln ironfleet/src/IronRSLClient/IronRSLClient.sln ironfleet/src/IronRSLCounterClient/IronRSLCounterClient.sln ironfleet/src/IronRSLCounterServer/IronRSLCounterServer.sln ironfleet/src/IronRSLKVClient/IronRSLKVClient.sln ironfleet/src/IronRSLKVServer/IronRSLKVServer.sln ironfleet/src/IronSHTClient/IronSHTClient.sln ironfleet/src/IronSHTServer/IronSHTServer.sln ironfleet/src/RedisClient/IronfleetShtClient.sln ironfleet/src/TestIoFramework/TestIoFramework.sln ironfleet/tools/scripts/integration-project/build.sln ironfleet/tools/scripts/integration-project/make-project.sln - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.basm files (22): ironclad-apps/src/Checked/Nucleus/Main/dafny_sha256opt_i.imp.basm ironclad-apps/src/Trusted/Spec/AppLoaderContract.ifc.basm ironclad-apps/src/Trusted/Spec/AppLoaderContract.imp.basm ironclad-apps/src/Trusted/Spec/AssemblySpec.ifc.basm ironclad-apps/src/Trusted/Spec/AssemblySpec.imp.basm ironclad-apps/src/Trusted/Spec/BaseSpec.ifc.basm ironclad-apps/src/Trusted/Spec/BaseSpec.imp.basm ironclad-apps/src/Trusted/Spec/ExtendedAssembly.ifc.basm ironclad-apps/src/Trusted/Spec/ExtendedAssembly.imp.basm ironclad-apps/src/Trusted/Spec/IntSpec.ifc.basm ironclad-apps/src/Trusted/Spec/IntSpec.imp.basm ironclad-apps/src/Trusted/Spec/InterruptsSpec.ifc.basm ironclad-apps/src/Trusted/Spec/InterruptsSpec.imp.basm ironclad-apps/src/Trusted/Spec/IoSpec.ifc.basm ironclad-apps/src/Trusted/Spec/IoSpec.imp.basm ironclad-apps/src/Trusted/Spec/IoTypesSpec.ifc.basm ironclad-apps/src/Trusted/Spec/IoTypesSpec.imp.basm ironclad-apps/src/Trusted/Spec/MachineStateSpec.ifc.basm ironclad-apps/src/Trusted/Spec/MachineStateSpec.imp.basm ironclad-apps/src/Trusted/Spec/MemorySpec.ifc.basm ironclad-apps/src/Trusted/Spec/MemorySpec.imp.basm ironclad-apps/src/Trusted/Spec/Overflow.ifc.basm - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *. files (14): ironclad-apps/makefile ironclad-apps/src/Checked/BootLoader/SingLdrPc/makefile ironclad-apps/src/Clients/Benchmark/notes ironclad-apps/tools/Beat/makefile ironclad-apps/tools/BoogieAsm/makefile ironclad-apps/tools/Dafny/README ironclad-apps/tools/DafnyCC/Makefile ironclad-apps/tools/DafnySpec/Makefile ironclad-apps/tools/LineCount/makefile ironclad-apps/tools/NuBuild/makefile ironclad-apps/tools/NuBuild2/makefile ironfleet/LICENSE ironfleet/SConstruct ironfleet/tools/scripts/expand-tabs-in-place - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.bpl files (11): ironclad-apps/src/Trusted/Spec/Assembly_axioms.bpl ironclad-apps/src/Trusted/Spec/Base_axioms.bpl ironclad-apps/src/Trusted/Spec/BitVector_axioms.bpl ironclad-apps/src/Trusted/Spec/IntSpec_axioms.bpl ironclad-apps/src/Trusted/Spec/Io_axioms.bpl ironclad-apps/src/Trusted/Spec/Memory_axioms.bpl ironclad-apps/src/Trusted/Spec/NucleusInvCopying.bpl ironclad-apps/src/Trusted/Spec/Word_axioms.bpl ironclad-apps/tools/Dafny/DafnyPrelude.bpl ironclad-apps/tools/DafnyCC/blueprints/Analyze.bpl ironclad-apps/tools/DafnyCC/blueprints/RegAlloc.bpl - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.stitch files (11): ironclad-apps/src/Trusted/Spec/AddPerf/AppRequirements.ifc.stitch ironclad-apps/src/Trusted/Spec/AppLoader/AppRequirements.ifc.stitch ironclad-apps/src/Trusted/Spec/BenchmarkApp/AppRequirements.ifc.stitch ironclad-apps/src/Trusted/Spec/BenchmarkService/AppRequirements.ifc.stitch ironclad-apps/src/Trusted/Spec/DafnyCCTest/AppRequirements.ifc.stitch ironclad-apps/src/Trusted/Spec/DiffPriv/AppRequirements.ifc.stitch ironclad-apps/src/Trusted/Spec/Entry.ifc.basm.stitch ironclad-apps/src/Trusted/Spec/Notary/AppRequirements.ifc.stitch ironclad-apps/src/Trusted/Spec/PassHash/AppRequirements.ifc.stitch ironclad-apps/src/Trusted/Spec/TPMTest/AppRequirements.ifc.stitch ironclad-apps/src/Trusted/Spec/TrInc/AppRequirements.ifc.stitch - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.fsl files (4): ironclad-apps/tools/Beat/lex.fsl ironclad-apps/tools/BoogieAsm/lex.fsl ironclad-apps/tools/DafnySpec/Parser/lex.fsl ironclad-apps/tools/LineCount/lex.fsl - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.lib files (3): ironclad-apps/tools/Dafny/libiz3.lib ironclad-apps/tools/Dafny/z3.lib ironclad-apps/tools/Dafny/z3_dbg.lib - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.fsy files (3): ironclad-apps/tools/Beat/parse.fsy ironclad-apps/tools/BoogieAsm/parse.fsy ironclad-apps/tools/DafnySpec/Parser/parse.fsy - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.manifest files (3): ironclad-apps/tools/Dafny/Boogie.vshost.exe.manifest ironclad-apps/tools/Dafny/Dafny.vshost.exe.manifest ironclad-apps/tools/SymDiff/SymDiff.vshost.exe.manifest - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.vsix files (2): ironclad-apps/tools/Dafny/DafnyLanguageService.vsix ironclad-apps/tools/Dafny/DafnyMenu.vsix - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.wadcfg files (2): ironclad-apps/tools/NuBuild/NuBuildExecutionService/CloudExecutionWorkerContent/diagnostics.wadcfg ironclad-apps/tools/NuBuild2/NuBuildExecutionService/CloudExecutionWorkerContent/diagnostics.wadcfg - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.StyleCop files (2): ironclad-apps/tools/NuBuild/Settings.StyleCop ironclad-apps/tools/NuBuild2/Settings.StyleCop - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.sentinel files (2): ironclad-apps/IRONROOT.sentinel ironfleet/IRONROOT.sentinel - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.sx files (2): ironclad-apps/tools/SymDiff/TypedUnivBackPred2.sx ironclad-apps/tools/SymDiff/UnivBackPred2.sx - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.batch files (2): ironclad-apps/src/Dafny/Apps/apps.dfy.batch ironfleet/src/Dafny/Distributed/apps.dfy.batch - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.log files (1): ironclad-apps/tools/NuBuild2/modules.log - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.pkgdef files (1): ironclad-apps/tools/Dafny/DafnyMenu.pkgdef - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.suo files (1): ironclad-apps/tools/Dafny/Boogie.suo - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.result files (1): ironclad-apps/tools/NuBuild2/modules.result - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.disabled files (1): ironclad-apps/src/Dafny/Drivers/TPM/tpm-device.s.dfy.disabled - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.pyproj files (1): ironfleet/tools/scripts/integration-project/build.pyproj - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.plan files (1): ironclad-apps/src/Checked/Nucleus/Main/sha256opt2.plan - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.settings files (1): ironclad-apps/src/Clients/Benchmark/BenchmarkRequestGui/Properties/Settings.settings - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.whitelist files (1): ironclad-apps/src/Checked/Nucleus/Main/axiom.whitelist - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - *.plan2 files (1): ironclad-apps/src/Checked/Nucleus/Main/sha256opt2.plan2 - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -