From c2ef32ad796245edc706de9dabe21391ff343296 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 21 Aug 2026 09:22:25 -0700 Subject: [PATCH] State the assumptions on Symbols, MaxOffset and BuffSz Co-authored-by: Claude Opus 5 Signed-off-by: Markus Alexander Kuppe --- .../braf/BufferedRandomAccessFile.tla | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/specifications/braf/BufferedRandomAccessFile.tla b/specifications/braf/BufferedRandomAccessFile.tla index 9f5b94a8..5abfd45d 100644 --- a/specifications/braf/BufferedRandomAccessFile.tla +++ b/specifications/braf/BufferedRandomAccessFile.tla @@ -18,6 +18,10 @@ EXTENDS Naturals, Sequences, TLC, Common CONSTANT BuffSz +\* Seek's `pos \div BuffSz` needs a nonzero divisor, and Inv2 is unsatisfiable +\* when BuffSz = 0. +ASSUME BuffSzIsPositive == BuffSz \in Nat \ {0} + VARIABLES \* in-memory variables (BufferedRandomAccessFile class fields) dirty, @@ -380,13 +384,26 @@ Spec == Init /\ [][Next]_vars \* This module contains constants and definitions common to both \* RandomAccessFile and BufferedRandomAccessFile. -EXTENDS Naturals, Sequences +EXTENDS Naturals, Sequences, FiniteSets CONSTANTS Symbols, \* data stored in the file (in reality there are 256 symbols: bytes 0x00 to 0xFF) ArbitrarySymbol, \* special token for an arbitrary symbol (to reduce the need for nondeterministic choice) MaxOffset \* the highest possible offset (in reality this is 2^63 - 1) +\* DiskF and TruncateOrExtendFile mention ArbitrarySymbol explicitly, so +\* Permutations(Symbols) is an unsound SYMMETRY set unless it is not a symbol. +ASSUME ArbitrarySymbolIsDistinct == ArbitrarySymbol \notin Symbols + +\* Permutations requires a finite set, as does enumerating SymbolOrArbitrary. +ASSUME SymbolsIsFinite == IsFiniteSet(Symbols) + +\* Not needed for soundness; without it every offset holds ArbitrarySymbol. +ASSUME SymbolsIsNonEmpty == Symbols # {} + +\* Offset == 0..MaxOffset types curr, lo, diskPos, length, and file_pointer. +ASSUME MaxOffsetIsNat == MaxOffset \in Nat + \* The set of legal offsets Offset == 0..MaxOffset