first tests for (mm0 parser, mmu parser, mm0+mmu proof checker)

tests/README.md

@@ -0,0 +1,5 @@
+**Test files for mm0 and mmu**
+
+This folder holds various tests for MM0, MM1, MMU, and MMB.
+
+* `mm0_mmu/{pass, fail}`: Integration tests for MM0 + MMU that should pass or fail.

tests/mm0_mmu/fail/bad-id1.mm0

@@ -0,0 +1,2 @@
+--  empty id
+sort ;

tests/mm0_mmu/fail/bad-id1.mmu

@@ -0,0 +1,2 @@
+--  empty id
+(sort )

tests/mm0_mmu/fail/bad-id2.mm0

@@ -0,0 +1,3 @@
+--  blank id
+sort  
+ ;

tests/mm0_mmu/fail/bad-id2.mmu

@@ -0,0 +1,3 @@
+--  blank id
+(sort  
+ )

tests/mm0_mmu/fail/bad-id3.mm0

@@ -0,0 +1,2 @@
+--  id starting with a digit
+sort 0;

tests/mm0_mmu/fail/bad-id3.mmu

@@ -0,0 +1,2 @@
+--  id starting with a digit
+(sort 0)

tests/mm0_mmu/fail/bad-id4.mm0

@@ -0,0 +1,2 @@
+-- id with forbidden char -
+sort sot-;

tests/mm0_mmu/fail/bad-id4.mmu

@@ -0,0 +1,2 @@
+-- id with forbidden char -
+(sort sot-)

tests/mm0_mmu/fail/bad-id5.mm0

@@ -0,0 +1,2 @@
+--  id that is a single underscore _
+sort _;

tests/mm0_mmu/fail/bad-id5.mmu

@@ -0,0 +1,2 @@
+--  id that is a single underscore _
+(sort _)

tests/mm0_mmu/fail/bad-int2.mm0

@@ -0,0 +1,2 @@
+--                   V--  not an int
+prefix p : $+$ prec 1.0;

tests/mm0_mmu/fail/bad-int3.mm0

@@ -0,0 +1,2 @@
+--                  V--  forbidden sign
+prefix p : $+$ prec +1;

tests/mm0_mmu/fail/bad-int4.mm0

@@ -0,0 +1,2 @@
+--                      V--  forbidden sign
+prefix plus: $ + $ prec -1;

tests/mm0_mmu/fail/bad-int5.mm0

@@ -0,0 +1,2 @@
+--                  V--  forbidden 0 prefix -
+prefix p : $+$ prec 01;

tests/mm0_mmu/fail/bad-math-string1.mm0

@@ -0,0 +1,2 @@
+--         --V one $ too many
+delimiter $ $ $;

tests/mm0_mmu/fail/bad-math-string2.mm0

@@ -0,0 +1,2 @@
+--         --V one $ too many
+delimiter $ $ $  $  $ ;

tests/mm0_mmu/fail/bad-math-string3.mm0

@@ -0,0 +1,2 @@
+--               --V two $ too many
+delimiter $ $ $ $ $ $ ;

tests/mm0_mmu/fail/bad-sort21.mm0

@@ -0,0 +1,2 @@
+-- strict should be after pure
+strict pure sort s21;

tests/mm0_mmu/fail/bad-sort21.mmu

@@ -0,0 +1,2 @@
+-- strict should be after pure
+(sort s21 strict pure)

tests/mm0_mmu/fail/bad-sort31.mm0

@@ -0,0 +1,2 @@
+-- provable should be after pure
+provable pure sort s31;

tests/mm0_mmu/fail/bad-sort31.mmu

@@ -0,0 +1,2 @@
+-- provable should be after pure
+(sort s31 provable pure)

tests/mm0_mmu/fail/bad-sort32.mm0

@@ -0,0 +1,2 @@
+-- provable should be after strict
+provable strict sort s32;

tests/mm0_mmu/fail/bad-sort32.mmu

@@ -0,0 +1,2 @@
+-- provable should be after strict
+(sort s32 provable strict)

tests/mm0_mmu/fail/bad-sort41.mm0

@@ -0,0 +1,2 @@
+-- free should be after pure
+free pure sort s41;

tests/mm0_mmu/fail/bad-sort41.mmu

@@ -0,0 +1,2 @@
+-- free should be after pure
+(sort s41 free pure)

tests/mm0_mmu/fail/bad-sort42.mm0

@@ -0,0 +1,2 @@
+-- free should be after strict
+free strict sort s42;

tests/mm0_mmu/fail/bad-sort42.mmu

@@ -0,0 +1,2 @@
+-- free should be after strict
+(sort s42 free strict)

tests/mm0_mmu/fail/bad-sort43.mm0

@@ -0,0 +1,2 @@
+-- free should be after provable
+free provable sort s43;

tests/mm0_mmu/fail/bad-sort43.mmu

@@ -0,0 +1,2 @@
+-- free should be after provable
+(sort s43 free provable)

tests/mm0_mmu/fail/bad-whitespace1.mm0

@@ -0,0 +1,2 @@
+--     v-- this is a TAB
+sort s	;

tests/mm0_mmu/fail/bad-whitespace1.mmu

@@ -0,0 +1,2 @@
+--      v-- this is a TAB
+(sort s	)

tests/mm0_mmu/fail/bad-whitespace2.mm0

@@ -0,0 +1,2 @@
+--     v-- this is a LINE TABULATION
+sort s;

tests/mm0_mmu/fail/bad-whitespace2.mmu

