Moved induction proof to auto-run nightly

Author: pavpanchekha

.gitignore

@@ -8,7 +8,9 @@ bench/joel
 bench/pages/
 bench/fwt.rkt
 bench/bugs.rkt
+bench/induction.rkt
 geckodriver.log
+cache
 previous/
 
 # Racket and TypeScript junk

Makefile

@@ -103,3 +103,6 @@ bench/induction.rkt: capture/capture.py capture/all.js bench/induction/list.html
 		'bench/induction/list.html#2' 'bench/induction/list.html#3' \
 		'bench/induction/list.html#4' 'bench/induction/list.html#5' \
 		'bench/induction/list.html#50'
+
+reports/induction.html reports/induction.json: bench/induction.proof
+	racket src/report.rkt proofs $(FLAGS) --show-all --cache reports/induction.cache --timeout 600 -o reports/induction $^

bench/button_test_stress/button_test_stress.html

@@ -0,0 +1,81 @@
+;; -*- mode: scheme -*-
+;; A Proof to verify the functionality of a simple website that uses java script
+;; By Skyler Griffith
+
+(import "common.thm")
+
+(page press-0 (load "induction.rkt" doc-1)
+      :w (between 800 1920)
+      :h (between 600 1280)
+      :fs (between 16 32))
+ 
+(page press-1 (load "induction.rkt" doc-2)
+      :w (between 800 1920)
+      :h (between 600 1280)
+      :fs (between 16 32))
+ 
+(page press-2 (load "induction.rkt" doc-3)
+      :w (between 800 1920)
+      :h (between 600 1280)
+      :fs (between 16 32))
+ 
+(page press-3 (load "induction.rkt" doc-4)
+      :w (between 800 1920)
+      :h (between 600 1280)
+      :fs (between 16 32))
+ 
+(page press-4 (load "induction.rkt" doc-5)
+      :w (between 800 1920)
+      :h (between 600 1280)
+      :fs (between 16 32))
+ 
+(page press-5 (load "induction.rkt" doc-6)
+      :w (between 800 1920)
+      :h (between 600 1280)
+      :fs (between 16 32))
+ 
+(page press-50 (load "induction.rkt" doc-7)
+      :w (between 800 1920)
+      :h (between 600 1280)
+      :fs (between 16 32))
+ 
+(theorem (top-above-bottom b)
+  (>= (- (bottom b) (top b) 0)))
+
+(proof (top-above-bottom top-above-bottom press-0 press-1 press-2 press-3 press-4 press-5)
+  (component list (id list))
+  (component button (tag button))
+  (components todos (child (id list) *))
+
+  (erase todos :text)
+  (assert todos (and (> (height ?) 0) (float-flow-skip ?) (non-negative-margins ?)))
+  (pre list (= (floats-tracked ?) 0))
+  (induct list ; the inductive fact
+  	(and (>= (- (bottom inductive-footer) (top inductive-header)) 0) (= (floats-tracked inductive-footer) (floats-tracked inductive-header))))
+  (assert list (forall () (>= (- (bottom (last list)) (top (first list)) 0)))))
+
+(proof (stress-test top-above-bottom press-50)
+  (component list (id list))
+  (component button (tag button))
+  (components todos (child (id list) *))
+
+  (erase todos :text)
+  (assert todos (and (> (height ?) 0) (float-flow-skip ?) (non-negative-margins ?)))
+  (pre list (= (floats-tracked ?) 0))
+  (induct list ; the inductive fact
+  	(and (>= (- (bottom inductive-footer) (top inductive-header)) 0) (= (floats-tracked inductive-footer) (floats-tracked inductive-header))))
+  (assert list (forall () (>= (- (bottom (last list)) (top (first list)) 0)))))
+
+(proof (interactive-onscreen interactive-onscreen press-0 press-1 press-2 press-3)
+  (component list (id list))
+  (component button (tag button))
+  (components todos (child (id list) *))
+  (erase todos :text)
+  (assert list 
+    (=> (or (= (prev list) null)
+            (non-negative-margins (prev list)))
+        (non-negative-margins list)))
+  (assert * (forall (b) (=> (onscreen ?)
+  		            (=> (or (is-component b) (is-interactive b)) (onscreen b)))))
+  (assert (- * list) (forall (t) (=> (has-type t text) (> (width t) 0) (non-negative-margins ?))))
+  (assert root (onscreen root)))