1. 27

This a based on the Dawn article posted to lobsters recently.

  1.  

  2. 3

    I wrote some Agda formalizations here: https://github.com/wolverian/dawn/blob/main/Dawn.agda