import Base

# The AES byte substitution table, generated from the field inverse and affine map.
# A byte selects one literal branch so formal NIST checkpoints avoid expanding
# the exponentiation network for every substituted byte.
def lookup_index(index: Nat) -> U32:
    match index:
        case 0n: 99
        case 1n: 124
        case 2n: 119
        case 3n: 123
        case 4n: 242
        case 5n: 107
        case 6n: 111
        case 7n: 197
        case 8n: 48
        case 9n: 1
        case 10n: 103
        case 11n: 43
        case 12n: 254
        case 13n: 215
        case 14n: 171
        case 15n: 118
        case 16n: 202
        case 17n: 130
        case 18n: 201
        case 19n: 125
        case 20n: 250
        case 21n: 89
        case 22n: 71
        case 23n: 240
        case 24n: 173
        case 25n: 212
        case 26n: 162
        case 27n: 175
        case 28n: 156
        case 29n: 164
        case 30n: 114
        case 31n: 192
        case 32n: 183
        case 33n: 253
        case 34n: 147
        case 35n: 38
        case 36n: 54
        case 37n: 63
        case 38n: 247
        case 39n: 204
        case 40n: 52
        case 41n: 165
        case 42n: 229
        case 43n: 241
        case 44n: 113
        case 45n: 216
        case 46n: 49
        case 47n: 21
        case 48n: 4
        case 49n: 199
        case 50n: 35
        case 51n: 195
        case 52n: 24
        case 53n: 150
        case 54n: 5
        case 55n: 154
        case 56n: 7
        case 57n: 18
        case 58n: 128
        case 59n: 226
        case 60n: 235
        case 61n: 39
        case 62n: 178
        case 63n: 117
        case 64n: 9
        case 65n: 131
        case 66n: 44
        case 67n: 26
        case 68n: 27
        case 69n: 110
        case 70n: 90
        case 71n: 160
        case 72n: 82
        case 73n: 59
        case 74n: 214
        case 75n: 179
        case 76n: 41
        case 77n: 227
        case 78n: 47
        case 79n: 132
        case 80n: 83
        case 81n: 209
        case 82n: 0
        case 83n: 237
        case 84n: 32
        case 85n: 252
        case 86n: 177
        case 87n: 91
        case 88n: 106
        case 89n: 203
        case 90n: 190
        case 91n: 57
        case 92n: 74
        case 93n: 76
        case 94n: 88
        case 95n: 207
        case 96n: 208
        case 97n: 239
        case 98n: 170
        case 99n: 251
        case 100n: 67
        case 101n: 77
        case 102n: 51
        case 103n: 133
        case 104n: 69
        case 105n: 249
        case 106n: 2
        case 107n: 127
        case 108n: 80
        case 109n: 60
        case 110n: 159
        case 111n: 168
        case 112n: 81
        case 113n: 163
        case 114n: 64
        case 115n: 143
        case 116n: 146
        case 117n: 157
        case 118n: 56
        case 119n: 245
        case 120n: 188
        case 121n: 182
        case 122n: 218
        case 123n: 33
        case 124n: 16
        case 125n: 255
        case 126n: 243
        case 127n: 210
        case 128n: 205
        case 129n: 12
        case 130n: 19
        case 131n: 236
        case 132n: 95
        case 133n: 151
        case 134n: 68
        case 135n: 23
        case 136n: 196
        case 137n: 167
        case 138n: 126
        case 139n: 61
        case 140n: 100
        case 141n: 93
        case 142n: 25
        case 143n: 115
        case 144n: 96
        case 145n: 129
        case 146n: 79
        case 147n: 220
        case 148n: 34
        case 149n: 42
        case 150n: 144
        case 151n: 136
        case 152n: 70
        case 153n: 238
        case 154n: 184
        case 155n: 20
        case 156n: 222
        case 157n: 94
        case 158n: 11
        case 159n: 219
        case 160n: 224
        case 161n: 50
        case 162n: 58
        case 163n: 10
        case 164n: 73
        case 165n: 6
        case 166n: 36
        case 167n: 92
        case 168n: 194
        case 169n: 211
        case 170n: 172
        case 171n: 98
        case 172n: 145
        case 173n: 149
        case 174n: 228
        case 175n: 121
        case 176n: 231
        case 177n: 200
        case 178n: 55
        case 179n: 109
        case 180n: 141
        case 181n: 213
        case 182n: 78
        case 183n: 169
        case 184n: 108
        case 185n: 86
        case 186n: 244
        case 187n: 234
        case 188n: 101
        case 189n: 122
        case 190n: 174
        case 191n: 8
        case 192n: 186
        case 193n: 120
        case 194n: 37
        case 195n: 46
        case 196n: 28
        case 197n: 166
        case 198n: 180
        case 199n: 198
        case 200n: 232
        case 201n: 221
        case 202n: 116
        case 203n: 31
        case 204n: 75
        case 205n: 189
        case 206n: 139
        case 207n: 138
        case 208n: 112
        case 209n: 62
        case 210n: 181
        case 211n: 102
        case 212n: 72
        case 213n: 3
        case 214n: 246
        case 215n: 14
        case 216n: 97
        case 217n: 53
        case 218n: 87
        case 219n: 185
        case 220n: 134
        case 221n: 193
        case 222n: 29
        case 223n: 158
        case 224n: 225
        case 225n: 248
        case 226n: 152
        case 227n: 17
        case 228n: 105
        case 229n: 217
        case 230n: 142
        case 231n: 148
        case 232n: 155
        case 233n: 30
        case 234n: 135
        case 235n: 233
        case 236n: 206
        case 237n: 85
        case 238n: 40
        case 239n: 223
        case 240n: 140
        case 241n: 161
        case 242n: 137
        case 243n: 13
        case 244n: 191
        case 245n: 230
        case 246n: 66
        case 247n: 104
        case 248n: 65
        case 249n: 153
        case 250n: 45
        case 251n: 15
        case 252n: 176
        case 253n: 84
        case 254n: 187
        case 255n: 22
        case _: 0

def lookup(value: U32) -> U32:
    lookup_index(U32.to_nat(U32.and(255, value)))