如何修改Ironclad的Lisp版SHA256以生成SAT实例/布尔表达式？

核心逻辑很直接：把SHA256中所有数值位运算替换成布尔表达式构造逻辑——原来计算32位整数的地方，改成用32个布尔符号/表达式的列表来表示每个“字”，每个算术操作（与、或、异或、加法、移位）都对应生成对应的布尔表达式，而不是计算最终数值。

步骤1：用S表达式表示布尔运算 #

别用字符串拼接，Lisp的S表达式天生适合表示布尔逻辑，比如(and a b)、(xor c d)、(not e)，后续转SAT实例（比如CNF）也方便。先写几个辅助函数：

;; 构造与运算
(defun bool-and (&rest args)
  (cond ((null args) t)
        ((= (length args) 1) (first args))
        (t (cons 'and args))))

;; 构造或运算
(defun bool-or (&rest args)
  (cond ((null args) nil)
        ((= (length args) 1) (first args))
        (t (cons 'or args))))

;; 构造异或运算（支持多操作数）
(defun bool-xor (&rest args)
  (case (length args)
    (0 nil)
    (1 (first args))
    (2 (list 'xor (first args) (second args)))
    (t (reduce #'(lambda (a b) (list 'xor a b)) args))))

;; 构造非运算
(defun bool-not (arg)
  (list 'not arg))

;; 32位字循环左移n位：把布尔列表的前n位移到末尾
(defun bool-rol (bit-list n)
  (let ((split (- 32 n)))
    (append (subseq bit-list split) (subseq bit-list 0 split))))

步骤2：替换数值变量为布尔符号集合 #

Ironclad里SHA256处理的是32位整数，现在我们用32个布尔符号的列表表示每个字。比如消息的每个bit对应一个唯一符号：

;; 生成消息块中某个bit的唯一符号
(defun msg-bit-sym (block-idx word-idx bit-idx)
  (intern (format nil "MSG-~A-~A-~A" block-idx word-idx bit-idx)))

;; 把一个消息块（16个32位整数）转换成布尔符号列表的集合
(defun msg-block-to-bools (block block-idx)
  (loop for word-idx from 0 to 15
        for word across block
        collect (loop for bit-idx from 0 to 31
                      collect (msg-bit-sym block-idx word-idx bit-idx))))

初始哈希值的处理：如果是固定初始值（比如SHA256的H0-H7），可以直接把每个bit转换成t（1）或nil（0）；如果要把初始哈希也作为变量，就生成对应的布尔符号。

步骤3：重写SHA256核心运算 #

把Ironclad里的位运算函数，全部改成对布尔列表的操作。比如SHA256的Σ0、Ch这些核心函数：

;; 按位与两个32位布尔列表
(defun bool-word-and (w1 w2)
  (mapcar #'bool-and w1 w2))

;; 按位或两个32位布尔列表
(defun bool-word-or (w1 w2)
  (mapcar #'bool-or w1 w2))

;; 按位异或两个32位布尔列表
(defun bool-word-xor (w1 w2)
  (mapcar #'bool-xor w1 w2))

;; SHA256的Σ0运算：(ror x 2) xor (ror x 13) xor (ror x 22)
;; 右移n位等价于左移(32-n)位
(defun bool-sigma0 (word)
  (let ((ror2 (bool-rol word 30)) ; 32-2=30
        (ror13 (bool-rol word 19)) ;32-13=19
        (ror22 (bool-rol word 10))) ;32-22=10
    (bool-word-xor ror2 (bool-word-xor ror13 ror22))))

;; SHA256的Ch运算：(x ∧ y) ⊕ (¬x ∧ z)
(defun bool-ch (x y z)
  (bool-word-xor (bool-word-and x y)
                 (bool-word-and (mapcar #'bool-not x) z)))

步骤4：改造压缩函数 #

Ironclad的sha256-compress-block是核心，原来更新数值哈希，现在改成构造每个哈希bit的布尔表达式。这里最复杂的是模2^32加法——SHA256里的加法不是异或，是带进位的整数加法，需要实现全加器的布尔逻辑：

;; 单个bit的全加器：输入a、b、进位in，返回(sum, carry-out)的布尔表达式
(defun full-adder (a b cin)
  (let ((sum (bool-xor a (bool-xor b cin)))
        (cout (bool-or (bool-and a b) (bool-and cin (bool-xor a b)))))
    (list sum cout)))

;; 两个32位布尔列表的模2^32加法，返回结果布尔列表
(defun bool-word-add (w1 w2)
  (let ((carry nil))
    (loop for a in (reverse w1)
          for b in (reverse w2)
          collect (multiple-value-bind (sum new-carry)
                      (full-adder a b carry)
                    (setf carry new-carry)
                    sum)
          into result
          finally (return (reverse result)))))

然后基于这个加法，改造压缩函数的迭代逻辑：

;; 改造后的压缩函数：输入哈希状态（8个32位布尔列表）和消息块布尔列表，返回新的哈希布尔列表
(defun bool-sha256-compress (hash-state msg-bools)
  ;; 扩展消息块到64个32位布尔列表（和原SHA256逻辑一致）
  (let ((w (append msg-bools
                   (loop for i from 16 to 63
                         collect (let ((s0 (bool-sigma0 (nth (- i 15) w)))
                                       (s1 (bool-sigma1 (nth (- i 2) w))) ; 需自行实现bool-sigma1
                                       (w16 (nth (- i 16) w))
                                       (w7 (nth (- i 7) w)))
                                   (bool-word-add w16 (bool-word-add s0 (bool-word-add w7 s1))))))))
    ;; 初始化临时变量a-h为当前哈希状态
    (let ((a (nth 0 hash-state)) (b (nth 1 hash-state))
          (c (nth 2 hash-state)) (d (nth 3 hash-state))
          (e (nth 4 hash-state)) (f (nth 5 hash-state))
          (g (nth 6 hash-state)) (h (nth 7 hash-state)))
      ;; 64轮迭代
      (loop for i from 0 to 63
            for wi in w
            for k = (nth i *sha256-constants*) ; 常数转布尔列表，比如#x428a2f98→32个t/nil
            do (let ((t1 (bool-word-add h (bool-word-add (bool-sigma1 e)
                                                         (bool-word-add (bool-ch e f g)
                                                                       (bool-word-add k wi)))))
                     (t2 (bool-word-add (bool-sigma0 a) (bool-maj a b c)))) ; 需实现bool-maj
                 (setf h g g f f e
                       d (bool-word-add d t1)
                       e d c b b a
                       a (bool-word-add t1 t2)))
            finally (return (list (bool-word-add a (nth 0 hash-state))
                                  (bool-word-add b (nth 1 hash-state))
                                  (bool-word-add c (nth 2 hash-state))
                                  (bool-word-add d (nth 3 hash-state))
                                  (bool-word-add e (nth 4 hash-state))
                                  (bool-word-add f (nth 5 hash-state))
                                  (bool-word-add g (nth 6 hash-state))
                                  (bool-word-add h (nth 7 hash-state)))))))

关键注意点 #

1. 表达式简化：直接生成的布尔表达式会极其庞大，必须在构造过程中做简化，比如(and t x)→x，(xor x x)→nil，否则后续转SAT实例会完全无法处理。可以给辅助函数加简化逻辑。
2. 符号唯一性：确保每个输入bit对应唯一的符号，避免命名冲突，用intern生成符号是简单可靠的方法。
3. 常数处理：SHA256的轮常数K0-K63要转换成对应的布尔列表，直接用logbitp遍历每个bit即可。

新手进阶建议 #

• 先从简化版哈希函数练手，比如只保留几轮迭代，熟悉数值转布尔表达式的逻辑。
• 仔细读Ironclad的SHA256源码，逐行对比替换，重点攻克加法部分的布尔实现。
• 学习S表达式的遍历与转换，后续可以把生成的布尔表达式转换成CNF格式（SAT求解器的标准输入）。

内容的提问来源于stack exchange，提问作者gautam