(* This code extends 'word_prelude'. *) val Sbox = (fn v1 => let val x = ((EL v1) (Cons (99, (Cons (124, (Cons (119, (Cons (123, (Cons (242, (Cons (107, (Cons (111, (Cons (197, (Cons (48, (Cons (1, (Cons (103, (Cons (43, (Cons (254, (Cons (215, (Cons (171, (Cons (118, (Cons (202, (Cons (130, (Cons (201, (Cons (125, (Cons (250, (Cons (89, (Cons (71, (Cons (240, (Cons (173, (Cons (212, (Cons (162, (Cons (175, (Cons (156, (Cons (164, (Cons (114, (Cons (192, (Cons (183, (Cons (253, (Cons (147, (Cons (38, (Cons (54, (Cons (63, (Cons (247, (Cons (204, (Cons (52, (Cons (165, (Cons (229, (Cons (241, (Cons (113, (Cons (216, (Cons (49, (Cons (21, (Cons (4, (Cons (199, (Cons (35, (Cons (195, (Cons (24, (Cons (150, (Cons (5, (Cons (154, (Cons (7, (Cons (18, (Cons (128, (Cons (226, (Cons (235, (Cons (39, (Cons (178, (Cons (117, (Cons (9, (Cons (131, (Cons (44, (Cons (26, (Cons (27, (Cons (110, (Cons (90, (Cons (160, (Cons (82, (Cons (59, (Cons (214, (Cons (179, (Cons (41, (Cons (227, (Cons (47, (Cons (132, (Cons (83, (Cons (209, (Cons (0, (Cons (237, (Cons (32, (Cons (252, (Cons (177, (Cons (91, (Cons (106, (Cons (203, (Cons (190, (Cons (57, (Cons (74, (Cons (76, (Cons (88, (Cons (207, (Cons (208, (Cons (239, (Cons (170, (Cons (251, (Cons (67, (Cons (77, (Cons (51, (Cons (133, (Cons (69, (Cons (249, (Cons (2, (Cons (127, (Cons (80, (Cons (60, (Cons (159, (Cons (168, (Cons (81, (Cons (163, (Cons (64, (Cons (143, (Cons (146, (Cons (157, (Cons (56, (Cons (245, (Cons (188, (Cons (182, (Cons (218, (Cons (33, (Cons (16, (Cons (255, (Cons (243, (Cons (210, (Cons (205, (Cons (12, (Cons (19, (Cons (236, (Cons (95, (Cons (151, (Cons (68, (Cons (23, (Cons (196, (Cons (167, (Cons (126, (Cons (61, (Cons (100, (Cons (93, (Cons (25, (Cons (115, (Cons (96, (Cons (129, (Cons (79, (Cons (220, (Cons (34, (Cons (42, (Cons (144, (Cons (136, (Cons (70, (Cons (238, (Cons (184, (Cons (20, (Cons (222, (Cons (94, (Cons (11, (Cons (219, (Cons (224, (Cons (50, (Cons (58, (Cons (10, (Cons (73, (Cons (6, (Cons (36, (Cons (92, (Cons (194, (Cons (211, (Cons (172, (Cons (98, (Cons (145, (Cons (149, (Cons (228, (Cons (121, (Cons (231, (Cons (200, (Cons (55, (Cons (109, (Cons (141, (Cons (213, (Cons (78, (Cons (169, (Cons (108, (Cons (86, (Cons (244, (Cons (234, (Cons (101, (Cons (122, (Cons (174, (Cons (8, (Cons (186, (Cons (120, (Cons (37, (Cons (46, (Cons (28, (Cons (166, (Cons (180, (Cons (198, (Cons (232, (Cons (221, (Cons (116, (Cons (31, (Cons (75, (Cons (189, (Cons (139, (Cons (138, (Cons (112, (Cons (62, (Cons (181, (Cons (102, (Cons (72, (Cons (3, (Cons (246, (Cons (14, (Cons (97, (Cons (53, (Cons (87, (Cons (185, (Cons (134, (Cons (193, (Cons (29, (Cons (158, (Cons (225, (Cons (248, (Cons (152, (Cons (17, (Cons (105, (Cons (217, (Cons (142, (Cons (148, (Cons (155, (Cons (30, (Cons (135, (Cons (233, (Cons (206, (Cons (85, (Cons (40, (Cons (223, (Cons (140, (Cons (161, (Cons (137, (Cons (13, (Cons (191, (Cons (230, (Cons (66, (Cons (104, (Cons (65, (Cons (153, (Cons (45, (Cons (15, (Cons (176, (Cons (84, (Cons (187, (Cons (22, Nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in (x mod 256) end ) ; val InvSbox = (fn v1 => let val x = ((EL v1) (Cons (82, (Cons (9, (Cons (106, (Cons (213, (Cons (48, (Cons (54, (Cons (165, (Cons (56, (Cons (191, (Cons (64, (Cons (163, (Cons (158, (Cons (129, (Cons (243, (Cons (215, (Cons (251, (Cons (124, (Cons (227, (Cons (57, (Cons (130, (Cons (155, (Cons (47, (Cons (255, (Cons (135, (Cons (52, (Cons (142, (Cons (67, (Cons (68, (Cons (196, (Cons (222, (Cons (233, (Cons (203, (Cons (84, (Cons (123, (Cons (148, (Cons (50, (Cons (166, (Cons (194, (Cons (35, (Cons (61, (Cons (238, (Cons (76, (Cons (149, (Cons (11, (Cons (66, (Cons (250, (Cons (195, (Cons (78, (Cons (8, (Cons (46, (Cons (161, (Cons (102, (Cons (40, (Cons (217, (Cons (36, (Cons (178, (Cons (118, (Cons (91, (Cons (162, (Cons (73, (Cons (109, (Cons (139, (Cons (209, (Cons (37, (Cons (114, (Cons (248, (Cons (246, (Cons (100, (Cons (134, (Cons (104, (Cons (152, (Cons (22, (Cons (212, (Cons (164, (Cons (92, (Cons (204, (Cons (93, (Cons (101, (Cons (182, (Cons (146, (Cons (108, (Cons (112, (Cons (72, (Cons (80, (Cons (253, (Cons (237, (Cons (185, (Cons (218, (Cons (94, (Cons (21, (Cons (70, (Cons (87, (Cons (167, (Cons (141, (Cons (157, (Cons (132, (Cons (144, (Cons (216, (Cons (171, (Cons (0, (Cons (140, (Cons (188, (Cons (211, (Cons (10, (Cons (247, (Cons (228, (Cons (88, (Cons (5, (Cons (184, (Cons (179, (Cons (69, (Cons (6, (Cons (208, (Cons (44, (Cons (30, (Cons (143, (Cons (202, (Cons (63, (Cons (15, (Cons (2, (Cons (193, (Cons (175, (Cons (189, (Cons (3, (Cons (1, (Cons (19, (Cons (138, (Cons (107, (Cons (58, (Cons (145, (Cons (17, (Cons (65, (Cons (79, (Cons (103, (Cons (220, (Cons (234, (Cons (151, (Cons (242, (Cons (207, (Cons (206, (Cons (240, (Cons (180, (Cons (230, (Cons (115, (Cons (150, (Cons (172, (Cons (116, (Cons (34, (Cons (231, (Cons (173, (Cons (53, (Cons (133, (Cons (226, (Cons (249, (Cons (55, (Cons (232, (Cons (28, (Cons (117, (Cons (223, (Cons (110, (Cons (71, (Cons (241, (Cons (26, (Cons (113, (Cons (29, (Cons (41, (Cons (197, (Cons (137, (Cons (111, (Cons (183, (Cons (98, (Cons (14, (Cons (170, (Cons (24, (Cons (190, (Cons (27, (Cons (252, (Cons (86, (Cons (62, (Cons (75, (Cons (198, (Cons (210, (Cons (121, (Cons (32, (Cons (154, (Cons (219, (Cons (192, (Cons (254, (Cons (120, (Cons (205, (Cons (90, (Cons (244, (Cons (31, (Cons (221, (Cons (168, (Cons (51, (Cons (136, (Cons (7, (Cons (199, (Cons (49, (Cons (177, (Cons (18, (Cons (16, (Cons (89, (Cons (39, (Cons (128, (Cons (236, (Cons (95, (Cons (96, (Cons (81, (Cons (127, (Cons (169, (Cons (25, (Cons (181, (Cons (74, (Cons (13, (Cons (45, (Cons (229, (Cons (122, (Cons (159, (Cons (147, (Cons (201, (Cons (156, (Cons (239, (Cons (160, (Cons (224, (Cons (59, (Cons (77, (Cons (174, (Cons (42, (Cons (245, (Cons (176, (Cons (200, (Cons (235, (Cons (187, (Cons (60, (Cons (131, (Cons (83, (Cons (153, (Cons (97, (Cons (23, (Cons (43, (Cons (4, (Cons (126, (Cons (186, (Cons (119, (Cons (214, (Cons (38, (Cons (225, (Cons (105, (Cons (20, (Cons (99, (Cons (85, (Cons (33, (Cons (12, (Cons (125, Nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) in (x mod 256) end ) ; val genSubBytes = (fn v31 => (fn v32 => (case v32 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 ((v31 v30), (Pair ((v31 v28), (Pair ((v31 v26), (Pair ((v31 v24), (Pair ((v31 v22), (Pair ((v31 v20), (Pair ((v31 v18), (Pair ((v31 v16), (Pair ((v31 v14), (Pair ((v31 v12), (Pair ((v31 v10), (Pair ((v31 v8), (Pair ((v31 v6), (Pair ((v31 v4), (Pair ((v31 v2), (v31 v1)))))))))))))))))))))))))))))))))))))))))))))))) ; val SubBytes = (fn v1 => ((genSubBytes Sbox) v1)) ; val ShiftRows = (fn 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 (v30, (Pair (v28, (Pair (v26, (Pair (v24, (Pair (v20, (Pair (v18, (Pair (v16, (Pair (v22, (Pair (v10, (Pair (v8, (Pair (v14, (Pair (v12, (Pair (v1, (Pair (v6, (Pair (v4, v2)))))))))))))))))))))))))))))))))))))))))))))) ; val XOR_BLOCK = (fn v61 => (fn v62 => (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 v62 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 (((word_xor_1 v60) v30), (Pair (((word_xor_1 v58) v28), (Pair (((word_xor_1 v56) v26), (Pair (((word_xor_1 v54) v24), (Pair (((word_xor_1 v52) v22), (Pair (((word_xor_1 v50) v20), (Pair (((word_xor_1 v48) v18), (Pair (((word_xor_1 v46) v16), (Pair (((word_xor_1 v44) v14), (Pair (((word_xor_1 v42) v12), (Pair (((word_xor_1 v40) v10), (Pair (((word_xor_1 v38) v8), (Pair (((word_xor_1 v36) v6), (Pair (((word_xor_1 v34) v4), (Pair (((word_xor_1 v32) v2), ((word_xor_1 v31) v1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ; val AddRoundKey = (fn v1 => (XOR_BLOCK v1)) ; val genMixColumns = (fn v59 => (fn v60 => (case v60 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)) => let val v28 = (v59 (Pair (v58, (Pair (v50, (Pair (v42, v34))))))) in (case v28 of (Pair (v27, v26)) => (case v26 of (Pair (v25, v24)) => (case v24 of (Pair (v23, v22)) => let val v21 = (v59 (Pair (v56, (Pair (v48, (Pair (v40, v32))))))) in (case v21 of (Pair (v20, v19)) => (case v19 of (Pair (v18, v17)) => (case v17 of (Pair (v16, v15)) => let val v14 = (v59 (Pair (v54, (Pair (v46, (Pair (v38, v30))))))) in (case v14 of (Pair (v13, v12)) => (case v12 of (Pair (v11, v10)) => (case v10 of (Pair (v9, v8)) => let val v7 = (v59 (Pair (v52, (Pair (v44, (Pair (v36, v29))))))) in (case v7 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (Pair (v27, (Pair (v20, (Pair (v13, (Pair (v6, (Pair (v25, (Pair (v18, (Pair (v11, (Pair (v4, (Pair (v23, (Pair (v16, (Pair (v9, (Pair (v2, (Pair (v22, (Pair (v15, (Pair (v8, v1))))))))))))))))))))))))))))))))) end ))) end ))) end ))) end ))))))))))))))))) ; val xtime = (fn v1 => ((word_xor_1 ((word_lsl_2 v1) 1)) (if (word_msb_2 v1) then let val x = 27 in (x mod 256) end else let val x = 0 in (x mod 256) end ))) ; fun ** v1 = (fn v2 => (if (v1 = let val x = 0 in (x mod 256) end ) then let val x = 0 in (x mod 256) end else (if (word_lsb_2 v1) then ((word_xor_1 v2) (( ** ((word_lsr_2 v1) 1)) (xtime v2))) else (( ** ((word_lsr_2 v1) 1)) (xtime v2))))) ; val MultCol = (fn v7 => (case v7 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (Pair (((word_xor_1 (( ** let val x = 2 in (x mod 256) end ) v6)) ((word_xor_1 (( ** let val x = 3 in (x mod 256) end ) v4)) ((word_xor_1 v2) v1))), (Pair (((word_xor_1 v6) ((word_xor_1 (( ** let val x = 2 in (x mod 256) end ) v4)) ((word_xor_1 (( ** let val x = 3 in (x mod 256) end ) v2)) v1))), (Pair (((word_xor_1 v6) ((word_xor_1 v4) ((word_xor_1 (( ** let val x = 2 in (x mod 256) end ) v2)) (( ** let val x = 3 in (x mod 256) end ) v1)))), ((word_xor_1 (( ** let val x = 3 in (x mod 256) end ) v6)) ((word_xor_1 v4) ((word_xor_1 v2) (( ** let val x = 2 in (x mod 256) end ) v1)))))))))))))) ; val MixColumns = (fn v1 => ((genMixColumns MultCol) v1)) ; val ROTKEYS = (fn 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 (v18, (Pair (v16, (Pair (v14, (Pair (v12, (Pair (v10, (Pair (v8, (Pair (v6, (Pair (v4, (Pair (v2, (Pair (v1, v20))))))))))))))))))))))))))))))) ; fun RoundTuple v5 = (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (if (v4 <= 0) then (Pair (0, (Pair ((ROTKEYS v2), ((AddRoundKey (FST v2)) (ShiftRows (SubBytes v1))))))) else (RoundTuple (Pair ((v4 - 1), (Pair ((ROTKEYS v2), ((AddRoundKey (FST v2)) (MixColumns (ShiftRows (SubBytes v1)))))))))))) ; val Round = (fn v2 => (fn v1 => (fn v3 => (SND (SND (RoundTuple (Pair (v2, (Pair (v1, v3)))))))))) ; val from_state = (fn 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 (v30, (Pair (v22, (Pair (v14, (Pair (v6, (Pair (v28, (Pair (v20, (Pair (v12, (Pair (v4, (Pair (v26, (Pair (v18, (Pair (v10, (Pair (v2, (Pair (v24, (Pair (v16, (Pair (v8, v1)))))))))))))))))))))))))))))))))))))))))))))) ; val to_state = (fn 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 (v30, (Pair (v22, (Pair (v14, (Pair (v6, (Pair (v28, (Pair (v20, (Pair (v12, (Pair (v4, (Pair (v26, (Pair (v18, (Pair (v10, (Pair (v2, (Pair (v24, (Pair (v16, (Pair (v8, v1)))))))))))))))))))))))))))))))))))))))))))))) ; val InvMultCol = (fn v7 => (case v7 of (Pair (v6, v5)) => (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (Pair (((word_xor_1 (( ** let val x = 14 in (x mod 256) end ) v6)) ((word_xor_1 (( ** let val x = 11 in (x mod 256) end ) v4)) ((word_xor_1 (( ** let val x = 13 in (x mod 256) end ) v2)) (( ** let val x = 9 in (x mod 256) end ) v1)))), (Pair (((word_xor_1 (( ** let val x = 9 in (x mod 256) end ) v6)) ((word_xor_1 (( ** let val x = 14 in (x mod 256) end ) v4)) ((word_xor_1 (( ** let val x = 11 in (x mod 256) end ) v2)) (( ** let val x = 13 in (x mod 256) end ) v1)))), (Pair (((word_xor_1 (( ** let val x = 13 in (x mod 256) end ) v6)) ((word_xor_1 (( ** let val x = 9 in (x mod 256) end ) v4)) ((word_xor_1 (( ** let val x = 14 in (x mod 256) end ) v2)) (( ** let val x = 11 in (x mod 256) end ) v1)))), ((word_xor_1 (( ** let val x = 11 in (x mod 256) end ) v6)) ((word_xor_1 (( ** let val x = 13 in (x mod 256) end ) v4)) ((word_xor_1 (( ** let val x = 9 in (x mod 256) end ) v2)) (( ** let val x = 14 in (x mod 256) end ) v1)))))))))))))) ; val InvMixColumns = (fn v1 => ((genMixColumns InvMultCol) v1)) ; val InvShiftRows = (fn 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 (v30, (Pair (v28, (Pair (v26, (Pair (v24, (Pair (v16, (Pair (v22, (Pair (v20, (Pair (v18, (Pair (v10, (Pair (v8, (Pair (v14, (Pair (v12, (Pair (v4, (Pair (v2, (Pair (v1, v6)))))))))))))))))))))))))))))))))))))))))))))) ; val InvSubBytes = (fn v1 => ((genSubBytes InvSbox) v1)) ; fun InvRoundTuple v5 = (case v5 of (Pair (v4, v3)) => (case v3 of (Pair (v2, v1)) => (if (v4 <= 0) then (Pair (0, (Pair ((ROTKEYS v2), ((AddRoundKey (FST v2)) (InvSubBytes (InvShiftRows v1))))))) else (InvRoundTuple (Pair ((v4 - 1), (Pair ((ROTKEYS v2), (InvMixColumns ((AddRoundKey (FST v2)) (InvSubBytes (InvShiftRows v1)))))))))))) ; val InvRound = (fn v2 => (fn v1 => (fn v3 => (SND (SND (InvRoundTuple (Pair (v2, (Pair (v1, v3)))))))))) ; val AES_FWD = (fn v1 => ((op o from_state) ((op o ((Round 9) (ROTKEYS v1))) ((op o (AddRoundKey (FST v1))) to_state)))) ; val AES_BWD = (fn v1 => ((op o from_state) ((op o ((InvRound 9) (ROTKEYS v1))) ((op o (AddRoundKey (FST v1))) to_state)))) ;