The codex[2²⁵⁶ - 1 - uint(keccak256(1)) + 1] corresponds to slot 0. How is that possible?

Question

I'm stuck with Ethernaut Alien Codex problem. I understood underflow attack except that codex[2²⁵⁶ - 1 - uint(keccak256(1)) + 1] corresponds to slot 0. I referred to the below tables.

Slot #	Variable
0	contact bool(1 bytes] & owner address (20 bytes), both fit on one slot
1	codex.length
keccak256(1)	codex[0]
keccak256(1) + 1	codex[1]
2²⁵⁶ - 1	codex[2²⁵⁶ - 1 - uint(keccak256(1))]
0	codex[2²⁵⁶ - 1 - uint(keccak256(1)) + 1] --> can write slot 0!

All I know is Storage has 2²⁵⁶ slots and a dynamic array that had been attacked can control every slot in the Storage. What am I missing? The source code is below.

// SPDX-License-Identifier: MIT
pragma solidity ^0.5.0;

import '../helpers/Ownable-05.sol';

contract AlienCodex is Ownable {

  bool public contact;
  bytes32[] public codex;

  modifier contacted() {
    assert(contact);
    _;
  }
  
  function make_contact() public {
    contact = true;
  }

  function record(bytes32 _content) contacted public {
    codex.push(_content);
  }

  function retract() contacted public {
    codex.length--;
  }

  function revise(uint i, bytes32 _content) contacted public {
    codex[i] = _content;
  }
}

Answer 1

So, we know codex[a] writes to slot a + keccak(1), for every number a, since that's how solidity saves a dynamic variable.

The number 2**256 - 1 - uint(keccak256(1)) + 1 can be simplified into 2**256 - keccak(1), since -1+1 = 0. Also since 2**256 = 0 (thinking modulo 2**256), the number becomes -keccak(1).

Using a = -keccak(1), we get:

codex[a] --->   a + keccak(1) = -keccak(1) + keccak(1) = 0

so we're writing to slot 0.