20201211 11:32:54 08:00



Require Import Coq.ZArith.Int.




Require Import Coq.Lists.ListSet.




Require Import Coq.Vectors.VectorDef.




Require Import Coq.Vectors.Fin.

20201212 01:44:16 08:00



Require Import Coq.Program.Equality.




Require Import Coq.Logic.Eqdep_dec.




Require Import Coq.Arith.Peano_dec.

20201212 22:49:52 08:00



Require Import Coq.Program.Wf.




Require Import Lia.

20201211 11:32:54 08:00







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.





20201213 20:34:28 08:00



(* A single program state .*)

20201211 11:32:54 08:00



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.





20201213 20:34:28 08:00



(* Change a jump to a nop, or a nop to a jump. *)




Definition replace (i : inst) : inst :=




match i with




 (add, t) => (add, t)




 (nop, t) => (jmp, t)




 (jmp, t) => (nop, t)




end.





20201211 11:32:54 08:00



(* 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).





20201213 20:34:28 08:00



(* Cast a fin n to a fin (S n). *)

20201212 01:44:16 08:00



Fixpoint weaken_one {n} (f : fin n) : fin (S n) :=




match f with




 F1 => F1




 FS f' => FS (weaken_one f')




end.

20201211 11:32:54 08:00




20201213 20:34:28 08:00



(* Convert a nat to fin. *)

20201212 20:08:21 08:00



Fixpoint nat_to_fin (n : nat) : fin (S n) :=




match n with




 O => F1




 S n' => FS (nat_to_fin n')




end.





20201213 20:34:28 08:00



(* A finite natural is either its maximum value (aka nat_to_fin n),




or it's not thatbig, which means it can be cast down to




a fin (pred n). *)

20201212 20:08:21 08:00



Lemma fin_big_or_small : forall {n} (f : fin (S n)),




