Give formalizing day 8 a shot.

console.cr

@@ -0,0 +1,36 @@
+def parse(input)
+  input.lines.map do |s|
+    code, int = s.split(" ")
+    {code, int.to_i32}
+  end
+end
+
+def run(prog)
+  acc = 0
+  pc = 0
+  visited = Set(Int32).new
+  input = Channel(Int32).new
+  output = Channel({Symbol, Int32}).new
+  spawn do
+    loop do
+      if pc >= prog.size
+        output.send({:term, acc})
+        break
+      elsif visited.includes? pc
+        output.send({:inf, acc})
+        break
+      end
+
+      visited << pc
+      code, int = prog[pc]
+      case code
+      when "acc"
+        acc += int
+      when "jmp"
+        pc += int - 1
+      end
+      pc += 1
+    end
+  end
+  {input, output}
+end

day10.cr

@@ -0,0 +1,37 @@
+require "advent"
+INPUT = input(2020, 10).lines.map(&.to_i32).sort!
+
+def part1(input)
+  diff_1 = 0
+  diff_3 = 0
+  curr = 0
+  input << (input.max + 3)
+  input.each do |i|
+    diff_1 += 1 if (i - curr) == 1
+    diff_3 += 1 if (i - curr) == 3
+    curr = i
+  end
+  puts diff_1 * diff_3
+end
+
+def count_ways(input, prev, index, mem, indent = 0)
+  if m = mem[{prev, index}]?
+    return m 
+  end
+  return 0_i64 if input[index] - prev > 3 || index >= input.size
+  return 1_i64 if index == input.size - 1
+
+  total = count_ways(input, input[index], index+1, mem, indent + 1)
+  total += count_ways(input, prev, index+1, mem, indent + 1)
+
+  mem[{prev, index}] = total
+  return total
+end
+
+def part2(input)
+  input << (input.max + 3)
+  count_ways(input, 0, 0, {} of {Int32, Int32} => Int64)
+end
+
+puts part1(INPUT.clone)
+puts part2(INPUT.clone)

day11.cr

@@ -0,0 +1,64 @@
+require "advent"
+INPUT = input(2020, 11).lines.map(&.chars) 
+
+abstract class Search
+  def search(current, x, y, dx, dy)
+    x, y = x + dx, y + dy
+    return 0 if y < 0 || y >= current.size
+    return 0 if x < 0 || x >= current[y].size
+    search_impl(current,x,y,dx,dy)
+  end
+
+  abstract def search_impl(current, x, y, dx, dy)
+end
+
+class FirstSearch < Search
+  def search_impl(current, x, y, dx, dy)
+    return current[y][x] == '#' ? 1 : 0
+  end
+end
+
+class SecondSearch < Search
+  def search_impl(current, x, y, dx, dy)
+    return 1 if current[y][x] == '#'
+    return 0 if current[y][x] == 'L'
+    return search(current, x, y, dx, dy)
+  end
+end
+
+DIRS = [{-1,-1}, {-1, 0}, {-1, 1}, {0, -1}, {0, 1}, {1, -1}, {1, 0}, {1,1}]
+
+def step(current, step, check, n)
+  current.each_with_index do |row, y|
+    row.each_with_index do |seat, x|
+      step[y][x] = current[y][x]
+      count = DIRS.sum do |dx, dy|
+        check.search(current, x, y, dx, dy)
+      end
+      step[y][x] = 'L' if seat == '#' && count >= n
+      step[y][x] = '#' if seat == 'L' && count == 0
+    end
+  end
+  {step, current}
+end
+
+def run(input, search, n)
+  current = input
+  step = input.clone
+  loop do
+    current, step = step(current, step, search, n)
+    break if current.zip_with(step) { |l, r| l == r }.all?
+  end
+  current.sum(&.count(&.==('#')))
+end
+
+def part1(input)
+  run(input, FirstSearch.new, 4)
+end
+
+def part2(input)
+  run(input, SecondSearch.new, 5)
+end
+
+puts part1(INPUT.clone)
+puts part2(INPUT.clone)

