Using the verified log transformer, the current number of log entries is stored as a nat in a separate file (Count). Having a separate file can be avoided by letting the snapshot_interval be a fixed-size "machine" integer, e.g., of type int31, and storing the current number of log entries as such an integer at the head of the Log file. This would require having an operation that replaces the head of a file while leaving the rest intact. Note that overflow is impossible because one can prove that the count is always less than snapshot_interval.
Using the verified log transformer, the current number of log entries is stored as a
natin a separate file (Count). Having a separate file can be avoided by letting thesnapshot_intervalbe a fixed-size "machine" integer, e.g., of typeint31, and storing the current number of log entries as such an integer at the head of theLogfile. This would require having an operation that replaces the head of a file while leaving the rest intact. Note that overflow is impossible because one can prove that the count is always less thansnapshot_interval.