mylsm-lsm-store@0.5.0.0 relies on unsafe/foreign

0x4fcd94fa965aa1443134557fd075a483

no description

mylsm-lsm-store@0.5.0.0 by FabianVegaA

Earlier versions (5)

Published: 2026-10-08
Size: 533,314 bytes, 58 files
License: BSD (LICENSE)
Declarations: 0 laws (0 proved), 1216 defs, 85 types

Import

import mylsm-lsm-store@0.5.0.0/mylsm.bend as Mylsm
import 0x4fcd94fa965aa1443134557fd075a483/mylsm.bend as Mylsm
import mylsm-lsm-store@0.5.0.0/src/BitTree.bend as BitTree
import 0x4fcd94fa965aa1443134557fd075a483/src/BitTree.bend as BitTree
import mylsm-lsm-store@0.5.0.0/src/Compact.bend as Compact
import 0x4fcd94fa965aa1443134557fd075a483/src/Compact.bend as Compact
import mylsm-lsm-store@0.5.0.0/src/CompactIo.bend as CompactIo
import 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.bend as CompactIo
import mylsm-lsm-store@0.5.0.0/src/Console.bend as Console
import 0x4fcd94fa965aa1443134557fd075a483/src/Console.bend as Console
import mylsm-lsm-store@0.5.0.0/src/CrashPoint.bend as CrashPoint
import 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.bend as CrashPoint
import mylsm-lsm-store@0.5.0.0/src/CrashPointPolicy.bend as CrashPointPolicy
import 0x4fcd94fa965aa1443134557fd075a483/src/CrashPointPolicy.bend as CrashPointPolicy
import mylsm-lsm-store@0.5.0.0/src/Db.bend as Db
import 0x4fcd94fa965aa1443134557fd075a483/src/Db.bend as Db
import mylsm-lsm-store@0.5.0.0/src/DbIo.bend as DbIo
import 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.bend as DbIo
import mylsm-lsm-store@0.5.0.0/src/DbLock.bend as DbLock
import 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.bend as DbLock
import mylsm-lsm-store@0.5.0.0/src/DbLockPolicy.bend as DbLockPolicy
import 0x4fcd94fa965aa1443134557fd075a483/src/DbLockPolicy.bend as DbLockPolicy
import mylsm-lsm-store@0.5.0.0/src/DurableBatchPolicy.bend as DurableBatchPolicy
import 0x4fcd94fa965aa1443134557fd075a483/src/DurableBatchPolicy.bend as DurableBatchPolicy
import mylsm-lsm-store@0.5.0.0/src/DurableCommit.bend as DurableCommit
import 0x4fcd94fa965aa1443134557fd075a483/src/DurableCommit.bend as DurableCommit
import mylsm-lsm-store@0.5.0.0/src/DurableDb.bend as DurableDb
import 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.bend as DurableDb
import mylsm-lsm-store@0.5.0.0/src/DurableDbPolicy.bend as DurableDbPolicy
import 0x4fcd94fa965aa1443134557fd075a483/src/DurableDbPolicy.bend as DurableDbPolicy
import mylsm-lsm-store@0.5.0.0/src/DurableError.bend as DurableError
import 0x4fcd94fa965aa1443134557fd075a483/src/DurableError.bend as DurableError
import mylsm-lsm-store@0.5.0.0/src/Flush.bend as Flush
import 0x4fcd94fa965aa1443134557fd075a483/src/Flush.bend as Flush
import mylsm-lsm-store@0.5.0.0/src/FlushPolicy.bend as FlushPolicy
import 0x4fcd94fa965aa1443134557fd075a483/src/FlushPolicy.bend as FlushPolicy
import mylsm-lsm-store@0.5.0.0/src/Fs.bend as Fs
import 0x4fcd94fa965aa1443134557fd075a483/src/Fs.bend as Fs
import mylsm-lsm-store@0.5.0.0/src/FsPolicy.bend as FsPolicy
import 0x4fcd94fa965aa1443134557fd075a483/src/FsPolicy.bend as FsPolicy
import mylsm-lsm-store@0.5.0.0/src/Keys.bend as Keys
import 0x4fcd94fa965aa1443134557fd075a483/src/Keys.bend as Keys
import mylsm-lsm-store@0.5.0.0/src/Manifest.bend as Manifest
import 0x4fcd94fa965aa1443134557fd075a483/src/Manifest.bend as Manifest
import mylsm-lsm-store@0.5.0.0/src/MemTable.bend as MemTable
import 0x4fcd94fa965aa1443134557fd075a483/src/MemTable.bend as MemTable
import mylsm-lsm-store@0.5.0.0/src/MergeIter.bend as MergeIter
import 0x4fcd94fa965aa1443134557fd075a483/src/MergeIter.bend as MergeIter
import mylsm-lsm-store@0.5.0.0/src/Recover.bend as Recover
import 0x4fcd94fa965aa1443134557fd075a483/src/Recover.bend as Recover
import mylsm-lsm-store@0.5.0.0/src/RecoverPure.bend as RecoverPure
import 0x4fcd94fa965aa1443134557fd075a483/src/RecoverPure.bend as RecoverPure
import mylsm-lsm-store@0.5.0.0/src/SortedRun.bend as SortedRun
import 0x4fcd94fa965aa1443134557fd075a483/src/SortedRun.bend as SortedRun
import mylsm-lsm-store@0.5.0.0/src/SstFile.bend as SstFile
import 0x4fcd94fa965aa1443134557fd075a483/src/SstFile.bend as SstFile
import mylsm-lsm-store@0.5.0.0/src/SstStreamIo.bend as SstStreamIo
import 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.bend as SstStreamIo
import mylsm-lsm-store@0.5.0.0/src/Sstable.bend as Sstable
import 0x4fcd94fa965aa1443134557fd075a483/src/Sstable.bend as Sstable
import mylsm-lsm-store@0.5.0.0/src/StorageBytes.bend as StorageBytes
import 0x4fcd94fa965aa1443134557fd075a483/src/StorageBytes.bend as StorageBytes
import mylsm-lsm-store@0.5.0.0/src/Wal.bend as Wal
import 0x4fcd94fa965aa1443134557fd075a483/src/Wal.bend as Wal
import mylsm-lsm-store@0.5.0.0/src/hub_sha/core.bend as Core
import 0x4fcd94fa965aa1443134557fd075a483/src/hub_sha/core.bend as Core
import mylsm-lsm-store@0.5.0.0/src/hub_sha/sha256.bend as Sha256
import 0x4fcd94fa965aa1443134557fd075a483/src/hub_sha/sha256.bend as Sha256
import mylsm-lsm-store@0.5.0.0/src/hub_sha/state.bend as State
import 0x4fcd94fa965aa1443134557fd075a483/src/hub_sha/state.bend as State

