WongSSH

介绍了更接近形式化证明顶层的 Program Annotations 中的 Function Specifications / Loop Invariants / assertion / assume statements 的概念和应用，特别是这些内容在形式化证明语言，比如 dafny 和 solidity SMTChecker 内的应用。在阅读完成目前内容后，读者也许可以使用 dafny 构造一些证明

@yanbo2004 系统级感觉是一个优势，什么软件都可以用，体感准确度还可以，主要可以把视频和字幕分离，我有看字幕的习惯，分开后就会好一些

@wong_ssh 准确率一般 有时候可能不如浏览器插件lol

原来 MacOS 还有实时字幕的功能，这下可以上面屏幕看视频，下面屏幕显示字幕，然后听不懂的话就低头看一下下面屏幕内的字幕。这个字幕功能支持好多种英语啊，不知道印度英语是否对印度发音更友好。

@QC76088918 理论上会有，我看看能不能写一个，AA VE v4 内部有很多有趣的形式化证明案例，基本都是为了避免模糊性，比如这个案例是证明 supply 和 remove 的互逆，这个不变量被打破就会导致经典的 Inflation Attacks。 单元测试或者 fuzz 永远不是证明，但是按照数学逻辑推理一定会得到正确结论。

@wong_ssh 会有形式化证明一些合约代码的案例吗？ 期待，之前有看过 weth 的形式化证明，不过我对形式化验证不太理解，没看懂形式化证明在干什么，形式化验证给我一种感觉像是更高级的单元测试

最近一直读形式化证明的书，之前学的很多东西过于理论，但最近刚刚在书中学会了对真正的代码的证明，所以刚好以此为教学案例介绍形式化证明。当然，我也会给出部分理论基础和名词解释，目前写的这一节就是介绍这部分内容。博客介绍的方法是半自动的，命题证明丢给了 z3 避免引入太多逻辑学内容。

今天晚上补充了 theory 的背景知识，写得很枯燥，但是读完就可以知道为什么 z3 的文档内有一个被称为 theory 的章节。 限于篇幅，没有介绍 theory of equality 这个无聊但重要的 theory，也没有介绍实数的 theory，这些内容可以去读书了解。

@ByteRamble @woaidaxiong123 @guil_lambert 你是指理论模型还是实际操作，我记得理论模型是不考虑 rebalance 的滑点问题的，这个研究的后续是去 panoptic 捡垃圾，在 panoptic 内借入低价 LP 同时卖出 LP，构建收益结构类似价差的期权组合。

@wong_ssh @woaidaxiong123 @guil_lambert 请教下，验证时rebalance是自己实现的，还是用现成的工具

rebalance 状态下 LP 的价值如何变化？假设我们可以不断在 LP 突破区间后立即进行 rebalance 操作，假设 rebalance 操作无滑点和手续费，我们可以获得如下 LP 价值曲线。同时假设 LP 内的包含非稳定币和稳定币两部分。 下图中的红色线条为非稳定币的币价，而蓝色线条为 LP 价格。

这篇文章的前言应该是我写的最长的文章前言。对我来说，LLM 时代下的形式化证明以及数学的未来比 OpenClaw 更有趣。

文章链接 @wongssh/BJKd99hKWx" target="_blank" rel="nofollow noopener">hackmd.io/@wongssh/BJKd9…

博客地址: @wongssh/uniswap-v3-whitepaper" target="_blank" rel="nofollow noopener">hackmd.io/@wongssh/unisw…

终于写完了 Uniswap v3 的文章，虽然一直控制篇幅，但是字数还是超过了 1 万字，基本涵盖了所有核心内容，除了 Oracle 部分，感觉可以找一个时间写一篇博客专题讨论 Uniswap v2 和 v3 内的 Oracle 实现和应用。

HackMd 链接: @wongssh/uniswap-v3-whitepaper" target="_blank" rel="nofollow noopener">hackmd.io/@wongssh/unisw…

继续为系列课程写讲义，相比于之前写的 Uniswap v3 的文章，这篇文章更加简单，可读性更高，主要按照白皮书的顺序介绍代码(其实是按照核心逻辑)，打散代码介绍顺序并简化了数学分析，很多数学公式直接给出而不是推导。 当然，目前还没写完，如果有任何问题，可以给文档评论或者直接在此推文下留言

@0xkaka1379 @z0r0zzz 这个攻击方法还挺著名的，Uniswap v4 router 内全是内联汇编解析 calldata，但是都做了校验 github.com/Uniswap/v4-per…

昨天 @z0r0zzz 开发的uniswapv4 优化路由合约遭到了攻击，一用户损失了42k USDC。 在本次事件分析中，也新接触到了一种攻击面——“ABI偏移篡改”攻击。 在claude的辅助下，写了篇文章进行记录。 @0xkaka1379/ABIOffsetManipulation" target="_blank" rel="nofollow noopener">hackmd.io/@0xkaka1379/AB…

在这里也把冒泡排序的形式化的第一步补充一下，这里 L1 和 L2 代表 loop invariants，也可以理解为循环的中间状态，由于内部存在多个分支，所以最后这段代码会被拆成 6 个 path，每一个 path 都需要利用证明，上图中给出的方法为 weakest precondition，是一种倒推方法

形式化证明很好玩，虽然看起来就是天书。这是冒泡排序算法的一个 if 路径的形式化证明，F 是给定的输入限制，而 G 是给定的输出要求，assume 是编写的代码中的额外限制，partitioned(a, ℓ1, u1, ℓ2, u2) 等价为 ∀i, j. ℓ1 ≤i ≤u1 < ℓ2 ≤j ≤u2 → a[i] ≤a[j]

通俗来说，这些理论会允许 SMT Solver 使用一些特殊的规则(实际上就是公理)对逻辑命题进行推导，下图展示自然数(Presburger arithmetic) 的公理。当我们获得一个逻辑命题时，就可以套用 axioms 内的内容进行化简和求解

有了这个表格，大家也许就可以看到自己的求解器内不同的模式的含义，比如下图来自 Yices SMT Solver

哪些领域的逻辑问题是可判定的？以及判定算法的复杂度是多少？我使用的逻辑学教科书给出了以下表格。此处的 QFF 指的是无量词逻辑命题(与求解器内的 QF 前缀等价)，即不包含任意、存在的逻辑命题。 此处的 linear integers 不包含变量乘法即不允许 x * y = 42 这种命题，因为整数方程不一定有解。

@jeffishjeff 链接: @wongssh/uniswap-v2" target="_blank" rel="nofollow noopener">hackmd.io/@wongssh/unisw…

最近受邀和 @jeffishjeff 录制一个关于 Uniswap 的系列课程，趁此把 Uniswap 全系列的合约再过一篇。 我在此前一直没有完整读过 Uniswap v2，此次把 v2 完整读了一遍并且写了 1 万字的稿件。内容涉及的非常广泛，还包含大量外部链接指向拓展内容，对刚刚学会 solidity 语法的学习者也许是一份好材料