Technology Comes First

本文将概述几篇云上形式化验证的论文，其中大部分源于 amazon.science 里的 Automated Reasoning 分类。 本文关注的重点方向包括： 可满足性模理论（Satisfiability Modulo Theories）的工程实践。 AWS IAM Policy（下面的表格会梳理本文对于常见术语的中文表达）。 AWS IAM Access Analyzer 的产品和背后用到的技术，特别是 AWS 的内部服务 Zelkova。 英语术语 中文术语 含义 Policy 策略 用于形式化表达一组 IAM 授权，是由 Statement 构成的一个数组 Statement 语句 构成策略数组的元素，包含 Effect, Action, Conditon, Resource 等维度 Effect 效果 Allow 和 Deny 二选一，表示本条 Statement 是授权语义和拒绝语义 Action 权限 表示本条 Statement 关联的授权或拒绝的权限点 Resource 资源 表示本条 Statement 关联的授权或拒绝的资源 ...

总体印象 2024 年底抽空在云南逛了三天，属于是特种兵式的旅游，总体感想如下： 我们在云南主动或被动地体验了各种交通方式，包括飞机、高铁、大巴、中巴、观光巴士、电动三轮车和共享单车等。最最厌恶的是各个景点门口扯着嗓子招揽客人的中巴车（黑车）司机。 云南的物价比杭州低很多，就连景区价都能够接受。不过热带水果没有想象中的那么便宜。 云南的咖啡店很多，特别是自有的小粒咖啡。花茶店和鲜花饼店也很多，古镇路上全是店员在邀请试吃。云南常见的连锁奶茶店是霸王茶姬、蜜雪冰城和当地的香巴拉，常见的便利店是美宜家。 昆明·着陆风波 我们坐的是周五傍晚 17:0517:0517:05 杭州直飞大理的航班，小延一会后顺利起飞，原计划在大理古城一直逛到深夜。临近大理准备下降时，机上传来广播：大理风太大无法着陆，飞机会在上空盘旋直至地面指挥台给降落信号。我俩对这条通知没放在心上，谁知十分钟后来了下一条通知：因天气原因无法着陆大理，机长决定备降昆明。机上的乘客立即炸开了锅，空姐在众人周围来回解释：当下备降昆明的事实已无可改变，落地后可能会在机上等一会观察大理天气情况，若无好转只能下机入住航司安排的酒店，等深夜 ...

总体印象 2024 年的中秋假期前往马尔代夫的莉莉岛玩了五天四晚，感受总结如下： 开放式管理，上岛后要签免责协议，沿海的平台没有护栏，游到深海也没人管。 莉莉岛上中国人很多，平均占比超过 50%。欧美日韩俄的游客都有。 马代除了本地语言外，和游客沟通的标准语言是英文。很多人会说几句常见的中文（如莉莉岛上服务员会说西瓜、谢谢等，购物时店家会说便宜、中国、冰箱贴等）。 水很蓝很清澈，人很少，浮潜能看到很多珊瑚和鱼。 莉莉岛的饮食马马虎虎，酒水饮料的品种很多。 关于小费，经过几次大手笔的 555 美元的失败尝试后，我们把进餐或搭车的小费稳定在 1∼21 \sim 21∼2 美元。 临行准备 马尔代夫印度洋上的群岛国家，首都马累，主要产业是旅游业和船运业。马代旅游模式主要包括以下两种： 居民岛：岛上选酒店，自行 DIY 交通、餐饮和活动，预算偏低。最有代表性的就是马富士岛（Maafushi）。 度假村：一岛一酒店的开发模式，商业化成熟，预算偏高。旅行社可代订五天四晚套餐，主流价格区间是人均 1w−2w1w-2w1w−2w 人民币。岛屿酒店的房型主要分为沙屋和水屋两种：沙屋坐落在岛的陆地上 ...