(f = nat_to_fin n) \/ (exists (f' : fin n), f = weaken_one f').




Proof.




(* Hey, looks like the creator of Fin provided




us with nice inductive principles. Using Coq's




default `induction` breaks here.








Merci, Pierre! *)




apply Fin.rectS.




 intros n. destruct n.




+ left. reflexivity.




+ right. exists F1. auto.




 intros n p IH.




destruct IH.




+ left. rewrite H. reflexivity.




+ right. destruct H as [f' Heq].




exists (FS f'). simpl. rewrite Heq.




reflexivity.




Qed.





20201212 01:44:16 08:00



(* One modification: we really want to use 'allowed' addresses,




a set that shrinks as the program continues, rather than 'visited'




addresses, a set that increases as the program continues. *)

20201211 11:32:54 08:00



Inductive step_noswap {n} : input n > state n > state n > Prop :=

20201212 01:44:16 08:00



 step_noswap_add : forall inp pc' v acc t,

20201211 11:32:54 08:00



nth inp pc' = (add, t) >

20201212 20:08:21 08:00



set_In pc' v >

20201212 01:44:16 08:00



step_noswap inp (weaken_one pc', v, acc) (FS pc', set_remove Fin.eq_dec pc' v, M.add acc t)

20201211 11:32:54 08:00



 step_noswap_nop : forall inp pc' v acc t,




nth inp pc' = (nop, t) >

20201212 20:08:21 08:00



set_In pc' v >

20201212 01:44:16 08:00



step_noswap inp (weaken_one pc', v, acc) (FS pc', set_remove Fin.eq_dec pc' v, acc)

20201211 11:32:54 08:00



 step_noswap_jmp : forall inp pc' pc'' v acc t,




nth inp pc' = (jmp, t) >

20201212 20:08:21 08:00



set_In pc' v >

20201211 11:32:54 08:00



valid_jump_t pc' t = Some pc'' >

20201212 01:44:16 08:00



step_noswap inp (weaken_one pc', v, acc) (pc'', set_remove Fin.eq_dec pc' v, acc).

20201211 11:32:54 08:00




20201212 20:08:21 08:00



Inductive done {n} : input n > state n > Prop :=




 done_prog : forall inp v acc, done inp (nat_to_fin n, v, acc).








Inductive stuck {n} : input n > state n > Prop :=




 stuck_prog : forall inp pc' v acc,




~ set_In pc' v > stuck inp (weaken_one pc', v, acc).

20201211 11:32:54 08:00







Inductive run_noswap {n} : input n > state n > state n > Prop :=

20201212 20:08:21 08:00



 run_noswap_ok : forall inp st, done inp st > run_noswap inp st st




 run_noswap_fail : forall inp st, stuck inp st > run_noswap inp st st

20201211 11:32:54 08:00



 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.





20201212 20:08:21 08:00



Section ValidInput.




Variable n : nat.




Variable inp : input n.




Hypothesis Hv : valid_input inp.





20201213 20:34:28 08:00



(* If the current address, which is not the end of the array, is




present in the "allowed" set, the program can continue. *)

20201212 20:08:21 08:00



Lemma step_if_possible : forall pcs v acc,




set_In pcs v >




exists pc' acc', step_noswap inp (weaken_one pcs, v, acc) (pc', set_remove Fin.eq_dec pcs v, acc').




Proof.




intros pcs v acc Hin.




remember (nth inp pcs) as instr. destruct instr as [op t]. destruct op.




+ exists (FS pcs). exists (M.add acc t). apply step_noswap_add; auto.




+ exists (FS pcs). exists acc. apply step_noswap_nop with t; auto.




+ unfold valid_input in Hv. specialize (Hv pcs).




rewrite < Heqinstr in Hv. inversion Hv; subst.




exists f'. exists acc. apply step_noswap_jmp with t; auto.




Qed.





20201213 20:34:28 08:00



(* A program is either done, stuck (at an invalid/visited address), or can step. *)

20201212 20:08:21 08:00



Theorem valid_input_progress : forall pc v acc,




(pc = nat_to_fin n /\ done inp (pc, v, acc)) \/

20201212 22:49:52 08:00



(exists pcs, pc = weaken_one pcs /\

20201212 20:08:21 08:00



((~ set_In pcs v /\ stuck inp (pc, v, acc)) \/

20201213 20:34:28 08:00



(exists pc' acc', set_In pcs v /\




step_noswap inp (pc, v, acc) (pc', set_remove Fin.eq_dec pcs v, acc')))).

20201212 20:08:21 08:00



Proof.




intros pc v acc.




(* Have we reached the end? *)




destruct (fin_big_or_small pc).




(* We're at the end, so we're done. *)




left. rewrite H. split. reflexivity. apply done_prog.

20201213 20:34:28 08:00



(* We're not at the end. *)

20201212 20:08:21 08:00



right. destruct H as [pcs H]. exists pcs. rewrite H. split. reflexivity.

20201213 20:34:28 08:00



(* We're not at the end. Is the PC valid? *)

20201212 20:08:21 08:00



destruct (set_In_dec Fin.eq_dec pcs v).




 (* It is. *)




right.




destruct (step_if_possible pcs v acc) as [pc' [acc' Hstep]]; auto.




exists pc'. exists acc'. split; auto.

20201213 20:34:28 08:00



 (* It is not. *)

20201212 20:08:21 08:00



left. split; auto. apply stuck_prog; auto.




Qed.





20201213 20:34:28 08:00



(* A valid input always terminates, either by getting to the end of the program,




or by looping and thus getting stuck. *)

20201212 22:49:52 08:00



Program Fixpoint valid_input_terminates (pc : fin (S n)) (v : set (fin n)) (acc : t) (Hnd : List.NoDup v)




{ measure (length v) }:




(exists pc', run_noswap inp (pc, v, acc) pc') :=




match valid_input_progress pc v acc with




 or_introl (conj Heq Hdone) =>




inhabited_sig_to_exists




(inhabits




(@exist (state n)




(fun x => run_noswap inp (pc, v, acc) x) (pc, v, acc) (run_noswap_ok _ _ Hdone)))




 or_intror (ex_intro _ pcs (conj Hw w)) =>




match w with




 or_introl (conj Hnin Hstuck) =>




inhabited_sig_to_exists




(inhabits




(@exist (state n)




(fun x => run_noswap inp (pc, v, acc) x) (pc, v, acc) (run_noswap_fail _ _ Hstuck)))




 or_intror (ex_intro _ pc' (ex_intro _ acc' (conj Hin Hst))) =>




match valid_input_terminates pc' (set_remove Fin.eq_dec pcs v) acc' (set_remove_nodup Fin.eq_dec pcs Hnd) with




 ex_intro _ pc'' Hrun =>




inhabited_sig_to_exists




(inhabits




(@exist (state n)




(fun x => run_noswap inp (pc, v, acc) x) pc''




(run_noswap_trans _ _ (pc', set_remove Fin.eq_dec pcs v, acc') _ Hst Hrun)))




end




end




end.




Obligation 1.




clear Heq_anonymous. clear valid_input_terminates. clear Hst.




induction v.




 inversion Hin.




 destruct (Fin.eq_dec pcs a) eqn:Heq_dec.




+ simpl. rewrite Heq_dec. lia.




+ inversion Hnd; subst.




inversion Hin. subst. exfalso. apply n0. auto.




specialize (IHv H2 H).




simpl. rewrite Heq_dec. simpl. lia.

20201212 20:08:21 08:00



Qed.

20201213 20:34:28 08:00



End ValidInput.

20201211 11:32:54 08:00



End DayEight.