@@ -0,0 +1,2 @@
+--      v-- this is a LINE TABULATION
+(sort s)

tests/mm0_mmu/fail/bad-whitespace3.mm0

@@ -0,0 +1,2 @@
+--     v-- this is a FORM FEED
+sort s;

tests/mm0_mmu/fail/bad-whitespace3.mmu

@@ -0,0 +1,2 @@
+--      v-- this is a FORM FEED
+(sort s)

tests/mm0_mmu/fail/bad-whitespace4.mm0

@@ -0,0 +1,2 @@
+--     v-- this is a CARRIAGE RETURN
+sort s;

tests/mm0_mmu/fail/bad-whitespace4.mmu

@@ -0,0 +1,2 @@
+--      v-- this is a CARRIAGE RETURN
+(sort s)

tests/mm0_mmu/fail/non-ascii1.mm0

@@ -0,0 +1 @@
+sort ß;

tests/mm0_mmu/fail/non-ascii1.mmu

@@ -0,0 +1 @@
+(sort ß)

tests/mm0_mmu/fail/non-ascii2.mm0

@@ -0,0 +1,2 @@
+--    v- non-break space
+sort s ;

tests/mm0_mmu/fail/non-ascii2.mmu

@@ -0,0 +1,2 @@
+--     v- non-break space
+(sort s )

tests/mm0_mmu/pass/comment.mm0

@@ -0,0 +1,4 @@
+ --  <-- comment doesn't start the line
+sort 
+-- comment inside a statement
+s;

tests/mm0_mmu/pass/comment.mmu

@@ -0,0 +1,4 @@
+ --  <-- comment doesn't start the line
+(sort 
+-- comment inside a directive
+s)

tests/mm0_mmu/pass/id.mm0

@@ -0,0 +1,4 @@
+-- identifier ::= [a-zA-Z_][a-zA-Z0-9_]*
+sort id_1;
+sort Id2_;
+sort _id3;

tests/mm0_mmu/pass/id.mmu

@@ -0,0 +1,4 @@
+-- identifier ::= [a-zA-Z_][a-zA-Z0-9_]*
+(sort id_1)
+(sort Id2_)
+(sort _id3)

tests/mm0_mmu/pass/int.mm0

@@ -0,0 +1,6 @@
+-- int number ::= 0 | [1-9][0-9]*
+-- Verifiers should support precedences up to at least 2^11 - 2 = 2046
+prefix a: $ + $ prec 0;
+prefix b: $ * $ prec 2046;
+prefix c: $ - $ prec 1875;
+prefix d: $ / $ prec 39;

tests/mm0_mmu/pass/sort.mm0

@@ -0,0 +1,16 @@
+sort s0;
+free sort s1;
+provable sort s2;
+provable free sort s3;
+strict sort s4;
+strict free sort s5;
+strict provable sort s6;
+strict provable free sort s7;
+pure sort s8;
+pure free sort s9;
+pure provable sort s10;
+pure provable free sort s11;
+pure strict sort s12;
+pure strict free sort s13;
+pure strict provable sort s14;
+pure strict provable free sort s15;

tests/mm0_mmu/pass/sort.mmu

@@ -0,0 +1,16 @@
+(sort s0 )
+(sort s1 free )
+(sort s2 provable )
+(sort s3 provable free )
+(sort s4 strict )
+(sort s5 strict free )
+(sort s6 strict provable )
+(sort s7 strict provable free )
+(sort s8 pure )
+(sort s9 pure free )
+(sort s10 pure provable )
+(sort s11 pure provable free )
+(sort s12 pure strict )
+(sort s13 pure strict free )
+(sort s14 pure strict provable )
+(sort s15 pure strict provable free )

tests/mm0_mmu/pass/whitespace1.mm0

@@ -0,0 +1,2 @@
+--    v-- this is a SPACE
+sort s ;

tests/mm0_mmu/pass/whitespace1.mmu

@@ -0,0 +1,2 @@
+--     v-- this is a SPACE
+(sort s )

tests/mm0_mmu/pass/whitespace2.mm0

@@ -0,0 +1,3 @@
+--    v-- this is a NEWLINE '\n'
+sort s
+;

tests/mm0_mmu/pass/whitespace2.mmu

@@ -0,0 +1,3 @@
+--     v-- this is a NEWLINE '\n'
+(sort s
+)

tests/mm0_mmu/run-mm0-hs.sh

@@ -0,0 +1,5 @@
+#!/bin/sh
+
+# Usage: ./run-mm0-hs.sh pass/TEST
+#                     or fail/TEST
+mm0-hs verify $1.mm0 $1.mmu

tests/mm0_mmu/run/bad-int1.mm0

@@ -0,0 +1,2 @@
+--                      V--  overflowing hazard
+prefix p : $+$ prec 4294967296;

tests/mm0_mmu/run/math-string.mm0

@@ -0,0 +1,10 @@
+-- math-string ::= '$' [^\$]* '$'
+delimiter $  $;
+delimiter $ NUL SOH STX ETX EOT ENQ ACK BEL BS HT LF VT FF CR SO SI
+ DLE DC1 DC2 DC3 DC4 NAK SYN ETB CAN EM SUB ESC FS GS RS US
+    ! " # % & ' ( ) * + , - . /
+  0 1 2 3 4 5 6 7 8 9 : ; < = > ?
+  @ A B C D E F G H I J K L M N O
+  P Q R S T U V W X Y Z [ \ ] ^ _
+  ` a b c d e f g h i j k l m n o
+   p q r s t u v w x y z { | } ~ DEL $;