Skip to content

MITMWFAR_verifier #3

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

MITMWFAR_verifier #3

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 42 additions & 0 deletions verify/CTL.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
From BusyCoq Require Export Permute.

Module CTL (Ctx : Ctx).
Module Permute := Permute Ctx. Export Permute.

Definition Language :Type := Q * tape -> Prop.

Definition closed (L : Language) (tm : TM) :=
forall c c',
c -[ tm ]-> c' ->
L c ->
L c'.

Definition non_halt (L : Language) (tm : TM) :=
forall c,
L c ->
~halted tm c.

Lemma closed_tape_language_nonhalt:
forall (L : Language) (tm: TM) (c: Q*tape),
closed L tm ->
non_halt L tm ->
L c ->
~ halts tm c.
Proof.
introv HClosed HNonhalt HStart.
apply progress_nonhalt with (P:=L).
- introv Hc1.
unfold non_halt in HNonhalt.
pose proof Hc1 as Hnext.
apply HNonhalt in Hnext.
apply no_halted_step in Hnext.
destruct Hnext as [c2 HStep].
exists c2.
split.
+ unfold closed in HClosed.
apply HClosed with (c := c1). assumption. assumption.
+ apply progress_intro with (c' := c2). assumption. apply evstep_refl.
- assumption.
Qed.

End CTL.
4 changes: 2 additions & 2 deletions verify/Individual.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,11 @@

From Coq Require Export Lists.Streams.
From Coq Require Import Lia.
From BusyCoq Require Export Permute.
From BusyCoq Require Export WNFA.
Set Default Goal Selector "!".

Module Individual (Ctx : Ctx).
Module Permute := Permute Ctx. Export Permute.
Module WNFA := WNFA Ctx. Export WNFA.

(** Trivial lemmas, but [simpl] in these situations leaves a mess. *)
Lemma move_left_const : forall s0 s r,
Expand Down
73 changes: 73 additions & 0 deletions verify/MITMWFAR_Test.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
From Coq Require Import Lists.List.
From Coq Require Import ZArith.
From BusyCoq Require Import Individual52 Finned.
Set Default Goal Selector "!".

Definition tm : TM := fun '(q, s) =>
match q, s with
| A, 0 => Some (1, R, B) | A, 1 => None
| B, 0 => Some (0, R, C) | B, 1 => Some (1, L, B)
| C, 0 => Some (1, R, D) | C, 1 => Some (1, R, C)
| D, 0 => Some (1, L, E) | D, 1 => Some (1, L, D)
| E, 0 => Some (0, R, A) | E, 1 => Some (0, L, E)
end.
Close Scope sym.

Definition lwfa : WNFA := [(0%nat, 0%nat, 0%sym, 0%Z);
(1%nat, 1%nat, 0%sym, 0%Z);
(1%nat, 1%nat, 1%sym, 0%Z);
(2%nat, 2%nat, 1%sym, 0%Z);
(2%nat, 3%nat, 0%sym, 1%Z);
(3%nat, 1%nat, 0%sym, 0%Z);
(3%nat, 2%nat, 1%sym, 0%Z);
(0%nat, 2%nat, 1%sym, 0%Z)].

Definition rwfa : WNFA := [(1%nat, 1%nat, 0%sym, 0%Z);
(1%nat, 1%nat, 1%sym, 0%Z);
(2%nat, 0%nat, 0%sym, (-1)%Z);
(2%nat, 2%nat, 1%sym, 0%Z);
(0%nat, 0%nat, 0%sym, 0%Z);
(0%nat, 2%nat, 1%sym, 0%Z)].

Open Scope nat.
Definition lnn : list nat := [0;1;2;3].
Definition lnp : list nat := [0].
Definition rnn : list nat := [1].
Definition rnp : list nat := [0;1;2].
Close Scope nat.

Definition aset : list AcceptTuple := [(A, 0%sym, 0%nat, 0%nat, Some 0%Z, Some 0%Z);
(D, 0%sym, 2%nat, 0%nat, Some 1%Z, None);
(B, 1%sym, 3%nat, 2%nat, Some 1%Z, None);
(B, 1%sym, 2%nat, 2%nat, Some 1%Z, None);
(C, 0%sym, 3%nat, 0%nat, Some 1%Z, None);
(C, 1%sym, 2%nat, 2%nat, Some 1%Z, None);
(E, 1%sym, 0%nat, 0%nat, Some 0%Z, Some 0%Z);
(E, 0%sym, 0%nat, 0%nat, Some 0%Z, Some 0%Z);
(B, 1%sym, 2%nat, 0%nat, Some 1%Z, None);
(C, 0%sym, 2%nat, 2%nat, Some 2%Z, None);
(C, 1%sym, 2%nat, 0%nat, Some 1%Z, None);
(E, 1%sym, 2%nat, 0%nat, Some 0%Z, None);
(D, 1%sym, 3%nat, 2%nat, Some 2%Z, None);
(A, 0%sym, 3%nat, 2%nat, Some 1%Z, None);
(B, 0%sym, 2%nat, 0%nat, Some 0%Z, None);
(C, 1%sym, 3%nat, 0%nat, Some 1%Z, None);
(C, 1%sym, 3%nat, 2%nat, Some 1%Z, None);
(D, 1%sym, 2%nat, 0%nat, Some 2%Z, None);
(E, 1%sym, 2%nat, 2%nat, Some 1%Z, None);
(C, 0%sym, 3%nat, 2%nat, Some 2%Z, None);
(D, 1%sym, 2%nat, 2%nat, Some 2%Z, None);
(C, 0%sym, 2%nat, 0%nat, Some 1%Z, None);
(E, 0%sym, 2%nat, 0%nat, Some (-1)%Z, None);
(B, 0%sym, 2%nat, 2%nat, Some 0%Z, None);
(D, 0%sym, 2%nat, 2%nat, Some 1%Z, None);
(E, 1%sym, 3%nat, 2%nat, Some 1%Z, None);
(E, 1%sym, 3%nat, 0%nat, Some 0%Z, None);
(A, 0%sym, 3%nat, 0%nat, Some 0%Z, None)].

Definition certData := (lwfa, rwfa, lnn, lnp, rnn, rnp, aset).

Theorem nonhalt : ~ halts tm c0.
Proof.
apply check_MITMWFA_cert_correct with certData. reflexivity.
Qed.
2 changes: 1 addition & 1 deletion verify/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ ALLVFILES := LibTactics.v Helper.v Pigeonhole.v TM.v Compute.v Flip.v Permute.v
Cyclers.v TranslatedCyclers.v BackwardsReasoning.v Bouncers.v Individual.v \
BB52.v Individual52.v FixedBin.v ShiftOverflow.v ShiftOverflowBins.v Skelet15.v Skelet26.v Skelet33.v Skelet34.v Skelet35.v \
Skelet10.v Skelet17.v Skelet1.v Finned.v Finned1.v Finned2.v Finned3.v Finned4.v Finned5.v Extraction.v \
BB33.v Individual33.v
BB33.v Individual33.v CTL.v WNFA.v MITMWFAR_Test.v

all: check verify skelet1

Expand Down
Loading