(* This code extends 'word_prelude'. *) val GETKEYS = (fn v87 => (case v87 of (Pair (v86, v85)) => (case v85 of (Pair (v84, v83)) => (case v83 of (Pair (v82, v81)) => (case v81 of (Pair (v80, v79)) => (case v79 of (Pair (v78, v77)) => (case v77 of (Pair (v76, v75)) => (case v75 of (Pair (v74, v73)) => (case v73 of (Pair (v72, v71)) => (case v71 of (Pair (v70, v69)) => (case v69 of (Pair (v68, v67)) => (case v67 of (Pair (v66, v65)) => (case v65 of (Pair (v64, v63)) => (case v63 of (Pair (v62, v61)) => (case v61 of (Pair (v60, v59)) => (case v59 of (Pair (v58, v57)) => (case v57 of (Pair (v56, v55)) => (case v55 of (Pair (v54, v53)) => (case v53 of (Pair (v52, v51)) => (case v51 of (Pair (v50, v49)) => (case v49 of (Pair (v48, v47)) => (case v47 of (Pair (v46, v45)) => (case v45 of (Pair (v44, v43)) => (case v43 of (Pair (v42, v41)) => (case v41 of (Pair (v40, v39)) => (case v39 of (Pair (v38, v37)) => (case v37 of (Pair (v36, v35)) => (case v35 of (Pair (v34, v33)) => (case v33 of (Pair (v32, v31)) => (case v31 of (Pair (v30, v29)) => (case v29 of (Pair (v28, v27)) => (case v27 of (Pair (v26, v25)) => (case v25 of (Pair (v24, v23)) => (case v23 of (Pair (v22, v21)) => (case v21 of (Pair (v20, v19)) => (case v19 of (Pair (v18, v17)) => (case v17 of (Pair (v16, v15)) => (case v15 of (Pair (v14, v13)) => (case v13 of (Pair (v12, v11)) => (case v11 of (Pair (v10, v9)) => (case v9 of (Pair (v8, v7)) => (case v7 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (Pair (v86, v84)))))))))))))))))))))))))))))))))))))))))))))) ; val PreWhitening = (fn v7 => (fn v8 => (case v8 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (Pair (v6, (Pair (((word_add v4) (FST (GETKEYS v7))), (Pair (v2, ((word_add v1) (SND (GETKEYS v7)))))))))))))) ; val ROTKEYS = (fn v87 => (case v87 of (Pair (v86, v85)) => (case v85 of (Pair (v84, v83)) => (case v83 of (Pair (v82, v81)) => (case v81 of (Pair (v80, v79)) => (case v79 of (Pair (v78, v77)) => (case v77 of (Pair (v76, v75)) => (case v75 of (Pair (v74, v73)) => (case v73 of (Pair (v72, v71)) => (case v71 of (Pair (v70, v69)) => (case v69 of (Pair (v68, v67)) => (case v67 of (Pair (v66, v65)) => (case v65 of (Pair (v64, v63)) => (case v63 of (Pair (v62, v61)) => (case v61 of (Pair (v60, v59)) => (case v59 of (Pair (v58, v57)) => (case v57 of (Pair (v56, v55)) => (case v55 of (Pair (v54, v53)) => (case v53 of (Pair (v52, v51)) => (case v51 of (Pair (v50, v49)) => (case v49 of (Pair (v48, v47)) => (case v47 of (Pair (v46, v45)) => (case v45 of (Pair (v44, v43)) => (case v43 of (Pair (v42, v41)) => (case v41 of (Pair (v40, v39)) => (case v39 of (Pair (v38, v37)) => (case v37 of (Pair (v36, v35)) => (case v35 of (Pair (v34, v33)) => (case v33 of (Pair (v32, v31)) => (case v31 of (Pair (v30, v29)) => (case v29 of (Pair (v28, v27)) => (case v27 of (Pair (v26, v25)) => (case v25 of (Pair (v24, v23)) => (case v23 of (Pair (v22, v21)) => (case v21 of (Pair (v20, v19)) => (case v19 of (Pair (v18, v17)) => (case v17 of (Pair (v16, v15)) => (case v15 of (Pair (v14, v13)) => (case v13 of (Pair (v12, v11)) => (case v11 of (Pair (v10, v9)) => (case v9 of (Pair (v8, v7)) => (case v7 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (Pair (v82, (Pair (v80, (Pair (v78, (Pair (v76, (Pair (v74, (Pair (v72, (Pair (v70, (Pair (v68, (Pair (v66, (Pair (v64, (Pair (v62, (Pair (v60, (Pair (v58, (Pair (v56, (Pair (v54, (Pair (v52, (Pair (v50, (Pair (v48, (Pair (v46, (Pair (v44, (Pair (v42, (Pair (v40, (Pair (v38, (Pair (v36, (Pair (v34, (Pair (v32, (Pair (v30, (Pair (v28, (Pair (v26, (Pair (v24, (Pair (v22, (Pair (v20, (Pair (v18, (Pair (v16, (Pair (v14, (Pair (v12, (Pair (v10, (Pair (v8, (Pair (v6, (Pair (v4, (Pair (v2, (Pair (v1, (Pair (v86, v84)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ; val InvPostWhitening = (fn v7 => (fn v8 => (case v8 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (Pair (v6, (Pair (((word_sub v4) (FST (GETKEYS v7))), (Pair (v2, ((word_sub v1) (SND (GETKEYS v7)))))))))))))) ; val InvPreWhitening = (fn v7 => (fn v8 => (case v8 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (Pair (((word_sub v6) (SND (GETKEYS v7))), (Pair (v4, (Pair (((word_sub v2) (SND (GETKEYS v7))), v1))))))))))) ; val RightShift = (fn v2 => (fn v1 => ((word_ror v2) v1))) ; val LeftShift = (fn v2 => (fn v1 => ((word_rol v2) v1))) ; val CompUT = (fn v1 => ((word_rol ((word_mul v1) ((word_add ((word_add v1) v1)) let val x = 1 in (x mod 4294967296) end ))) 5)) ; val FwdRound = (fn v10 => (fn v9 => (case v10 of (Pair (v8, v7)) => (case v7 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v9 of (Pair (v2, v1)) => (Pair (v6, (Pair (((word_add ((LeftShift ((word_xor v4) (CompUT v3))) (CompUT v6))) v1), (Pair (v3, ((word_add ((LeftShift ((word_xor v8) (CompUT v6))) (CompUT v3))) v2))))))))))))) ; val BwdRound = (fn v10 => (fn v9 => (case v10 of (Pair (v8, v7)) => (case v7 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v9 of (Pair (v2, v1)) => (Pair (((word_xor ((RightShift ((word_sub v3) v2)) (CompUT v4))) (CompUT v8)), (Pair (v8, (Pair (((word_xor ((RightShift ((word_sub v6) v1)) (CompUT v8))) (CompUT v4)), v4)))))))))))) ; val PostWhitening = (fn v7 => (fn v8 => (case v8 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (Pair (((word_add v6) (SND (GETKEYS v7))), (Pair (v4, (Pair (((word_add v2) (SND (GETKEYS v7))), v1))))))))))) ; fun Round v3 = (fn v2 => (fn v1 => (if (v3 <= 0) then ((PostWhitening v2) v1) else (((Round (v3 - 1)) (ROTKEYS v2)) ((FwdRound v1) (GETKEYS v2)))))) ; fun InvRound v3 = (fn v2 => (fn v1 => (if (v3 <= 0) then ((InvPreWhitening v2) v1) else ((BwdRound (((InvRound (v3 - 1)) (ROTKEYS v2)) v1)) (GETKEYS v2))))) ; val r = 20 ; val RC6_FWD = (fn v1 => ((op o ((Round r) v1)) (PreWhitening v1))) ; val RC6_BWD = (fn v1 => ((op o (InvPostWhitening v1)) ((InvRound r) v1))) ;