59def sha256RoundState =
60 (lambda unrestricted roundConstant : (family ModelWord32) .
61 (lambda unrestricted scheduleWord : (family ModelWord32) .
62 (lambda unrestricted state : (family SHA256State) .
63 (eliminate
64 SHA256State
65 (lambda unrestricted current : (family SHA256State) . (family SHA256State))
66 state
67 (branch
68 SHA256StateValue
69 a
70 b
71 c
72 d
73 e
74 f
75 g
76 h
77 .
78 (app
79 (lambda unrestricted sigma1 : (family ModelWord32) .
80 (app
81 (lambda unrestricted choose : (family ModelWord32) .
82 (app
83 (lambda unrestricted temp1 : (family ModelWord32) .
84 (app
85 (lambda unrestricted sigma0 : (family ModelWord32) .
86 (app
87 (lambda unrestricted majority : (family ModelWord32) .
88 (app
89 (lambda unrestricted temp2 : (family ModelWord32) .
90 (constructor
91 SHA256State
92 SHA256StateValue
93 (modelWord32Add temp1 temp2)
94 a
95 b
96 c
97 (modelWord32Add d temp1)
98 e
99 f
100 g))
101 (modelWord32Add sigma0 majority)))
102 (modelWord32Majority a b c)))
103 (sha256BigSigma0 a)))
104 (modelWord32AddFive h sigma1 choose roundConstant scheduleWord)))
105 (modelWord32Choose e f g)))
106 (sha256BigSigma1 e)))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.