day8.cr

@@ -1,41 +1,21 @@
 require "advent"
-INPUT = input(2020, 8).lines.map do |s|
-  code, int = s.split(" ")
-  {code, int.to_i32}
-end
+require "./console.cr"
 
-def run(prog)
-  acc = 0
-  pc = 0
-  visited = Set(Int32).new
-  loop do
-    return {:term, acc} if pc >= prog.size
-    return {:inf, acc} if visited.includes? pc
-      
-    visited << pc
-    code, int = prog[pc]
-    case code
-    when "acc"
-      acc += int
-    when "jmp"
-      pc += int - 1
-    end
-    pc += 1
-  end
-end
+INPUT = input(2020, 8)
 
 def part1
-  run(INPUT)[1]
+  run(parse(INPUT))[1].receive[1]
 end
 
 def part2
-  jnp = INPUT.find_indices { |e| e[0] == "jmp" || e[0] == "nop" }
+  input = parse(INPUT)
+  jnp = input.find_indices { |e| e[0] == "jmp" || e[0] == "nop" }
   jnp.each do |i|
-    prog = INPUT.clone
+    prog = input.clone
     op, int = prog[i]
     prog[i] = {op.tr("jmpnop", "nopjmp"), int}
 
-    code, acc = run(prog)
+    code, acc = run(prog)[1].receive
     return acc if code == :term
   end
 end

day8.v