Modules

mylsm.bend 111 declarations
src/BitTree.bend 36 declarations
src/Compact.bend 50 declarations
src/CompactIo.bend 22 declarations
src/Console.bend 2 declarations
src/CrashPoint.bend 3 declarations
src/CrashPointPolicy.bend 2 declarations
src/Db.bend 48 declarations
src/DbIo.bend 24 declarations
src/DbLock.bend 16 declarations
src/DbLockPolicy.bend 5 declarations
src/DurableBatchPolicy.bend 7 declarations
src/DurableCommit.bend 6 declarations
src/DurableDb.bend 51 declarations
src/DurableDbPolicy.bend 15 declarations
src/DurableError.bend 39 declarations
src/Flush.bend 44 declarations
src/FlushPolicy.bend 1 declarations
src/Fs.bend 20 declarations
src/FsPolicy.bend 2 declarations
src/Keys.bend 24 declarations
src/Manifest.bend 115 declarations
src/MemTable.bend 27 declarations
src/MergeIter.bend 6 declarations
src/Recover.bend 118 declarations
src/RecoverPure.bend 23 declarations
src/SortedRun.bend 52 declarations
src/SstFile.bend 191 declarations
src/SstStreamIo.bend 55 declarations
src/Sstable.bend 81 declarations
src/StorageBytes.bend 33 declarations
src/Wal.bend 66 declarations
src/hub_sha/core.bend 164 declarations — Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f
src/hub_sha/sha256.bend 20 declarations — Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f
src/hub_sha/state.bend 2 declarations — Vendored from bend-collections 0x9ee2e9a299991dcc089fe22c7f3ceb5f

Other files

Dependencies

bend-kit-bytes@0.3.2.0 via mylsm.bend: import bend-kit-bytes@0.3.2.0/bytes.bend as Bytes
0x9ee2e9a2 via src/BitTree.bend: import 0x9ee2e9a299991dcc089fe22c7f3ceb5f/src/containers/bitset.bend as BitWords
bend-kit-files@0.1.1.0 via src/Fs.bend: import 0x6c54b2522c2258baf6f58d2b970c3902/files.bend as PackedFiles
bend-mathlib@0.7.0.0 via src/Keys.bend: import bend-mathlib@0.7.0.0/string.bend as MString

