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

0x571fd57004366c423dfd4b51196743b5

no description

mylsm-lsm-store@0.4.0.0 by FabianVegaA

Other versions (5)

mylsm-lsm-store@0.5.0.0 2026-10-08 latest
mylsm-lsm-store@0.3.2.0 2026-09-27
mylsm-lsm-store@0.3.1.0 2026-09-26
mylsm-lsm-store@0.3.0.0 2026-09-25
mylsm-lsm-store@0.2.0.0 2026-09-25

Published: 2026-10-05
Size: 436,490 bytes, 52 files
License: BSD (LICENSE)
Declarations: 0 laws (0 proved), 998 defs, 53 types

Import

import mylsm-lsm-store@0.4.0.0/mylsm.bend as Mylsm
import 0x571fd57004366c423dfd4b51196743b5/mylsm.bend as Mylsm
import mylsm-lsm-store@0.4.0.0/src/BitTree.bend as BitTree
import 0x571fd57004366c423dfd4b51196743b5/src/BitTree.bend as BitTree
import mylsm-lsm-store@0.4.0.0/src/Compact.bend as Compact
import 0x571fd57004366c423dfd4b51196743b5/src/Compact.bend as Compact
import mylsm-lsm-store@0.4.0.0/src/CompactIo.bend as CompactIo
import 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.bend as CompactIo
import mylsm-lsm-store@0.4.0.0/src/Console.bend as Console
import 0x571fd57004366c423dfd4b51196743b5/src/Console.bend as Console
import mylsm-lsm-store@0.4.0.0/src/CrashPoint.bend as CrashPoint
import 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.bend as CrashPoint
import mylsm-lsm-store@0.4.0.0/src/CrashPointPolicy.bend as CrashPointPolicy
import 0x571fd57004366c423dfd4b51196743b5/src/CrashPointPolicy.bend as CrashPointPolicy
import mylsm-lsm-store@0.4.0.0/src/Db.bend as Db
import 0x571fd57004366c423dfd4b51196743b5/src/Db.bend as Db
import mylsm-lsm-store@0.4.0.0/src/DbIo.bend as DbIo
import 0x571fd57004366c423dfd4b51196743b5/src/DbIo.bend as DbIo
import mylsm-lsm-store@0.4.0.0/src/Flush.bend as Flush
import 0x571fd57004366c423dfd4b51196743b5/src/Flush.bend as Flush
import mylsm-lsm-store@0.4.0.0/src/FlushPolicy.bend as FlushPolicy
import 0x571fd57004366c423dfd4b51196743b5/src/FlushPolicy.bend as FlushPolicy
import mylsm-lsm-store@0.4.0.0/src/Fs.bend as Fs
import 0x571fd57004366c423dfd4b51196743b5/src/Fs.bend as Fs
import mylsm-lsm-store@0.4.0.0/src/Keys.bend as Keys
import 0x571fd57004366c423dfd4b51196743b5/src/Keys.bend as Keys
import mylsm-lsm-store@0.4.0.0/src/Manifest.bend as Manifest
import 0x571fd57004366c423dfd4b51196743b5/src/Manifest.bend as Manifest
import mylsm-lsm-store@0.4.0.0/src/MemTable.bend as MemTable
import 0x571fd57004366c423dfd4b51196743b5/src/MemTable.bend as MemTable
import mylsm-lsm-store@0.4.0.0/src/MergeIter.bend as MergeIter
import 0x571fd57004366c423dfd4b51196743b5/src/MergeIter.bend as MergeIter
import mylsm-lsm-store@0.4.0.0/src/Recover.bend as Recover
import 0x571fd57004366c423dfd4b51196743b5/src/Recover.bend as Recover
import mylsm-lsm-store@0.4.0.0/src/RecoverPure.bend as RecoverPure
import 0x571fd57004366c423dfd4b51196743b5/src/RecoverPure.bend as RecoverPure
import mylsm-lsm-store@0.4.0.0/src/SortedRun.bend as SortedRun
import 0x571fd57004366c423dfd4b51196743b5/src/SortedRun.bend as SortedRun
import mylsm-lsm-store@0.4.0.0/src/SstFile.bend as SstFile
import 0x571fd57004366c423dfd4b51196743b5/src/SstFile.bend as SstFile
import mylsm-lsm-store@0.4.0.0/src/SstStreamIo.bend as SstStreamIo
import 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.bend as SstStreamIo
import mylsm-lsm-store@0.4.0.0/src/Sstable.bend as Sstable
import 0x571fd57004366c423dfd4b51196743b5/src/Sstable.bend as Sstable
import mylsm-lsm-store@0.4.0.0/src/StorageBytes.bend as StorageBytes
import 0x571fd57004366c423dfd4b51196743b5/src/StorageBytes.bend as StorageBytes
import mylsm-lsm-store@0.4.0.0/src/Wal.bend as Wal
import 0x571fd57004366c423dfd4b51196743b5/src/Wal.bend as Wal
import mylsm-lsm-store@0.4.0.0/src/hub_sha/core.bend as Core
import 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/core.bend as Core
import mylsm-lsm-store@0.4.0.0/src/hub_sha/sha256.bend as Sha256
import 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/sha256.bend as Sha256
import mylsm-lsm-store@0.4.0.0/src/hub_sha/state.bend as State
import 0x571fd57004366c423dfd4b51196743b5/src/hub_sha/state.bend as State

