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