Dependents

No package in this build imports it.

Status on bend 2.0.36

File	Status	Checker says	Time
mylsm.bend	relies on unsafe/foreign	248 defs rely on unsafe or foreign code defs: `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.remove`, `0x6c54b2522c2258baf6f58d2b970c3902/files.rename`, `0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat`, `0x6c54b2522c2258baf6f58d2b970c3902/files.exists`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.encoded`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.run`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.valid`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.mfst_opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.load_mfst`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.dir_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.ensure_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.written`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_drift`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.loaded`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.written`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.ensured`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pre`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_frozen`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pick`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict_start`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.directory_synced`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.written`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.drift_go`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.loaded`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.written`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.ensured`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_pre`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_trig`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.exact.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.load_tables`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.load_levels`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.exact.start`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.truncate.result`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.truncate`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.decode`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.body.bound`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.body`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.bound`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length.checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length.value`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.remaining`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.end`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header.decoded`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header.truncated`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.file`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.size`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.present`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_open.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_open`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_one`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_get`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_cnt`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_part.initialized`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_part`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels_checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels.loaded`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_names_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root_cnt`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.swept`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.ensured`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_remove_list`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked_count`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked_path`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dir.result`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dirs`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_sweep_result`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing.present`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_locked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_initialized`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_published`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_written`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_locked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.flush_dec`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.flush_gate`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_once.flushed`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_once`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_pick`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain.flushed`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain.drained`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain_unwrap`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.write`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.put`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.del`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.DbLock.try_lock`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.DbLock.try_unlock`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.lock_file`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.acquire`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.unlock_file`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.release`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.open_result`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.locked_result`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.preflight_manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.preflight_result`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.open_existing`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.create_locked`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.created_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.create`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.close`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.committed_result`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.batch_result`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.batch_count_result`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.batch_count`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.write_batch`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.put`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.delete`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.flush_result`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.compact_result`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.flush`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.compact`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_names`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_levels`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_active_manifest_size`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_active_manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_io`, `0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats`, `open_recovering`, `create`, `open_existing`, `write_batch`, `put`, `delete`, `flush`, `compact`, `stats`, `close`, `Session.put`, `Session.delete`, `Session.write_batch`, `Session.flush`, `Session.compact`, `Session.stats`, `Session.finish`, `Session.finish_pair`, `Session.run_opened`, `create_database`, `open_database` output SOME PROOFS FAIL Error: 248 defs rely on unsafe or foreign code: - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir - 0x6c54b2522c2258baf6f58d2b970c3902/files.remove - 0x6c54b2522c2258baf6f58d2b970c3902/files.rename - 0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.read.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.write.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat - 0x6c54b2522c2258baf6f58d2b970c3902/files.exists - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table - 0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line - 0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file.opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes.opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.encoded - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.loop - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.run - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.valid - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.mfst_opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.load_mfst - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.dir_tail - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.ensure_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.synced - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.written - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_drift - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.loaded - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.synced - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.written - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.ensured - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pre - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_frozen - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pick - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict_start - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.directory_synced - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.written - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.drift_go - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.loaded - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.synced - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.written - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.ensured - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_pre - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_trig - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.exact.loop - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.load_tables - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.load_levels - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.exact.start - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.truncate.result - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.truncate - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.decode - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.body.bound - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.body - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.bound - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length.checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length.value - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.remaining - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.end - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header.decoded - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header.truncated - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.file - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.size - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.present - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_open.exists - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_open - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_one - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_get - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_cnt - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_part.initialized - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_part - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels_checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels.loaded - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_names_go - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root_go - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root_cnt - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.swept - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.manifest - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.ensured - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_remove_list - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked_count - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked_path - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dir.result - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dirs - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_sweep_result - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_manifest - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing.present - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_locked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_initialized - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_published - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_written - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_locked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.flush_dec - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.flush_gate - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_once.flushed - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_once - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_pick - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_go - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain.flushed - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain.drained - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain_unwrap - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.write - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.put - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.del - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.DbLock.try_lock - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.DbLock.try_unlock - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.lock_file - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.acquire - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.unlock_file - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.release - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.open_result - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.locked_result - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.preflight_manifest - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.preflight_result - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.open_existing - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.create_locked - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.created_dir - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.create - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.close - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.committed_result - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.batch_result - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.batch_count_result - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.batch_count - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.write_batch - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.put - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.delete - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.flush_result - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.compact_result - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.flush - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.compact - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_names - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_levels - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_active_manifest_size - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_active_manifest - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats_io - 0x4fcd94fa965aa1443134557fd075a483/src/DurableDb.stats - open_recovering - create - open_existing - write_batch - put - delete - flush - compact - stats - close - Session.put - Session.delete - Session.write_batch - Session.flush - Session.compact - Session.stats - Session.finish - Session.finish_pair - Session.run_opened - create_database - open_database	4.5 s
src/BitTree.bend	checks	ALL PROOFS CHECK	0.9 s
src/Compact.bend	checks	ALL PROOFS CHECK	3.6 s
src/CompactIo.bend	relies on unsafe/foreign	123 defs rely on unsafe or foreign code defs: `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.remove`, `0x6c54b2522c2258baf6f58d2b970c3902/files.rename`, `0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat`, `0x6c54b2522c2258baf6f58d2b970c3902/files.exists`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.encoded`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.run`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.valid`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.mfst_opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.load_mfst`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.dir_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.ensure_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.written`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_drift`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.loaded`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.written`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.ensured`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pre`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_frozen`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pick`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush`, `remove_list`, `remove_list_strict`, `remove_list_strict_start`, `compact_goB.directory_synced`, `compact_goB.renamed`, `compact_goB.written`, `compact_goB`, `drift_go`, `compact_goA.loaded`, `compact_goA.synced`, `compact_goA.renamed`, `compact_goA.written`, `compact_goA.ensured`, `compact_goA`, `compact_pre`, `compact_trig`, `compact` output SOME PROOFS FAIL Error: 123 defs rely on unsafe or foreign code: - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir - 0x6c54b2522c2258baf6f58d2b970c3902/files.remove - 0x6c54b2522c2258baf6f58d2b970c3902/files.rename - 0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.read.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.write.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat - 0x6c54b2522c2258baf6f58d2b970c3902/files.exists - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table - 0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line - 0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file.opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes.opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.encoded - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.loop - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.run - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.valid - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.mfst_opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.load_mfst - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.dir_tail - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.ensure_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.synced - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.written - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_drift - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.loaded - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.synced - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.written - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.ensured - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pre - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_frozen - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pick - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush - remove_list - remove_list_strict - remove_list_strict_start - compact_goB.directory_synced - compact_goB.renamed - compact_goB.written - compact_goB - drift_go - compact_goA.loaded - compact_goA.synced - compact_goA.renamed - compact_goA.written - compact_goA.ensured - compact_goA - compact_pre - compact_trig - compact	4.5 s
src/Console.bend	relies on unsafe/foreign	2 defs rely on unsafe or foreign code defs: `read_line`, `get_env` output SOME PROOFS FAIL Error: 2 defs rely on unsafe or foreign code: - read_line - get_env	0.6 s
src/CrashPoint.bend	relies on unsafe/foreign	5 defs rely on unsafe or foreign code defs: `0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env`, `stop`, `hit_decision`, `hit` output SOME PROOFS FAIL Error: 5 defs rely on unsafe or foreign code: - 0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line - 0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env - stop - hit_decision - hit	0.8 s
src/CrashPointPolicy.bend	checks	ALL PROOFS CHECK	0.7 s
src/Db.bend	checks	ALL PROOFS CHECK	3.4 s
src/DbIo.bend	relies on unsafe/foreign	60 defs rely on unsafe or foreign code defs: `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.remove`, `0x6c54b2522c2258baf6f58d2b970c3902/files.rename`, `0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat`, `0x6c54b2522c2258baf6f58d2b970c3902/files.exists`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit`, `wal_tail`, `wal.initialize.fsync`, `wal.initialize.synced`, `wal.initialize.written`, `wal.initialize.opened`, `wal.initialize.header`, `wal.initialize.header_if_empty`, `wal.initialize.existing`, `wal.initialize.present`, `wal.initialize.exists`, `wal_initialize`, `wal_encoded`, `wal_append`, `append_synced`, `append_written`, `append_opened`, `append_frame`, `encoded_append`, `wal_commit`, `db_write_durable`, `db_write`, `db_put`, `db_write_staged`, `db_del` output SOME PROOFS FAIL Error: 60 defs rely on unsafe or foreign code: - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir - 0x6c54b2522c2258baf6f58d2b970c3902/files.remove - 0x6c54b2522c2258baf6f58d2b970c3902/files.rename - 0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.read.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.write.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat - 0x6c54b2522c2258baf6f58d2b970c3902/files.exists - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line - 0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit - wal_tail - wal.initialize.fsync - wal.initialize.synced - wal.initialize.written - wal.initialize.opened - wal.initialize.header - wal.initialize.header_if_empty - wal.initialize.existing - wal.initialize.present - wal.initialize.exists - wal_initialize - wal_encoded - wal_append - append_synced - append_written - append_opened - append_frame - encoded_append - wal_commit - db_write_durable - db_write - db_put - db_write_staged - db_del	4.2 s
src/DbLock.bend	relies on unsafe/foreign	7 defs rely on unsafe or foreign code defs: `DbLock.try_lock`, `DbLock.try_unlock`, `lock_file`, `opened`, `acquire`, `unlock_file`, `release` output SOME PROOFS FAIL Error: 7 defs rely on unsafe or foreign code: - DbLock.try_lock - DbLock.try_unlock - lock_file - opened - acquire - unlock_file - release	1.8 s
src/DbLockPolicy.bend	checks	ALL PROOFS CHECK	2.2 s
src/DurableBatchPolicy.bend	checks	ALL PROOFS CHECK	0.7 s
src/DurableCommit.bend	checks	ALL PROOFS CHECK	3.8 s
src/DurableDb.bend	relies on unsafe/foreign	227 defs rely on unsafe or foreign code defs: `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.DbLock.try_lock`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.DbLock.try_unlock`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.lock_file`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.acquire`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.unlock_file`, `0x4fcd94fa965aa1443134557fd075a483/src/DbLock.release`, `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.remove`, `0x6c54b2522c2258baf6f58d2b970c3902/files.rename`, `0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat`, `0x6c54b2522c2258baf6f58d2b970c3902/files.exists`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.encoded`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.run`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.valid`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.mfst_opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.load_mfst`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.dir_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.ensure_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.written`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_drift`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.loaded`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.written`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.ensured`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pre`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_frozen`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pick`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict_start`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.directory_synced`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.written`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.drift_go`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.loaded`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.written`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.ensured`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_pre`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_trig`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.exact.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.load_tables`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.load_levels`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.exact.start`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.truncate.result`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.truncate`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.decode`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.body.bound`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.body`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.bound`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length.checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length.value`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.remaining`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.end`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header.decoded`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header.truncated`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.file`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.size`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.present`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_open.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_open`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_one`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_get`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_cnt`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_part.initialized`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_part`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels_checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels.loaded`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_names_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root_cnt`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.swept`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.ensured`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_remove_list`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked_count`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked_path`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dir.result`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dirs`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_sweep_result`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_checked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing.present`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_locked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_initialized`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_published`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_written`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_locked`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.flush_dec`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.flush_gate`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_once.flushed`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_once`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_pick`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain.flushed`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain.drained`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain_unwrap`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.write`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.put`, `0x4fcd94fa965aa1443134557fd075a483/src/Recover.del`, `open_result`, `locked_result`, `preflight_manifest`, `preflight_result`, `open_existing`, `create_locked`, `created_dir`, `create`, `close`, `committed_result`, `batch_result`, `batch_count_result`, `batch_count`, `write_batch`, `put`, `delete`, `flush_result`, `compact_result`, `flush`, `compact`, `stats_names`, `stats_levels`, `stats_active_manifest_size`, `stats_active_manifest`, `stats_io`, `stats` output SOME PROOFS FAIL Error: 227 defs rely on unsafe or foreign code: - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.DbLock.try_lock - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.DbLock.try_unlock - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.lock_file - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.acquire - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.unlock_file - 0x4fcd94fa965aa1443134557fd075a483/src/DbLock.release - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir - 0x6c54b2522c2258baf6f58d2b970c3902/files.remove - 0x6c54b2522c2258baf6f58d2b970c3902/files.rename - 0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.read.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.write.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat - 0x6c54b2522c2258baf6f58d2b970c3902/files.exists - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line - 0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file.opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes.opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.encoded - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.loop - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.run - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.valid - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.mfst_opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.load_mfst - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.dir_tail - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.ensure_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.synced - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.written - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_drift - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.loaded - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.synced - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.written - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.ensured - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pre - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_frozen - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pick - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict_start - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.directory_synced - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.written - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.drift_go - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.loaded - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.synced - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.written - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.ensured - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_pre - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_trig - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.exact.loop - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.load_tables - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.load_levels - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.exact.start - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.truncate.result - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.truncate - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.decode - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.body.bound - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.body - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.bound - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length.checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length.value - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.length - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.remaining - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames.end - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.frames - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header.decoded - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header.truncated - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.header - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.file - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.size - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal.open.present - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_open.exists - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_open - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_one - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_get - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_cnt - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_part.initialized - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.wal_part - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels_checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels.loaded - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_levels - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_names_go - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root_go - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root_cnt - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_root - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.swept - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.manifest - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db.ensured - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_db - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_remove_list - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked_count - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_read_checked_path - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dir.result - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked_dirs - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.sweep_checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_sweep_result - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_manifest - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_checked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing.present - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.open_existing_locked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_initialized - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_published - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_written - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.create_locked - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.flush_dec - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.flush_gate - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_once.flushed - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_once - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_pick - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.drain_go - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain.flushed - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain.drained - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.maintain_unwrap - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.write - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.put - 0x4fcd94fa965aa1443134557fd075a483/src/Recover.del - open_result - locked_result - preflight_manifest - preflight_result - open_existing - create_locked - created_dir - create - close - committed_result - batch_result - batch_count_result - batch_count - write_batch - put - delete - flush_result - compact_result - flush - compact - stats_names - stats_levels - stats_active_manifest_size - stats_active_manifest - stats_io - stats	4.3 s
src/DurableDbPolicy.bend	checks	ALL PROOFS CHECK	2.0 s
src/DurableError.bend	checks	ALL PROOFS CHECK	2.0 s
src/Flush.bend	relies on unsafe/foreign	106 defs rely on unsafe or foreign code defs: `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.remove`, `0x6c54b2522c2258baf6f58d2b970c3902/files.rename`, `0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat`, `0x6c54b2522c2258baf6f58d2b970c3902/files.exists`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del`, `write_tail.chmod`, `write_tail.fsync`, `write_tail`, `write_file.opened`, `write_file`, `write_manifest.bytes.opened`, `write_manifest.bytes`, `write_manifest.encoded`, `write_manifest`, `manifest.read.loop`, `manifest.read.size.run`, `manifest.read.size.valid`, `manifest.read.size`, `mfst_opened`, `load_mfst`, `dir_tail`, `ensure_dir`, `flush_goB.synced`, `flush_goB.renamed`, `flush_goB.written`, `flush_goB`, `flush_drift`, `flush_goA.loaded`, `flush_goA.synced`, `flush_goA.renamed`, `flush_goA.written`, `flush_goA.ensured`, `flush_goA`, `flush_pre`, `flush_frozen`, `flush_pick`, `flush` output SOME PROOFS FAIL Error: 106 defs rely on unsafe or foreign code: - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir - 0x6c54b2522c2258baf6f58d2b970c3902/files.remove - 0x6c54b2522c2258baf6f58d2b970c3902/files.rename - 0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.read.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.write.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat - 0x6c54b2522c2258baf6f58d2b970c3902/files.exists - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table - 0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line - 0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del - write_tail.chmod - write_tail.fsync - write_tail - write_file.opened - write_file - write_manifest.bytes.opened - write_manifest.bytes - write_manifest.encoded - write_manifest - manifest.read.loop - manifest.read.size.run - manifest.read.size.valid - manifest.read.size - mfst_opened - load_mfst - dir_tail - ensure_dir - flush_goB.synced - flush_goB.renamed - flush_goB.written - flush_goB - flush_drift - flush_goA.loaded - flush_goA.synced - flush_goA.renamed - flush_goA.written - flush_goA.ensured - flush_goA - flush_pre - flush_frozen - flush_pick - flush	4.4 s
src/FlushPolicy.bend	checks	ALL PROOFS CHECK	0.7 s
src/Fs.bend	relies on unsafe/foreign	31 defs rely on unsafe or foreign code defs: `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.remove`, `0x6c54b2522c2258baf6f58d2b970c3902/files.rename`, `0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat`, `0x6c54b2522c2258baf6f58d2b970c3902/files.exists`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all`, `read_words`, `write_words`, `read_bytes`, `write_bytes`, `fsync`, `truncate`, `rename`, `remove`, `read_dir_count`, `read_dir_at`, `make_dir`, `chmod`, `exists`, `file_size`, `read_go`, `read_dir` output SOME PROOFS FAIL Error: 31 defs rely on unsafe or foreign code: - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir - 0x6c54b2522c2258baf6f58d2b970c3902/files.remove - 0x6c54b2522c2258baf6f58d2b970c3902/files.rename - 0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.read.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.write.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat - 0x6c54b2522c2258baf6f58d2b970c3902/files.exists - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all - read_words - write_words - read_bytes - write_bytes - fsync - truncate - rename - remove - read_dir_count - read_dir_at - make_dir - chmod - exists - file_size - read_go - read_dir	1.4 s
src/FsPolicy.bend	checks	ALL PROOFS CHECK	0.8 s
src/Keys.bend	checks	ALL PROOFS CHECK	1.8 s
src/Manifest.bend	checks	ALL PROOFS CHECK	2.0 s
src/MemTable.bend	checks	ALL PROOFS CHECK	1.8 s
src/MergeIter.bend	checks	ALL PROOFS CHECK	1.7 s
src/Recover.bend	relies on unsafe/foreign	194 defs rely on unsafe or foreign code defs: `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.remove`, `0x6c54b2522c2258baf6f58d2b970c3902/files.rename`, `0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat`, `0x6c54b2522c2258baf6f58d2b970c3902/files.exists`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder`, `0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line`, `0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision`, `0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged`, `0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes.opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.encoded`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.loop`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.run`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.valid`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.mfst_opened`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.load_mfst`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.dir_tail`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.ensure_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.written`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_drift`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.loaded`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.written`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.ensured`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pre`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_frozen`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pick`, `0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict_start`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.directory_synced`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.written`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.drift_go`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.loaded`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.synced`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.renamed`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.written`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.ensured`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_pre`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_trig`, `0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact`, `exact.loop`, `load_tables`, `load_levels`, `exact.start`, `wal.truncate.result`, `wal.truncate`, `wal.frames.decode`, `wal.frames.body.bound`, `wal.frames.body`, `wal.frames.bound`, `wal.frames.length.checked`, `wal.frames.length.value`, `wal.frames.length`, `wal.frames.remaining`, `wal.frames.end`, `wal.frames`, `wal.header.decoded`, `wal.header.truncated`, `wal.header`, `wal.open.file`, `wal.open.size`, `wal.open.present`, `wal_open.exists`, `wal_open`, `sweep_one`, `sweep_get`, `sweep_cnt`, `sweep_dir`, `wal_part.initialized`, `wal_part`, `open_levels_checked`, `open_levels.loaded`, `open_levels`, `open_names_go`, `sweep_root_go`, `sweep_root_cnt`, `sweep_root`, `open_db.swept`, `open_db.manifest`, `open_db.ensured`, `open_db`, `sweep_checked_remove_list`, `sweep_read_checked`, `sweep_read_checked_count`, `sweep_read_checked_path`, `sweep_checked_dir.result`, `sweep_checked_dir`, `sweep_checked_dirs`, `sweep_checked`, `open_existing_sweep_result`, `open_existing_manifest`, `open_existing_checked`, `open_existing.present`, `open_existing_locked`, `create_initialized`, `create_published`, `create_written`, `create_locked`, `flush_dec`, `flush_gate`, `drain_once.flushed`, `drain_once`, `drain_pick`, `drain_go`, `maintain.flushed`, `maintain.drained`, `maintain`, `maintain_unwrap`, `write`, `put`, `del` output SOME PROOFS FAIL Error: 194 defs rely on unsafe or foreign code: - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir - 0x6c54b2522c2258baf6f58d2b970c3902/files.remove - 0x6c54b2522c2258baf6f58d2b970c3902/files.rename - 0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.read.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.write.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat - 0x6c54b2522c2258baf6f58d2b970c3902/files.exists - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.exact.start - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.loop - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size.checked - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read.table.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.read_table - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish.synced - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.finish - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.step - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder.opened - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write.encoder - 0x4fcd94fa965aa1443134557fd075a483/src/SstStreamIo.write_table - 0x4fcd94fa965aa1443134557fd075a483/src/Console.read_line - 0x4fcd94fa965aa1443134557fd075a483/src/Console.get_env - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.stop - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit_decision - 0x4fcd94fa965aa1443134557fd075a483/src/CrashPoint.hit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_tail - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.header_if_empty - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.existing - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.present - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal.initialize.exists - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_initialize - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_encoded - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_synced - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_written - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_opened - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.append_frame - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.encoded_append - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.wal_commit - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_durable - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_put - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_write_staged - 0x4fcd94fa965aa1443134557fd075a483/src/DbIo.db_del - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_tail - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file.opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_file - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes.opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest.encoded - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.write_manifest - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.loop - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.run - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size.valid - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.manifest.read.size - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.mfst_opened - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.load_mfst - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.dir_tail - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.ensure_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.synced - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB.written - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goB - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_drift - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.loaded - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.synced - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.written - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA.ensured - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_goA - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pre - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_frozen - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush_pick - 0x4fcd94fa965aa1443134557fd075a483/src/Flush.flush - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.remove_list_strict_start - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.directory_synced - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB.written - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goB - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.drift_go - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.loaded - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.synced - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.renamed - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.written - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA.ensured - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_goA - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_pre - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact_trig - 0x4fcd94fa965aa1443134557fd075a483/src/CompactIo.compact - exact.loop - load_tables - load_levels - exact.start - wal.truncate.result - wal.truncate - wal.frames.decode - wal.frames.body.bound - wal.frames.body - wal.frames.bound - wal.frames.length.checked - wal.frames.length.value - wal.frames.length - wal.frames.remaining - wal.frames.end - wal.frames - wal.header.decoded - wal.header.truncated - wal.header - wal.open.file - wal.open.size - wal.open.present - wal_open.exists - wal_open - sweep_one - sweep_get - sweep_cnt - sweep_dir - wal_part.initialized - wal_part - open_levels_checked - open_levels.loaded - open_levels - open_names_go - sweep_root_go - sweep_root_cnt - sweep_root - open_db.swept - open_db.manifest - open_db.ensured - open_db - sweep_checked_remove_list - sweep_read_checked - sweep_read_checked_count - sweep_read_checked_path - sweep_checked_dir.result - sweep_checked_dir - sweep_checked_dirs - sweep_checked - open_existing_sweep_result - open_existing_manifest - open_existing_checked - open_existing.present - open_existing_locked - create_initialized - create_published - create_written - create_locked - flush_dec - flush_gate - drain_once.flushed - drain_once - drain_pick - drain_go - maintain.flushed - maintain.drained - maintain - maintain_unwrap - write - put - del	3.9 s
src/RecoverPure.bend	checks	ALL PROOFS CHECK	2.5 s
src/SortedRun.bend	checks	ALL PROOFS CHECK	1.8 s
src/SstFile.bend	checks	ALL PROOFS CHECK	2.9 s
src/SstStreamIo.bend	relies on unsafe/foreign	45 defs rely on unsafe or foreign code defs: `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.remove`, `0x6c54b2522c2258baf6f58d2b970c3902/files.rename`, `0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write.words`, `0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes`, `0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir`, `0x6c54b2522c2258baf6f58d2b970c3902/files.stat`, `0x6c54b2522c2258baf6f58d2b970c3902/files.exists`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go`, `0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go`, `0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir`, `exact.loop`, `exact.start`, `read.loop`, `read.table.opened`, `read.table.size.checked`, `read.table.size`, `read.table.file_size`, `read_table`, `write.finish.synced`, `write.finish`, `write.step`, `write.encoder.opened`, `write.encoder`, `write_table` output SOME PROOFS FAIL Error: 45 defs rely on unsafe or foreign code: - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat.raw - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir - 0x6c54b2522c2258baf6f58d2b970c3902/files.remove - 0x6c54b2522c2258baf6f58d2b970c3902/files.rename - 0x6c54b2522c2258baf6f58d2b970c3902/files.temp_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.read.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.read_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.write.words - 0x6c54b2522c2258baf6f58d2b970c3902/files.write_bytes - 0x6c54b2522c2258baf6f58d2b970c3902/files.list_dir - 0x6c54b2522c2258baf6f58d2b970c3902/files.stat - 0x6c54b2522c2258baf6f58d2b970c3902/files.exists - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all.go - 0x6c54b2522c2258baf6f58d2b970c3902/files.mkdir_all - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_words - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.write_bytes - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.fsync - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.truncate - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.rename - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.remove - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_count - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir_at - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.make_dir - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.chmod - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.exists - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.file_size - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_go - 0x4fcd94fa965aa1443134557fd075a483/src/Fs.read_dir - exact.loop - exact.start - read.loop - read.table.opened - read.table.size.checked - read.table.size - read.table.file_size - read_table - write.finish.synced - write.finish - write.step - write.encoder.opened - write.encoder - write_table	3.1 s
src/Sstable.bend	checks	ALL PROOFS CHECK	2.0 s
src/StorageBytes.bend	checks	ALL PROOFS CHECK	1.1 s
src/Wal.bend	checks	ALL PROOFS CHECK	3.1 s
src/hub_sha/core.bend	checks	ALL PROOFS CHECK	1.4 s
src/hub_sha/sha256.bend	checks	ALL PROOFS CHECK	1.8 s
src/hub_sha/state.bend	checks	ALL PROOFS CHECK	0.8 s