Ligo is pinned to an old version of LLTZ, the following contract fails to compile and raises LLTZ errors, this has now been fixed in a recent LLTZ commit: ``` module Sha256 = struct type hashstate = nat * nat * nat * nat * nat * nat * nat * nat type block = nat * nat * nat * nat * nat * nat * nat * nat * nat * nat * nat * nat * nat * nat * nat * nat type storage = hashstate type ret = operation list * storage let max_uint32 = 4294967295n (* 0xFFFFFFFF *) let const_K : nat list = [ 1116352408; 1899447441; 3049323471; 3921009573; 961987163; 1508970993; 2453635748; 2870763221; 3624381080; 310598401; 607225278; 1426881987; 1925078388; 2162078206; 2614888103; 3248222580; 3835390401; 4022224774; 264347078; 604807628; 770255983; 1249150122; 1555081692; 1996064986; 2554220882; 2821834349; 2952996808; 3210313671; 3336571891; 3584528711; 113926993; 338241895; 666307205; 773529912; 1294757372; 1396182291; 1695183700; 1986661051; 2177026350; 2456956037; 2730485921; 2820302411; 3259730800; 3345764771; 3516065817; 3600352804; 4094571909; 275423344; 430227734; 506948616; 659060556; 883997877; 958139571; 1322822218; 1537002063; 1747873779; 1955562222; 2024104815; 2227730452; 2361852424; 2428436474; 2756734187; 3204031479; 3329325298; ] let state_init : hashstate = ( 1779033703, 3144134277, 1013904242, 2773480762, 1359893119, 2600822924, 528734635, 1541459225) let rot32 (n : nat) (s : nat) (sm32 : nat) : nat = let sr = n lsr s in let sl = n lsl sm32 in (sr lor sl) land max_uint32 let t1rot (n : nat) : nat = (rot32 n 6 26) lxor (rot32 n 11 21) lxor (rot32 n 25 7) let t2rot (n : nat) : nat = (rot32 n 2 30) lxor (rot32 n 13 19) lxor (rot32 n 22 10) let natnot (n : nat) : nat = n lxor max_uint32 let t1mix (z4 : nat) (z5 : nat) (z6 : nat) : nat = (z4 land z5) lxor ((natnot z4) land z6) let t2mix (z0 : nat) (z1 : nat) (z2 : nat) : nat = (z0 land z1) lxor (z0 land z2) lxor (z1 land z2) let rec select (i : int) (ns : nat list) : nat = match ns with | [] -> failwith "short list" | x :: xs -> if i = 0 then x else select (i-1) xs let rec push_back (elm : nat) (l : nat list) : nat list = match l with | [] -> [elm] | x :: xs -> x :: push_back elm xs let rec buildw_rec (i : int) (acc : nat list) : nat list = if i = 64 then acc else let v0 = select (i-15) acc in let sigma0 = (rot32 v0 7 25) lxor (rot32 v0 18 14) lxor (v0 lsr 3n) in let v1 = select (i-2) acc in let sigma1 = (rot32 v1 17 15) lxor (rot32 v1 19 13) lxor (v1 lsr 10n) in let w_i = sigma0 + (select (i-7) acc) + sigma1 + (select (i-16) acc) in buildw_rec (i+1) (push_back (w_i land max_uint32) acc) let compress (schedule : nat list) (hs : hashstate) : hashstate = let (h0,h1,h2,h3,h4,h5,h6,h7) : hashstate = hs in let rec round (ws : nat list) (ks : nat list) (s : hashstate ) : hashstate = let (a,b,c,d,e,f,g,h) = s in match (ws, ks) with | [],[] -> ( (h0+a) land max_uint32, (h1+b) land max_uint32, (h2+c) land max_uint32, (h3+d) land max_uint32, (h4+e) land max_uint32, (h5+f) land max_uint32, (h6+g) land max_uint32, (h7+h) land max_uint32) | wi::wx, ki::kx -> let t1 = h + (t1rot e) + (t1mix e f g) + ki + wi in let t2 = (t2rot a) + (t2mix a b c) in round wx kx ( (t1 + t2) land max_uint32, a, b, c, (d+t1) land max_uint32, e, f, g) | _ -> failwith "imposible state" in round schedule const_K hs let block (s : hashstate) (data : nat list) : hashstate = let w = buildw_rec 16 data in compress w s let input2list (input : block) : nat list = let (a,b,c,d,e,f,g,h,i,j,k,l,m,n,o,p) = input in [a; b; c; d; e; f; g; h; i; j; k; l; m; n; o; p] [@entry] let write_block (data : block) (store : storage) : ret = [], block store (input2list data) [@entry] let init () (_store : storage) : ret = [], state_init end ```