verified-ledger：使用 Lean 4 作为模糊测试预言机来验证 Rust 代码的实现逻辑
verified-ledger 展示如何利用 形式化验证（Formal Verification） 与 差异化模糊测试（Differential Fuzzing） 来确保关键系统（如账本系统）的正确定性与安全性。
项目核心理念：基于模型的合规性测试。其核心逻辑是：
- 形式化模型（Oracle） ：使用 Lean 4 （一种证明辅助语言）编写一个简单但经过严谨数学证明的账本模型，作为系统的“绝对正确标准”。
- 目标实现 ：使用 Rust 编写一个实际的账本实现。
- 差异化模糊测试 ：通过模糊测试工具同时运行 Rust 实现和 Lean 模型。如果两者的输出不一致，说明 Rust 代码中存在漏洞或逻辑错误。
技术栈：
- Lean 4 ：用于编写形式化规范、可执行模型以及相关的正确性证明。
- Rust ：用于编写高性能的业务逻辑实现。
- FFI (Foreign Function Interface) ：用于在 Rust 和 Lean 之间建立链接，使 Rust 能够调用 Lean 模型作为测试参考。
- LibAFL / Fuzzing Harness ：用于生成随机交易序列并比对执行结果。
该项目模拟了一个简单的账本系统，支持以下基本操作：
- Deposit（存款） ：增加指定账户的余额。
- Withdraw（取款） ：在余额充足时减少账户余额。
- Transfer（转账） ：从一个账户向另一个账户转移资金，包含充足余额检查。
项目结构与亮点：
- lean/ ：包含 Lean 4 模型文件（
Model.lean）和形式化证明（Proofs.lean）。证明涵盖了诸如“存款操作后余额必然增加”等数学特性。 - src/ ：包含 Rust 版本的账本实现。为了演示目的，这个 Rust 实现中特意引入了几个 Bug（例如：取款逻辑中的边界错误，或转账时未正确扣款），用来展示模糊测试是如何精准发现这些潜在缺陷的。
- CI/CD 集成 ：该架构设计用于集成到持续集成流水线中，通过不断演进的测试来监控代码迭代过程中的正确性。
这个项目并不是一个生产级的账本库，而是一个 教学和工程范例 ，适合以下人群参考：
- 希望在金融、区块链等高可靠性系统中引入形式化验证的开发者。
- 对 Lean 4 和 Rust 互操作性感兴趣的研究者。
- 寻找比传统单元测试更强大的“模型驱动测试”方案的架构师。
仓库：https://github.com/welltyped-systems/verified-ledger
文章《谁拥有内存？Part1：什么是对象？》
作者： Luca Lombardo
这是《Who Owns the Memory? 》系列文章的第一篇，深入探讨了 C、C++ 和 Rust 如何在底层管理内存。
内存的本质：只是字节（Bytes）
- 硬件视角：CPU 并不理解结构体或整数，它看到的只是一个平坦的字节数组。类型系统是人类在源代码中构建的抽象，旨在帮助编译器进行优化（如寄存器缓存、消除空检查等）。
- 虚拟地址空间：OS 通过 MMU 提供虚拟内存，实现进程隔离和硬件无关性。
- 内存对齐（Alignment）：为了硬件效率，特定类型必须存储在特定倍数的地址上。违反对齐会导致性能损失甚至硬件崩溃。
- 缓存行（Cache Lines）：现代 CPU 以 64 字节块读取数据。编译器通过在结构体中插入填充（Padding）来确保字段不会跨越缓存行边界，以提高访问效率。
从字节到“对象”：类型的解释。文章对比了三种语言如何将内存区域定义为“对象”：
- C 语言：有效类型规则（Effective Type Rules）。C 通过写入操作确立有效类型。严格别名规则（Strict Aliasing）允许编译器假设不同类型的指针不会指向同一内存，从而进行优化。
- C++：对象生命周期（Object Lifetime）。C++ 引入了构造和析构的概念。对象的生命周期始于构造完成，终于析构开始。即使内存字节还在，超出生命周期的访问也是未定义行为（UB）。
- Rust：有效性不变性（Validity Invariants）。Rust 的要求最严苛。每种类型都有严格的有效性要求（例如
bool只能是 0 或 1）。一旦产生无效位模式，立即触发 UB，即使你还没读取它。
存储期（Storage Duration）：内存分为四大类：
- 静态（Static）：程序全程存在（如全局变量）。
- 线程（Thread）：随线程生命周期。
- 自动/栈（Automatic/Stack）：随函数作用域，分配/释放是 O(1) 的，但内存是不初始化的。
- 分配/堆（Allocated/Heap）：显式控制。C 需要手动管理；C++ 倾向于 RAII（智能指针）；Rust 则强制所有权模型，确保内存被自动且确切地释放。
生命周期与借用检查（Rust 的核心）：
- C/C++ 的痛点：悬挂指针（Dangling pointers）在 C/C++ 中很容易产生，编译器通常不强制拦截。
- Rust 的解决方案：将生命周期（Lifetimes）视为控制流图（CFG）中的命名区域。借用检查器通过约束传播（Constraint Propagation）计算每个引用必须有效的最小区域。
- 非词法生命周期（NLL）：Rust 2018 引入，使引用的生命周期从其最后一次使用处结束，而非简单的作用域结束，增加了代码的灵活性。
未初始化内存：
- 在 C 中，读取未初始化变量得到的是“不确定值”；在 Rust 中，这被视为严重的 UB。
- Rust 提供了
MaybeUninit<T>作为处理未初始化内存的安全转义口，防止编译器在值准备好之前对其有效性做出错误假设。
别名（Aliasing）：优化之源
- 为什么编译器在意？ 如果两个指针可能指向同一内存（别名），编译器就不能把内存值缓存在寄存器里，也不能进行向量化（SIMD）优化。
- C 语言：使用
restrict关键字向编译器“保证”指针没有别名（如果撒谎则会导致 UB）。 - Rust：通过“共享不可变，可变不共享”（Shared XOR Mutable）原则在编译期强制保证。这让 Rust 默认就能获得类似甚至超过 C
restrict的优化效果，且具有安全性。
核心结论： 该文强调，虽然这三种语言在物理层面上操作的是同样的字节，但它们对**“对象何时存在”以及“谁被允许修改它”**的规则（抽象层）定义截然不同。Rust 的优势在于将这些规则从程序员的脑中移到了编译器的静态检查中。
阅读：https://lukefleed.xyz/posts/who-owns-the-memory-pt1/
DecentPaste：跨平台、点对点（P2P）剪贴板同步工具
DecentPaste 是一个隐私优先、极致轻量且高度实用的工具。它展示了如何利用 Rust 的安全性和性能，结合 libp2p 这种去中心化技术，解决日常生活中跨生态链的数据传输难题。对于厌倦了将数据上传到商业云端或受困于系统生态壁垒的用户来说，这是一个非常理想的替代方案。
核心动机：解决“给自己发消息”的痛点：
作者在 Reddit 帖中提到，他曾长期通过 Telegram 的“Notes to self”或发邮件来跨设备传输链接和文本。虽然 Apple 和三星有各自的生态同步功能，但在混合使用 Mac、Linux、Windows 和 Android 的场景下，这些原生方案统统失效。 因此，他开发了 DecentPaste，旨在提供一个不依赖云端、跨越所有主流系统的剪贴板同步方案。
技术亮点：
- Rust 后端 + Tauri v2：应用基于 Tauri 构建，这意味着它比 Electron 应用更轻量（约 15MB 内存占用，而非数百 MB）。
- libp2p 网络协议：使用
libp2p实现 P2P 通信，通过mDNS进行设备自动发现，利用gossipsub进行剪贴板广播。 - 端到端加密（E2E）：数据在本地网络传输前会经过加密。使用
X25519密钥交换和AES-256-GCM加密，密钥通过 ECDH 在本地生成，绝不上传。 - 数据安全：使用
IOTA Stronghold提供加密存储，结合Argon2id进行密钥派生，确保本地保存的剪贴板历史记录也是安全的。
主要功能：
- 跨平台同步：支持 Windows、macOS、Linux 和 Android。
- 即插即用：无需创建账户，无需连接云服务器，只要设备在同一 WiFi 下即可工作。
- 配对机制：通过简单的 4-6 位 PIN 码完成设备安全配对。
- 剪贴板历史：不仅同步当前内容，还兼任剪贴板历史管理器。
- 移动端集成：Android 端支持 Share Sheet，可以从任何应用分享内容到 DecentPaste。
现状与局限（处于 Alpha 阶段）：
- 仅限文本：目前仅支持文本同步，不支持图片或文件。
- 局域网限制：设备必须位于同一网络/子网（依赖 mDNS）。
- 移动端后台同步：为了省电，Android 端目前没有后台同步，需手动操作（或通过 Share Now）。
- iOS 暂缺：目前 iOS 端还在 App Store 审核/测试阶段（TestFlight），尚未正式发布。
仓库：https://github.com/decentpaste/decentpaste
--
From 日报小组 苦瓜小仔
社区学习交流平台订阅：
评论区
写评论还没有评论