整除 Division 除法定理（division theorem）：若 a,b∈Z,b>0a,b \in \mathbb{Z}, b>0a,b∈Z,b>0，则存在唯一的整数对 (q,r)(q,r)(q,r) 满足 a=qb+r0≤r<b\begin{align} a=qb+r \quad 0\le r < b \end{align} a=qb+r0≤r<b​​ 华罗庚在《数论导引》里的方法很简洁： ⌊ab⌋≤ab<⌊ab⌋+1a,b∈Z,b>00≤a−⌊ab⌋⋅b<ba=⌊ab⌋⋅b+r0≤r<b\lfloor \frac{a}{b} \rfloor \le \frac{a}{b} < \lfloor \frac{a}{b} \rfloor+1 \quad a,b \in \mathbb{Z}, b>0\\ 0 \le a - \lfloor \frac{a}{b} \rfloor \cdot b <b \\ a=\lfloor \frac{a}{b} \rfloor \cdot b+r \quad 0 \ ...

五一去日本玩了五天，整体行程推迟两天算是错峰了。记录一些美好的回忆。 日本印象： 酒店的马桶都是智能马桶；路面清洁，无环卫工人，垃圾桶很难找。 国际化，外国游人多。英语是最大外语，很多资料也会有中文解释。大概有 70%70\%70% 的店员能够用英语词汇沟通，30%30\%30% 的店员能够用中文沟通。 轨道交通发达，地铁里很安静。夜间地铁中空期只有四小时左右。Google Map 加持精准的交通，就连公交车也是掐点的。地铁和公交的价格大概是国内的三倍，但总比打车划算很多。 便利店文化繁盛，主要是罗森、全家和 711。 便利店不卖药。药店一般是大而全的松本清、大国药妆、堂吉诃德之类的，深夜买药不方便。 外卖少。很多外卖员用自行车配送。 乡镇的建筑（如富士山河口湖）都是四四方方的统一风格，很像乐高。 攻略总结： 带少量现金即可。正规的连锁店一般都支持支付宝和微信，这中间除了便利店外大多都支持退税。小店可以用 visa 或现金搞定，没遇到过两者都不能支付的情况。 对于轨道交通，某个城市周边待得久可以买一/两日的周游券，否则 Apple 西瓜卡随用随刷。 热门 ip 的热门产品可以在 ...

周六张杰演唱会+周日迪士尼的计划，随着黄牛票出票失败而被迫变化。 上海 CityWalk 周六 11:1611:1611:16 抵达虹桥站，二号线坐到中山公园站，在长宁来福士和我徒弟张扬播会合。 我们从四楼一直逛到七楼（电影院）都没找到想吃的店，美团上翻出两个感兴趣的都在斜对面的龙之梦。路过米桃时，门口的松鼠桂鱼海报吸引了我，价格还行+环境雅致，就决定是江苏菜了！无锡全家福小笼包上得很快，分为鲜肉，黑松露，蟹粉三种口味，一口爆汁；蟹粉带着点腥味，看起来货真价实；后悔点牛肋排了，我们仨胃口小吃得够呛；招牌的松鼠桂鱼上得最慢（想必制作工艺很麻烦），鱼肉外面用面粉包裹炸一圈，味道不错。 我们自来福士出，沿着愚园路步行。天气很好，愚园路的人却并不多。上海的建筑总给我一种泛红的厚重气息。励颖开开心心地从一家网红店里买了个蓝莓蛋糕，很难想象一个中午吃撑的人能完整吃下它。 根据计划，我们得从江苏路进站坐二号线至人民广场，沿着步行街一直走到外滩。事实上我们坐过了一站，只能各自多交 333 块钱往回。南京路步行街比愚园路热闹太多，马路宽行人多，两侧是各色的招牌。路边有一家很大的 M 豆店，我心想 ...

因为业务场景的需要，我在华为云接触到一些密码学知识，并在部门里做过一次 PPT 分享。这类分享以科普性质为主，强调易于理解性、实用性和图文并茂性，而且在细微之处时有疏漏和模糊之处，颇有不求甚解之感。趁着春节假期的空闲，我决定再系统性地整理一遍，以严谨而简洁的风格重新组织文字。 总而言之，本篇密码学导论主要有以下几个特征： 概括性。用统一的风格，列举经典的密码学概念、定理和算法。 准确性。总体风格不拘小节，每个细节力求准确无误。 应用性。重点关注工程上的密码学应用，省略对过于理论或过于前沿的知识点。 持续性。工程浩大，想到哪里就写到哪里，持续修正和扩展。 有任何问题欢迎批评指正！ 近期规划：更新概述部分、证书链部分，补充图片。 远期规划：新增零知识证明和格密码。 概述 密码学（Cryptography）可分为古典密码学和现代密码学。 1949 年香农（C. E. Shannon）发表了题为《保密系统的通信理论》的经典论文标志着现代密码学的开始。 密码学的本质是消息在传递过程中保证如下性质：机密性（Confidentiality）、完整性（Integrity）、可用性（Availab ...