@@ -0,0 +1,98 @@
+Require Import Coq.ZArith.Int.
+Require Import Coq.Lists.ListSet.
+Require Import Coq.Vectors.VectorDef.
+Require Import Coq.Vectors.Fin.
+
+Module DayEight (Import M:Int).
+  (* We need to coerce natural numbers into integers to add them. *)
+  Parameter nat_to_t : nat -> t.
+  (* We need a way to convert integers back into finite sets. *)
+  Parameter clamp : forall {n}, t -> option (Fin.t n).
+
+  Definition fin := Fin.t.
+  
+  (* The opcode of our instructions. *)
+  Inductive opcode : Type :=
+    | add
+    | nop
+    | jmp.
+
+  (* The result of running a program is either the accumulator
+     or an infinite loop error. In the latter case, we return the
+     set of instructions that we tried. *)
+  Inductive run_result {n : nat} : Type :=
+    | Ok : t -> run_result
+    | Fail : set (fin n) -> run_result.
+
+  Definition state n : Type := (fin (S n) * set (fin n) * t).
+
+  (* An instruction is a pair of an opcode and an argument. *)
+  Definition inst : Type := (opcode * t).
+  (* An input is a bounded list of instructions. *)
+  Definition input (n : nat) := VectorDef.t inst n.
+  (* 'indices' represents the list of instruction
+     addresses, which are used for calculating jumps. *)
+  Definition indices (n : nat) := VectorDef.t (fin n) n.
+
+  (* Compute the destination jump index, an integer. *)
+  Definition jump_t {n} (pc : fin n) (off : t) : t :=
+    M.add (nat_to_t (proj1_sig (to_nat pc))) off.
+
+  (* Compute a destination index that's valid.
+     Not all inputs are valid, so this may fail. *)
+  Definition valid_jump_t {n} (pc : fin n) (off : t) : option (fin (S n)) := @clamp (S n) (jump_t pc off).
+
+  Definition weaken_one {n} (f : fin n) : fin (S n).
+  Proof.
+    apply (@cast (n + 1)).
+    + apply L. apply f.
+    + rewrite <- plus_n_Sm. rewrite <- plus_n_O. reflexivity.
+  Defined.
+
+  Inductive step_noswap {n} : input n -> state n -> state n -> Prop :=
+    | step_noswap_acc : forall inp pc' v acc t,
+        nth inp pc' = (add, t) ->
+        ~ set_mem Fin.eq_dec pc' v = true ->
+        step_noswap inp (weaken_one pc', v, acc) (FS pc', set_add Fin.eq_dec pc' v, M.add acc t)
+    | step_noswap_nop : forall inp pc' v acc t,
+        nth inp pc' = (nop, t) ->
+        ~ set_mem Fin.eq_dec pc' v = true ->
+        step_noswap inp (weaken_one pc', v, acc) (FS pc', set_add Fin.eq_dec pc' v, acc)
+    | step_noswap_jmp : forall inp pc' pc'' v acc t,
+        nth inp pc' = (jmp, t) ->
+        ~ set_mem Fin.eq_dec pc' v = true ->
+        valid_jump_t pc' t = Some pc'' ->
+        step_noswap inp (weaken_one pc', v, acc) (pc'', set_add Fin.eq_dec pc' v, acc).
+
+  Fixpoint nat_to_fin (n : nat) : fin (S n) :=
+    match n with
+    | O => F1
+    | S n' => FS (nat_to_fin n')
+    end.
+
+  Inductive run_noswap {n} : input n -> state n -> state n -> Prop :=
+    | run_noswap_ok : forall inp v acc,
+        run_noswap inp (nat_to_fin n, v, acc) (nat_to_fin n, v, acc)
+    | run_noswap_fail : forall inp pc' v acc,
+        set_mem Fin.eq_dec pc' v = true ->
+        run_noswap inp (weaken_one pc', v, acc) (weaken_one pc', v, acc)
+    | run_noswap_trans : forall inp st st' st'',
+        step_noswap inp st st' -> run_noswap inp st' st'' -> run_noswap inp st st''.
+
+  Inductive valid_inst {n} : inst -> fin n -> Prop :=
+    | valid_inst_add : forall t f, valid_inst (add, t) f
+    | valid_inst_nop : forall t f f',
+        valid_jump_t f t = Some f' -> valid_inst (nop, t) f
+    | valid_inst_jmp : forall t f f',
+        valid_jump_t f t = Some f' -> valid_inst (jmp, t) f.
+
+  (* An input is valid if all its instructions are valid. *)
+  Definition valid_input {n} (inp : input n) : Prop := forall (pc : fin n),
+    valid_inst (nth inp pc) pc.
+
+  Theorem valid_input_terminates  : forall n (inp : input n) st,
+    valid_input inp -> exists st', run_noswap inp st st'.
+  Proof.
+    (* Stoppped here. *)
+  Admitted.
+End DayEight.

day9.cr

@@ -0,0 +1,37 @@
+require "advent"
+INPUT = input(2020, 9).lines.map(&.to_i64) 
+
+def is_sum(is, from, to, n)
+  if to <= from
+    return n == 0_i64
+  end
+  return is_sum(is, from, to-1, n) || is_sum(is, from, to-1, n-is[to-1])
+end
+
+def part1(input)
+  is = input
+  i = 25
+  loop do
+    return is[i] unless is_sum(is, i-25, i, is[i])
+    i += 1
+  end
+end
+
+def part2(input, i)
+  input.each_with_index do |e, j|
+    next if e == i
+    acc = i-e
+    k = j
+    while acc > 0
+      k += 1
+      acc -= input[k]
+    end
+    if acc == 0
+      min, max = input[j..k].minmax
+      return min+max
+    end
+  end
+end
+
+p1 = part1(INPUT.clone)
+puts part2(INPUT.clone, p1)

template.cr

@@ -1,13 +1,11 @@
 require "advent"
-INPUT = input(2020, n)#.lines.map(&.chomp) 
+INPUT = input(2020, n)#.lines.map(&.to_i32) 
 
-def part1
-  input = INPUT.clone
+def part1(input)
 end
 
-def part2
-  input = INPUT.clone
+def part2(input)
 end
 
-part1
-part2
+puts part1(INPUT.clone)
+puts part2(INPUT.clone)