Modules

mylsm.bend 36 declarations
src/BitTree.bend 36 declarations
src/Compact.bend 50 declarations
src/CompactIo.bend 7 declarations
src/Console.bend 2 declarations
src/CrashPoint.bend 3 declarations
src/CrashPointPolicy.bend 2 declarations
src/Db.bend 48 declarations
src/DbIo.bend 14 declarations
src/Flush.bend 30 declarations
src/FlushPolicy.bend 1 declarations
src/Fs.bend 19 declarations
src/Keys.bend 24 declarations
src/Manifest.bend 96 declarations
src/MemTable.bend 24 declarations
src/MergeIter.bend 6 declarations
src/Recover.bend 68 declarations
src/RecoverPure.bend 23 declarations
src/SortedRun.bend 52 declarations
src/SstFile.bend 191 declarations
src/SstStreamIo.bend 51 declarations
src/Sstable.bend 81 declarations
src/StorageBytes.bend 31 declarations
src/Wal.bend 65 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	130 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`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.rename`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.remove`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.exists`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.loop`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.start`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.loop`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size.checked`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read_table`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish.synced`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.step`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.encoder`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write_table`, `0x571fd57004366c423dfd4b51196743b5/src/Console.read_line`, `0x571fd57004366c423dfd4b51196743b5/src/Console.get_env`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_tail`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.synced`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.written`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header_if_empty`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.existing`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.present`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_initialize`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_encoded`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_append`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_put`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write_staged`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_del`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_tail`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_file`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.encoded`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.loop`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.run`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.valid`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.mfst_opened`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.load_mfst`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.dir_tail`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.ensure_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goB`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_drift`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goA`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pre`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_frozen`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pick`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.remove_list`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_goB`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.drift_go`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_goA`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_pre`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_trig`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.exact.loop`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.load_tables`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.load_levels`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.exact.start`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.truncate`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.decode`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.body.bound`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.body`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.bound`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.length.checked`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.length.value`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.length`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.remaining`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.end`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.header.decoded`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.header`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.open.present`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal_open`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_one`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_get`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_cnt`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.wal_part`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.open_levels_checked`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.open_levels`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.open_names_go`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_root_go`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_root_cnt`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_root`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.open_db`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.flush_dec`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.flush_gate`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.drain_once`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.drain_pick`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.drain_go`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.maintain`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.maintain_unwrap`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.write`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.put`, `0x571fd57004366c423dfd4b51196743b5/src/Recover.del`, `open_recovering` output SOME PROOFS FAIL Error: 130 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 - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync - 0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate - 0x571fd57004366c423dfd4b51196743b5/src/Fs.rename - 0x571fd57004366c423dfd4b51196743b5/src/Fs.remove - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at - 0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir - 0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod - 0x571fd57004366c423dfd4b51196743b5/src/Fs.exists - 0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.loop - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.start - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.loop - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size.checked - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read_table - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish.synced - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.step - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.encoder - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write_table - 0x571fd57004366c423dfd4b51196743b5/src/Console.read_line - 0x571fd57004366c423dfd4b51196743b5/src/Console.get_env - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_tail - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.synced - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.written - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header_if_empty - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.existing - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.present - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_initialize - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_encoded - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_append - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_put - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write_staged - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_del - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_tail - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_file - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.bytes - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.encoded - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.loop - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.run - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.valid - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size - 0x571fd57004366c423dfd4b51196743b5/src/Flush.mfst_opened - 0x571fd57004366c423dfd4b51196743b5/src/Flush.load_mfst - 0x571fd57004366c423dfd4b51196743b5/src/Flush.dir_tail - 0x571fd57004366c423dfd4b51196743b5/src/Flush.ensure_dir - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goB - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_drift - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goA - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pre - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_frozen - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pick - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.remove_list - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_goB - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.drift_go - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_goA - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_pre - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_trig - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact - 0x571fd57004366c423dfd4b51196743b5/src/Recover.exact.loop - 0x571fd57004366c423dfd4b51196743b5/src/Recover.load_tables - 0x571fd57004366c423dfd4b51196743b5/src/Recover.load_levels - 0x571fd57004366c423dfd4b51196743b5/src/Recover.exact.start - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.truncate - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.decode - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.body.bound - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.body - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.bound - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.length.checked - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.length.value - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.length - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.remaining - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames.end - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.frames - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.header.decoded - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.header - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal.open.present - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal_open - 0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_one - 0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_get - 0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_cnt - 0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_dir - 0x571fd57004366c423dfd4b51196743b5/src/Recover.wal_part - 0x571fd57004366c423dfd4b51196743b5/src/Recover.open_levels_checked - 0x571fd57004366c423dfd4b51196743b5/src/Recover.open_levels - 0x571fd57004366c423dfd4b51196743b5/src/Recover.open_names_go - 0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_root_go - 0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_root_cnt - 0x571fd57004366c423dfd4b51196743b5/src/Recover.sweep_root - 0x571fd57004366c423dfd4b51196743b5/src/Recover.open_db - 0x571fd57004366c423dfd4b51196743b5/src/Recover.flush_dec - 0x571fd57004366c423dfd4b51196743b5/src/Recover.flush_gate - 0x571fd57004366c423dfd4b51196743b5/src/Recover.drain_once - 0x571fd57004366c423dfd4b51196743b5/src/Recover.drain_pick - 0x571fd57004366c423dfd4b51196743b5/src/Recover.drain_go - 0x571fd57004366c423dfd4b51196743b5/src/Recover.maintain - 0x571fd57004366c423dfd4b51196743b5/src/Recover.maintain_unwrap - 0x571fd57004366c423dfd4b51196743b5/src/Recover.write - 0x571fd57004366c423dfd4b51196743b5/src/Recover.put - 0x571fd57004366c423dfd4b51196743b5/src/Recover.del - open_recovering	3.1 s
src/BitTree.bend	checks	ALL PROOFS CHECK	0.6 s
src/Compact.bend	checks	ALL PROOFS CHECK	2.2 s
src/CompactIo.bend	relies on unsafe/foreign	88 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`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.rename`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.remove`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.exists`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.loop`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.start`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.loop`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size.checked`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read_table`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish.synced`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.step`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.encoder`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write_table`, `0x571fd57004366c423dfd4b51196743b5/src/Console.read_line`, `0x571fd57004366c423dfd4b51196743b5/src/Console.get_env`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_tail`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.synced`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.written`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header_if_empty`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.existing`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.present`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_initialize`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_encoded`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_append`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_put`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write_staged`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_del`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_tail`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_file`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.encoded`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.loop`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.run`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.valid`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.mfst_opened`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.load_mfst`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.dir_tail`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.ensure_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goB`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_drift`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goA`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pre`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_frozen`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pick`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush`, `remove_list`, `compact_goB`, `drift_go`, `compact_goA`, `compact_pre`, `compact_trig`, `compact` output SOME PROOFS FAIL Error: 88 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 - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync - 0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate - 0x571fd57004366c423dfd4b51196743b5/src/Fs.rename - 0x571fd57004366c423dfd4b51196743b5/src/Fs.remove - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at - 0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir - 0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod - 0x571fd57004366c423dfd4b51196743b5/src/Fs.exists - 0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.loop - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.start - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.loop - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size.checked - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read_table - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish.synced - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.step - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.encoder - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write_table - 0x571fd57004366c423dfd4b51196743b5/src/Console.read_line - 0x571fd57004366c423dfd4b51196743b5/src/Console.get_env - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_tail - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.synced - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.written - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header_if_empty - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.existing - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.present - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_initialize - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_encoded - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_append - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_put - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write_staged - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_del - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_tail - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_file - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.bytes - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.encoded - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.loop - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.run - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.valid - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size - 0x571fd57004366c423dfd4b51196743b5/src/Flush.mfst_opened - 0x571fd57004366c423dfd4b51196743b5/src/Flush.load_mfst - 0x571fd57004366c423dfd4b51196743b5/src/Flush.dir_tail - 0x571fd57004366c423dfd4b51196743b5/src/Flush.ensure_dir - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goB - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_drift - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goA - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pre - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_frozen - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pick - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush - remove_list - compact_goB - drift_go - compact_goA - compact_pre - compact_trig - compact	3.1 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: `0x571fd57004366c423dfd4b51196743b5/src/Console.read_line`, `0x571fd57004366c423dfd4b51196743b5/src/Console.get_env`, `stop`, `hit_decision`, `hit` output SOME PROOFS FAIL Error: 5 defs rely on unsafe or foreign code: - 0x571fd57004366c423dfd4b51196743b5/src/Console.read_line - 0x571fd57004366c423dfd4b51196743b5/src/Console.get_env - stop - hit_decision - hit	0.6 s
src/CrashPointPolicy.bend	checks	ALL PROOFS CHECK	0.6 s
src/Db.bend	checks	ALL PROOFS CHECK	2.4 s
src/DbIo.bend	relies on unsafe/foreign	50 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`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.rename`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.remove`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.exists`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Console.read_line`, `0x571fd57004366c423dfd4b51196743b5/src/Console.get_env`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit`, `wal_tail`, `wal.initialize.synced`, `wal.initialize.written`, `wal.initialize.header`, `wal.initialize.header_if_empty`, `wal.initialize.existing`, `wal.initialize.present`, `wal_initialize`, `wal_encoded`, `wal_append`, `db_write`, `db_put`, `db_write_staged`, `db_del` output SOME PROOFS FAIL Error: 50 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 - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync - 0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate - 0x571fd57004366c423dfd4b51196743b5/src/Fs.rename - 0x571fd57004366c423dfd4b51196743b5/src/Fs.remove - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at - 0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir - 0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod - 0x571fd57004366c423dfd4b51196743b5/src/Fs.exists - 0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir - 0x571fd57004366c423dfd4b51196743b5/src/Console.read_line - 0x571fd57004366c423dfd4b51196743b5/src/Console.get_env - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit - wal_tail - wal.initialize.synced - wal.initialize.written - wal.initialize.header - wal.initialize.header_if_empty - wal.initialize.existing - wal.initialize.present - wal_initialize - wal_encoded - wal_append - db_write - db_put - db_write_staged - db_del	2.6 s
src/Flush.bend	relies on unsafe/foreign	81 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`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.rename`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.remove`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.exists`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.loop`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.start`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.loop`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size.checked`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read_table`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish.synced`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.step`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.encoder`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write_table`, `0x571fd57004366c423dfd4b51196743b5/src/Console.read_line`, `0x571fd57004366c423dfd4b51196743b5/src/Console.get_env`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_tail`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.synced`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.written`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header_if_empty`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.existing`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.present`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_initialize`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_encoded`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_append`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_put`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write_staged`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_del`, `write_tail`, `write_file`, `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`, `flush_drift`, `flush_goA`, `flush_pre`, `flush_frozen`, `flush_pick`, `flush` output SOME PROOFS FAIL Error: 81 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 - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync - 0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate - 0x571fd57004366c423dfd4b51196743b5/src/Fs.rename - 0x571fd57004366c423dfd4b51196743b5/src/Fs.remove - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at - 0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir - 0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod - 0x571fd57004366c423dfd4b51196743b5/src/Fs.exists - 0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.loop - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.start - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.loop - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size.checked - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read_table - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish.synced - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.step - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.encoder - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write_table - 0x571fd57004366c423dfd4b51196743b5/src/Console.read_line - 0x571fd57004366c423dfd4b51196743b5/src/Console.get_env - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_tail - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.synced - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.written - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header_if_empty - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.existing - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.present - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_initialize - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_encoded - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_append - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_put - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write_staged - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_del - write_tail - write_file - 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 - flush_drift - flush_goA - flush_pre - flush_frozen - flush_pick - flush	3.0 s
src/FlushPolicy.bend	checks	ALL PROOFS CHECK	0.6 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	0.9 s
src/Keys.bend	checks	ALL PROOFS CHECK	1.1 s
src/Manifest.bend	checks	ALL PROOFS CHECK	1.4 s
src/MemTable.bend	checks	ALL PROOFS CHECK	1.2 s
src/MergeIter.bend	checks	ALL PROOFS CHECK	1.3 s
src/Recover.bend	relies on unsafe/foreign	129 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`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.rename`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.remove`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.exists`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.loop`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.start`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.loop`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size.checked`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read_table`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish.synced`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.step`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.encoder`, `0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write_table`, `0x571fd57004366c423dfd4b51196743b5/src/Console.read_line`, `0x571fd57004366c423dfd4b51196743b5/src/Console.get_env`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision`, `0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_tail`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.synced`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.written`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header_if_empty`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.existing`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.present`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_initialize`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_encoded`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_append`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_put`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write_staged`, `0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_del`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_tail`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_file`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.encoded`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.loop`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.run`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.valid`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.mfst_opened`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.load_mfst`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.dir_tail`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.ensure_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goB`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_drift`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goA`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pre`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_frozen`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pick`, `0x571fd57004366c423dfd4b51196743b5/src/Flush.flush`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.remove_list`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_goB`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.drift_go`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_goA`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_pre`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_trig`, `0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact`, `exact.loop`, `load_tables`, `load_levels`, `exact.start`, `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`, `wal.open.present`, `wal_open`, `sweep_one`, `sweep_get`, `sweep_cnt`, `sweep_dir`, `wal_part`, `open_levels_checked`, `open_levels`, `open_names_go`, `sweep_root_go`, `sweep_root_cnt`, `sweep_root`, `open_db`, `flush_dec`, `flush_gate`, `drain_once`, `drain_pick`, `drain_go`, `maintain`, `maintain_unwrap`, `write`, `put`, `del` output SOME PROOFS FAIL Error: 129 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 - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync - 0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate - 0x571fd57004366c423dfd4b51196743b5/src/Fs.rename - 0x571fd57004366c423dfd4b51196743b5/src/Fs.remove - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at - 0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir - 0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod - 0x571fd57004366c423dfd4b51196743b5/src/Fs.exists - 0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.loop - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.exact.start - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.loop - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size.checked - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read.table.size - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.read_table - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish.synced - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.finish - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.step - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write.encoder - 0x571fd57004366c423dfd4b51196743b5/src/SstStreamIo.write_table - 0x571fd57004366c423dfd4b51196743b5/src/Console.read_line - 0x571fd57004366c423dfd4b51196743b5/src/Console.get_env - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.stop - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit_decision - 0x571fd57004366c423dfd4b51196743b5/src/CrashPoint.hit - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_tail - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.synced - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.written - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.header_if_empty - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.existing - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal.initialize.present - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_initialize - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_encoded - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.wal_append - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_put - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_write_staged - 0x571fd57004366c423dfd4b51196743b5/src/DbIo.db_del - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_tail - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_file - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.bytes - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest.encoded - 0x571fd57004366c423dfd4b51196743b5/src/Flush.write_manifest - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.loop - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.run - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size.valid - 0x571fd57004366c423dfd4b51196743b5/src/Flush.manifest.read.size - 0x571fd57004366c423dfd4b51196743b5/src/Flush.mfst_opened - 0x571fd57004366c423dfd4b51196743b5/src/Flush.load_mfst - 0x571fd57004366c423dfd4b51196743b5/src/Flush.dir_tail - 0x571fd57004366c423dfd4b51196743b5/src/Flush.ensure_dir - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goB - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_drift - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_goA - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pre - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_frozen - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush_pick - 0x571fd57004366c423dfd4b51196743b5/src/Flush.flush - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.remove_list - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_goB - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.drift_go - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_goA - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_pre - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact_trig - 0x571fd57004366c423dfd4b51196743b5/src/CompactIo.compact - exact.loop - load_tables - load_levels - exact.start - 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 - wal.open.present - wal_open - sweep_one - sweep_get - sweep_cnt - sweep_dir - wal_part - open_levels_checked - open_levels - open_names_go - sweep_root_go - sweep_root_cnt - sweep_root - open_db - flush_dec - flush_gate - drain_once - drain_pick - drain_go - maintain - maintain_unwrap - write - put - del	2.8 s
src/RecoverPure.bend	checks	ALL PROOFS CHECK	1.9 s
src/SortedRun.bend	checks	ALL PROOFS CHECK	1.0 s
src/SstFile.bend	checks	ALL PROOFS CHECK	2.2 s
src/SstStreamIo.bend	relies on unsafe/foreign	42 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`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.rename`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.remove`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.exists`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go`, `0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir`, `exact.loop`, `exact.start`, `read.loop`, `read.table.size.checked`, `read.table.size`, `read_table`, `write.finish.synced`, `write.finish`, `write.step`, `write.encoder`, `write_table` output SOME PROOFS FAIL Error: 42 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 - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_words - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.write_bytes - 0x571fd57004366c423dfd4b51196743b5/src/Fs.fsync - 0x571fd57004366c423dfd4b51196743b5/src/Fs.truncate - 0x571fd57004366c423dfd4b51196743b5/src/Fs.rename - 0x571fd57004366c423dfd4b51196743b5/src/Fs.remove - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_count - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir_at - 0x571fd57004366c423dfd4b51196743b5/src/Fs.make_dir - 0x571fd57004366c423dfd4b51196743b5/src/Fs.chmod - 0x571fd57004366c423dfd4b51196743b5/src/Fs.exists - 0x571fd57004366c423dfd4b51196743b5/src/Fs.file_size - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_go - 0x571fd57004366c423dfd4b51196743b5/src/Fs.read_dir - exact.loop - exact.start - read.loop - read.table.size.checked - read.table.size - read_table - write.finish.synced - write.finish - write.step - write.encoder - write_table	2.1 s
src/Sstable.bend	checks	ALL PROOFS CHECK	1.4 s
src/StorageBytes.bend	checks	ALL PROOFS CHECK	0.7 s
src/Wal.bend	checks	ALL PROOFS CHECK	2.3 s
src/hub_sha/core.bend	checks	ALL PROOFS CHECK	1.2 s
src/hub_sha/sha256.bend	checks	ALL PROOFS CHECK	1.4 s
src/hub_sha/state.bend	checks	ALL PROOFS CHECK	0.5 s