周六到周二（请假两天）去香港四天，主要就是三件事：买金，办卡和吃喝玩乐。 三句话总结 马路纵横交错，建筑排布很乱；路面很窄，行人之间摩肩接踵，几乎没有自行车和电动车。 和攻略上说的一样，充电宝和卫生间都很难找。 香港街上都有些什么建筑？ 银行、金店、711 和货币兑换，占据了路上 50%50\%50% 的建筑。 再加上药店、奢侈品店、饭店，占据了路上 80%80\%80% 的建筑。 周六 周六到周二（请假两天）去香港四天，主要有三件事：买金，办卡和吃喝玩乐。 直飞香港的机票太贵（班次少，单程不算机建燃油 700+700+700+），于是我来回都选择了深圳中转（班次很多，单程不算机建燃油在 200∼400200 \sim 400200∼400），再通过深圳福田中转前往香港西九龙（454545 分钟地铁+151515 分钟高铁）。香港真是寸土寸金，尖沙咀的酒店一晚上普遍都是一两千。咬牙订了家性价比还行的君怡酒店，三晚 2.2k2.2k2.2k。 在招行总共取了 300030003000 港币的现金，作为办卡激活和防身用。个人感觉八达通的实用性已经没那么高了，就没有办理。出发前提前购 ...

桌游，顾名思义是桌上游戏，发源于德国，内容涉及战争、贸易、文化、艺术、城市建设、历史等多个方面，大多使用纸质材料加上精美的模型辅助。桌游圈的 Wikipedia 是 BGG。 本文会记录我玩过的所有桌游（感谢金主爸爸何柱提供大部分桌游），并给予玩法简介和评价（缓更）。 打分 释义 S 我会主动邀请朋友玩，至今百玩不厌 A 我乐意把它推荐给朋友玩 B 我乐意接受朋友的邀请，但不会主动去玩 C 只有朋友强烈邀请，我才会去玩 D 即便朋友强烈邀请，我也一定不会玩 中文名 年份 (最佳)人数 BGG评分 BGG重度 本人 何柱 堕落 tsr 励颖 七大奇迹 2010 2,3,4,5,6,7 7.7 2.32 S A A ? A 重塑火星 2016 1,2,3,4,5 8.4 3.26 S A ? A 工业革命·伯明翰 2018 2,3,4 8.6 3.88 S S S ? B 葡萄酒庄园·精华版 2015 1,2,3,4,5,6 8.0 2.89 S A A ? A 灵迹岛 2017 1,2,3,4 8.3 4.06 S S ...

大语言模型（Large Language Model）在近年来呈井喷式发展。 自 2017 年特征提取器 Tranformer 发表以来，LLM 主要有三条发展方向： 发展方向 特征 简述 BERT Encoder Only 自编码，适合做理解任务 GPT Decode Only 自回归，适合做生成任务 T5 Encoder-Decoder 综合了上述两点的优势，参数暴涨但潜力大 图源: https://github.com/Mooler0410/LLMsPracticalGuide LLM News 2023.4 奶奶漏洞（Grandma Exploit）：网友发现在和大模型对话时，如果要求其扮演自己已经过世的祖母，就可以绕开模型的安全护栏机制，套取包括 Win11 序列号在内的敏感内容。 LLM Concept 思维链（chain of Thought）：要求模型在输出最终答案之前，显式输出中间逐步的推理步骤。CoT 是一种简单有效的 Prompt 技术，在复杂场景（如算术推理、常识推理、符号推理等）里效果很好。 涌现能力（emergent abili ...