(* This code extends 'word_prelude'. *) let Sbox = (fun v1 -> (let 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))) ;; let InvSbox = (fun v1 -> (let 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))) ;; let genSubBytes = (fun v31 -> (fun v32 -> (match v32 with (Pair (v30, v29)) -> (match v29 with (Pair (v28, v27)) -> (match v27 with (Pair (v26, v25)) -> (match v25 with (Pair (v24, v23)) -> (match v23 with (Pair (v22, v21)) -> (match v21 with (Pair (v20, v19)) -> (match v19 with (Pair (v18, v17)) -> (match v17 with (Pair (v16, v15)) -> (match v15 with (Pair (v14, v13)) -> (match v13 with (Pair (v12, v11)) -> (match v11 with (Pair (v10, v9)) -> (match v9 with (Pair (v8, v7)) -> (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (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)))))))))))))))))))))))))))))))))))))))))))))))) ;; let SubBytes = (fun v1 -> ((genSubBytes Sbox) v1)) ;; let ShiftRows = (fun v31 -> (match v31 with (Pair (v30, v29)) -> (match v29 with (Pair (v28, v27)) -> (match v27 with (Pair (v26, v25)) -> (match v25 with (Pair (v24, v23)) -> (match v23 with (Pair (v22, v21)) -> (match v21 with (Pair (v20, v19)) -> (match v19 with (Pair (v18, v17)) -> (match v17 with (Pair (v16, v15)) -> (match v15 with (Pair (v14, v13)) -> (match v13 with (Pair (v12, v11)) -> (match v11 with (Pair (v10, v9)) -> (match v9 with (Pair (v8, v7)) -> (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (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)))))))))))))))))))))))))))))))))))))))))))))) ;; let XOR_BLOCK = (fun v61 -> (fun v62 -> (match v61 with (Pair (v60, v59)) -> (match v59 with (Pair (v58, v57)) -> (match v57 with (Pair (v56, v55)) -> (match v55 with (Pair (v54, v53)) -> (match v53 with (Pair (v52, v51)) -> (match v51 with (Pair (v50, v49)) -> (match v49 with (Pair (v48, v47)) -> (match v47 with (Pair (v46, v45)) -> (match v45 with (Pair (v44, v43)) -> (match v43 with (Pair (v42, v41)) -> (match v41 with (Pair (v40, v39)) -> (match v39 with (Pair (v38, v37)) -> (match v37 with (Pair (v36, v35)) -> (match v35 with (Pair (v34, v33)) -> (match v33 with (Pair (v32, v31)) -> (match v62 with (Pair (v30, v29)) -> (match v29 with (Pair (v28, v27)) -> (match v27 with (Pair (v26, v25)) -> (match v25 with (Pair (v24, v23)) -> (match v23 with (Pair (v22, v21)) -> (match v21 with (Pair (v20, v19)) -> (match v19 with (Pair (v18, v17)) -> (match v17 with (Pair (v16, v15)) -> (match v15 with (Pair (v14, v13)) -> (match v13 with (Pair (v12, v11)) -> (match v11 with (Pair (v10, v9)) -> (match v9 with (Pair (v8, v7)) -> (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ;; let AddRoundKey = (fun v1 -> (XOR_BLOCK v1)) ;; let genMixColumns = (fun v59 -> (fun v60 -> (match v60 with (Pair (v58, v57)) -> (match v57 with (Pair (v56, v55)) -> (match v55 with (Pair (v54, v53)) -> (match v53 with (Pair (v52, v51)) -> (match v51 with (Pair (v50, v49)) -> (match v49 with (Pair (v48, v47)) -> (match v47 with (Pair (v46, v45)) -> (match v45 with (Pair (v44, v43)) -> (match v43 with (Pair (v42, v41)) -> (match v41 with (Pair (v40, v39)) -> (match v39 with (Pair (v38, v37)) -> (match v37 with (Pair (v36, v35)) -> (match v35 with (Pair (v34, v33)) -> (match v33 with (Pair (v32, v31)) -> (match v31 with (Pair (v30, v29)) -> (let v28 = (v59 (Pair (v58, (Pair (v50, (Pair (v42, v34))))))) in (match v28 with (Pair (v27, v26)) -> (match v26 with (Pair (v25, v24)) -> (match v24 with (Pair (v23, v22)) -> (let v21 = (v59 (Pair (v56, (Pair (v48, (Pair (v40, v32))))))) in (match v21 with (Pair (v20, v19)) -> (match v19 with (Pair (v18, v17)) -> (match v17 with (Pair (v16, v15)) -> (let v14 = (v59 (Pair (v54, (Pair (v46, (Pair (v38, v30))))))) in (match v14 with (Pair (v13, v12)) -> (match v12 with (Pair (v11, v10)) -> (match v10 with (Pair (v9, v8)) -> (let v7 = (v59 (Pair (v52, (Pair (v44, (Pair (v36, v29))))))) in (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ;; let xtime = (fun v1 -> ((word_xor_1 ((word_lsl_2 v1) 1)) (if (word_msb_2 v1) then (let x = 27 in (x mod 256)) else (let x = 0 in (x mod 256))))) ;; let rec ** v1 = (fun v2 -> (if (v1 = (let x = 0 in (x mod 256))) then (let x = 0 in (x mod 256)) 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))))) ;; let MultCol = (fun v7 -> (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (Pair (v2, v1)) -> (Pair (((word_xor_1 (( ** (let x = 2 in (x mod 256))) v6)) ((word_xor_1 (( ** (let x = 3 in (x mod 256))) v4)) ((word_xor_1 v2) v1))), (Pair (((word_xor_1 v6) ((word_xor_1 (( ** (let x = 2 in (x mod 256))) v4)) ((word_xor_1 (( ** (let x = 3 in (x mod 256))) v2)) v1))), (Pair (((word_xor_1 v6) ((word_xor_1 v4) ((word_xor_1 (( ** (let x = 2 in (x mod 256))) v2)) (( ** (let x = 3 in (x mod 256))) v1)))), ((word_xor_1 (( ** (let x = 3 in (x mod 256))) v6)) ((word_xor_1 v4) ((word_xor_1 v2) (( ** (let x = 2 in (x mod 256))) v1)))))))))))))) ;; let MixColumns = (fun v1 -> ((genMixColumns MultCol) v1)) ;; let ROTKEYS = (fun v21 -> (match v21 with (Pair (v20, v19)) -> (match v19 with (Pair (v18, v17)) -> (match v17 with (Pair (v16, v15)) -> (match v15 with (Pair (v14, v13)) -> (match v13 with (Pair (v12, v11)) -> (match v11 with (Pair (v10, v9)) -> (match v9 with (Pair (v8, v7)) -> (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (Pair (v2, v1)) -> (Pair (v18, (Pair (v16, (Pair (v14, (Pair (v12, (Pair (v10, (Pair (v8, (Pair (v6, (Pair (v4, (Pair (v2, (Pair (v1, v20))))))))))))))))))))))))))))))) ;; let rec RoundTuple v5 = (match v5 with (Pair (v4, v3)) -> (match v3 with (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)))))))))))) ;; let Round = (fun v2 -> (fun v1 -> (fun v3 -> (SND (SND (RoundTuple (Pair (v2, (Pair (v1, v3)))))))))) ;; let from_state = (fun v31 -> (match v31 with (Pair (v30, v29)) -> (match v29 with (Pair (v28, v27)) -> (match v27 with (Pair (v26, v25)) -> (match v25 with (Pair (v24, v23)) -> (match v23 with (Pair (v22, v21)) -> (match v21 with (Pair (v20, v19)) -> (match v19 with (Pair (v18, v17)) -> (match v17 with (Pair (v16, v15)) -> (match v15 with (Pair (v14, v13)) -> (match v13 with (Pair (v12, v11)) -> (match v11 with (Pair (v10, v9)) -> (match v9 with (Pair (v8, v7)) -> (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (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)))))))))))))))))))))))))))))))))))))))))))))) ;; let to_state = (fun v31 -> (match v31 with (Pair (v30, v29)) -> (match v29 with (Pair (v28, v27)) -> (match v27 with (Pair (v26, v25)) -> (match v25 with (Pair (v24, v23)) -> (match v23 with (Pair (v22, v21)) -> (match v21 with (Pair (v20, v19)) -> (match v19 with (Pair (v18, v17)) -> (match v17 with (Pair (v16, v15)) -> (match v15 with (Pair (v14, v13)) -> (match v13 with (Pair (v12, v11)) -> (match v11 with (Pair (v10, v9)) -> (match v9 with (Pair (v8, v7)) -> (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (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)))))))))))))))))))))))))))))))))))))))))))))) ;; let InvMultCol = (fun v7 -> (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (Pair (v2, v1)) -> (Pair (((word_xor_1 (( ** (let x = 14 in (x mod 256))) v6)) ((word_xor_1 (( ** (let x = 11 in (x mod 256))) v4)) ((word_xor_1 (( ** (let x = 13 in (x mod 256))) v2)) (( ** (let x = 9 in (x mod 256))) v1)))), (Pair (((word_xor_1 (( ** (let x = 9 in (x mod 256))) v6)) ((word_xor_1 (( ** (let x = 14 in (x mod 256))) v4)) ((word_xor_1 (( ** (let x = 11 in (x mod 256))) v2)) (( ** (let x = 13 in (x mod 256))) v1)))), (Pair (((word_xor_1 (( ** (let x = 13 in (x mod 256))) v6)) ((word_xor_1 (( ** (let x = 9 in (x mod 256))) v4)) ((word_xor_1 (( ** (let x = 14 in (x mod 256))) v2)) (( ** (let x = 11 in (x mod 256))) v1)))), ((word_xor_1 (( ** (let x = 11 in (x mod 256))) v6)) ((word_xor_1 (( ** (let x = 13 in (x mod 256))) v4)) ((word_xor_1 (( ** (let x = 9 in (x mod 256))) v2)) (( ** (let x = 14 in (x mod 256))) v1)))))))))))))) ;; let InvMixColumns = (fun v1 -> ((genMixColumns InvMultCol) v1)) ;; let InvShiftRows = (fun v31 -> (match v31 with (Pair (v30, v29)) -> (match v29 with (Pair (v28, v27)) -> (match v27 with (Pair (v26, v25)) -> (match v25 with (Pair (v24, v23)) -> (match v23 with (Pair (v22, v21)) -> (match v21 with (Pair (v20, v19)) -> (match v19 with (Pair (v18, v17)) -> (match v17 with (Pair (v16, v15)) -> (match v15 with (Pair (v14, v13)) -> (match v13 with (Pair (v12, v11)) -> (match v11 with (Pair (v10, v9)) -> (match v9 with (Pair (v8, v7)) -> (match v7 with (Pair (v6, v5)) -> (match v5 with (Pair (v4, v3)) -> (match v3 with (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)))))))))))))))))))))))))))))))))))))))))))))) ;; let InvSubBytes = (fun v1 -> ((genSubBytes InvSbox) v1)) ;; let rec InvRoundTuple v5 = (match v5 with (Pair (v4, v3)) -> (match v3 with (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)))))))))))) ;; let InvRound = (fun v2 -> (fun v1 -> (fun v3 -> (SND (SND (InvRoundTuple (Pair (v2, (Pair (v1, v3)))))))))) ;; let AES_FWD = (fun v1 -> ((o from_state) ((o ((Round 9) (ROTKEYS v1))) ((o (AddRoundKey (FST v1))) to_state)))) ;; let AES_BWD = (fun v1 -> ((o from_state) ((o ((InvRound 9) (ROTKEYS v1))) ((o (AddRoundKey (FST v1))) to_state)))) ;;