Allen categorized and split these up into files.

Author: calebegg

.DS_Store

@@ -0,0 +1,11 @@
+(in-package "ACL2")
+(include-book "basiclex-defs")
+(include-book "split-blocks-concat-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty append-pseudoinverts-splitoff-prefix-1
+  (ps :value (random-list-of (random-integer))
+   xs :value (random-list-of (random-integer)))
+  (equal (append (car (splitoff-prefix ps xs)) 
+                 (caddr (splitoff-prefix ps xs)))
+         xs))

Basiclex/.DS_Store

@@ -0,0 +1,12 @@
+(in-package "ACL2")
+(include-book "basiclex-defs")
+(include-book "split-blocks-concat-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty append-pseudoinverts-splitoff-prefix-2
+  (ps :value (random-list-of (random-integer))
+   xs :value (random-list-of (random-integer)))
+  (equal (append (car (splitoff-prefix ps xs)) 
+                 (cadr (splitoff-prefix ps xs)))
+         ps))
+  

Basiclex/append-psudeoinverts-splitoff-prefix-1.lisp

@@ -1,60 +1,60 @@
-(in-package "ACL2")
-
-; ds = list of delimiters (no constraints on what a delimiter is)
-; xs = list of values (no constraints on values)
-; (split-at-delimiter ds xs) = list of two elements
-;   1 longest prefix of xs containing no elements from ds
-;   2 rest of xs
-(defun split-at-delimiter (ds xs)
-  (if (or (endp xs) (member-equal (car xs) ds))
-      (list nil xs)
-      (let* ((cdr-split (split-at-delimiter ds (cdr xs))))
-        (list (cons (car xs) (car cdr-split))
-              (cadr cdr-split)))))
-
-; ps = list of signals to pass by (no constraints on signals)
-; xs = list of signals (no constraints on signals)
-; (span ps xs) = list of two elements
-;  1 longest prefix of xs containing only signals from ps
-;  2 rest of xs
-(defun span (ps xs)
-  (if (or (endp xs) (not (member-equal (car xs) ps)))
-      (list nil xs)
-      (let* ((cdr-span (span ps (cdr xs))))
-        (list (cons (car xs) (car cdr-span))
-              (cadr cdr-span)))))
-
-; ps = list of values (no constraints on values)
-; xs = list of values (no constraints on values)
-; (splitoff-prefix ps xs) = list of three elements
-;  1 longest prefix of ps that is also a prefix of xs
-;  2 rest of ps
-;  3 rest of xs beyond prefix that matches element 1
-(defun splitoff-prefix (ps xs)
-  (if (or (endp ps)
-          (endp xs)
-          (not (equal (car xs) (car ps))))
-      (list nil ps xs)
-      (let* ((3way (splitoff-prefix (cdr ps) (cdr xs))))
-        (list (cons (car ps) (car 3way))
-              (cadr 3way)
-              (caddr 3way)))))
-
-; tok = token (list of values, no constraints on values)
-; xs = list of values (no constraints on values)
-; (split-on-token tok xs) = list of three elements
-;  1 prefix of xs: portion before 1st contiguous sublist matching tok
-;                  (or xs, if there is no match for tok in xs)
-;  2 tok if tok matches a contiguous sublist of xs, otherwise nil
-;  3 suffix of xs: portion after 1st contiguous sublist matching tok
-;                  (or nil, if there is no match for tok in xs)
-(defun split-on-token (tok xs)
-  (if (endp xs)
-      (list nil nil nil)
-      (let* ((3way (splitoff-prefix tok xs)))
-        (if (endp (cadr 3way))
-            (list nil tok (caddr 3way))
-            (let* ((cdr-split (split-on-token tok (cdr xs))))
-              (list (cons (car xs) (car cdr-split))
-                    (cadr cdr-split)
-                    (caddr cdr-split)))))))
+(in-package "ACL2")
+
+; ds = list of delimiters (no constraints on what a delimiter is)
+; xs = list of values (no constraints on values)
+; (split-at-delimiter ds xs) = list of two elements
+;   1 longest prefix of xs containing no elements from ds
+;   2 rest of xs
+(defun split-at-delimiter (ds xs)
+  (if (or (endp xs) (member-equal (car xs) ds))
+      (list nil xs)
+      (let* ((cdr-split (split-at-delimiter ds (cdr xs))))
+        (list (cons (car xs) (car cdr-split))
+              (cadr cdr-split)))))
+
+; ps = list of signals to pass by (no constraints on signals)
+; xs = list of signals (no constraints on signals)
+; (span ps xs) = list of two elements
+;  1 longest prefix of xs containing only signals from ps
+;  2 rest of xs
+(defun span (ps xs)
+  (if (or (endp xs) (not (member-equal (car xs) ps)))
+      (list nil xs)
+      (let* ((cdr-span (span ps (cdr xs))))
+        (list (cons (car xs) (car cdr-span))
+              (cadr cdr-span)))))
+
+; ps = list of values (no constraints on values)
+; xs = list of values (no constraints on values)
+; (splitoff-prefix ps xs) = list of three elements
+;  1 longest prefix of ps that is also a prefix of xs
+;  2 rest of ps
+;  3 rest of xs beyond prefix that matches element 1
+(defun splitoff-prefix (ps xs)
+  (if (or (endp ps)
+          (endp xs)
+          (not (equal (car xs) (car ps))))
+      (list nil ps xs)
+      (let* ((3way (splitoff-prefix (cdr ps) (cdr xs))))
+        (list (cons (car ps) (car 3way))
+              (cadr 3way)
+              (caddr 3way)))))
+
+; tok = token (list of values, no constraints on values)
+; xs = list of values (no constraints on values)
+; (split-on-token tok xs) = list of three elements
+;  1 prefix of xs: portion before 1st contiguous sublist matching tok
+;                  (or xs, if there is no match for tok in xs)
+;  2 tok if tok matches a contiguous sublist of xs, otherwise nil
+;  3 suffix of xs: portion after 1st contiguous sublist matching tok
+;                  (or nil, if there is no match for tok in xs)
+(defun split-on-token (tok xs)
+  (if (endp xs)
+      (list nil nil nil)
+      (let* ((3way (splitoff-prefix tok xs)))
+        (if (endp (cadr 3way))
+            (list nil tok (caddr 3way))
+            (let* ((cdr-split (split-on-token tok (cdr xs))))
+              (list (cons (car xs) (car cdr-split))
+                    (cadr cdr-split)
+                    (caddr cdr-split)))))))

Basiclex/append-psudeoinverts-splitoff-prefix-2.lisp

@@ -0,0 +1,13 @@
+(in-package "ACL2")
+(include-book "basiclex-defs")
+(include-book "split-blocks-concat-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty split-at-delim-conserves-vals
+  (ds :value (random-list-of (random-integer))
+   xs :value (random-list-of (random-integer)))
+  (let* ((pair (split-at-delimiter ds xs))
+         (pfx (car pair))
+         (sfx (cadr pair)))
+    (equal (append pfx sfx)
+           xs)))

SE Definitions and Theorems/Not Working/basiclex.lisp Basiclex/basiclex-defs.lisp

@@ -0,0 +1,11 @@
+(in-package "ACL2")
+(include-book "basiclex-defs")
+(include-book "split-blocks-concat-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty split-at-delim-delivers-no-delims-in-prefix
+  (ds :value (random-list-of (random-between 0 10))
+   xs :value (random-list-of (random-between 0 10))
+   x  :value (random-between 0 10)
+      :where (member-equal x (car (split-at-delimiter ds xs))))
+  (not (member-equal x ds)))

Basiclex/split-at-delim-conserves-vals.lisp

@@ -0,0 +1,10 @@
+(in-package "ACL2")
+(include-book "basiclex-defs")
+(include-book "split-blocks-concat-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty split-at-delim-delivers-suffix-that-starts-with-delim
+  (ds :value (random-list-of (random-between 0 10))
+   xs :value (random-list-of (random-between 0 10))
+      :where (consp (cadr (split-at-delimiter ds xs))))
+  (member-equal (car (cadr (split-at-delimiter ds xs))) ds))

Basiclex/split-at-delim-delivers-no-delims-in-prefix.lisp

@@ -1,47 +1,47 @@
-; Definitions specify axiomatic properties
-(in-package "ACL2") ; form importable "book"
-
-;(defun split (n xs)
-;  (if (and (posp n) (consp xs))
-;      (list (cons (car xs)
-;                  (car (split (- n 1) (cdr xs))))
-;            (cadr (split (- n 1) (cdr xs))))
-;      (list nil xs)))
-;(defun insert-first (x xsys)
-;  (list (cons x (car xsys))
-;        (cadr xsys)))
-;(defun split (n xs)
-;  (if (and (posp n) (consp xs))
-;      (insert-first (car xs) 
-;                    (split (- n 1) (cdr xs)))
-;      (list nil xs)))
-(defun split (n xs)
-  (if (and (posp n) (consp xs))
-      (let* ((x  (car xs))
-             (s  (split (- n 1) (cdr xs)))
-             (fr (car s))
-             (bk (cadr s)))
-        (list (cons x fr) bk))
-      (list nil xs)))
-(defun firstN (n xs)
-  (car (split n xs)))
-(defun concat (xss)
-  (if (consp xss)
-      (append (car xss) (concat (cdr xss)))
-      xss))
-(defun total-len (xss)
-  (if (consp xss)
-      (+ (len (car xss)) (total-len (cdr xss)))
-      0))
-(defun member-one+ (x xss)
-  (if (consp xss)
-      (or (member-equal x (car xss))
-          (member-one+ x (cdr xss)))
-      nil))
-(defun blocks (n xs)
-  (if (and (posp n) (consp xs))
-      (let* ((s  (split n xs))
-             (fr (car s))
-             (bk (cadr s)))
-        (cons fr (blocks n bk)))
-      nil))
+; Definitions specify axiomatic properties
+(in-package "ACL2") ; form importable "book"
+
+;(defun split (n xs)
+;  (if (and (posp n) (consp xs))
+;      (list (cons (car xs)
+;                  (car (split (- n 1) (cdr xs))))
+;            (cadr (split (- n 1) (cdr xs))))
+;      (list nil xs)))
+;(defun insert-first (x xsys)
+;  (list (cons x (car xsys))
+;        (cadr xsys)))
+;(defun split (n xs)
+;  (if (and (posp n) (consp xs))
+;      (insert-first (car xs) 
+;                    (split (- n 1) (cdr xs)))
+;      (list nil xs)))
+(defun split (n xs)
+  (if (and (posp n) (consp xs))
+      (let* ((x  (car xs))
+             (s  (split (- n 1) (cdr xs)))
+             (fr (car s))
+             (bk (cadr s)))
+        (list (cons x fr) bk))
+      (list nil xs)))
+(defun firstN (n xs)
+  (car (split n xs)))
+(defun concat (xss)
+  (if (consp xss)
+      (append (car xss) (concat (cdr xss)))
+      xss))
+(defun total-len (xss)
+  (if (consp xss)
+      (+ (len (car xss)) (total-len (cdr xss)))
+      0))
+(defun member-one+ (x xss)
+  (if (consp xss)
+      (or (member-equal x (car xss))
+          (member-one+ x (cdr xss)))
+      nil))
+(defun blocks (n xs)
+  (if (and (posp n) (consp xs))
+      (let* ((s  (split n xs))
+             (fr (car s))
+             (bk (cadr s)))
+        (cons fr (blocks n bk)))
+      nil))

Basiclex/split-at-delim-delivers-suffix-that-starts-with-delim.lisp

@@ -0,0 +1,7 @@
+(include-book "cryptography-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty codevis->plainvis-inverts-plainvis->codevis
+  (vals :value (random-list-of (random-between 0 94))
+        :where (and (viscode-listp vals) (consp vals)))
+  (equal (codevis->plainvis (plainvis->codevis vals)) vals))

SE Definitions and Theorems/Not Working/split-blocks-concat-defs.lisp Basiclex/split-blocks-concat-defs.lisp

@@ -0,0 +1,43 @@
+;;;All the theorems in this file have been proven - ARS 04/11/12;;;;;;;;;;;
+(IN-PACKAGE "ACL2")
+(include-book "linear-encoding-defs")
+(include-book "doublecheck" :dir :teachpacks)
+(include-book "list-utilities" :dir :teachpacks)
+
+(defun codes->chrs (codes)
+   (if (endp codes)
+       nil
+       (cons (code-char (car codes)) (codes->chrs (cdr codes)))))
+
+(defun visibilize-txt (chrs)
+  (if (consp chrs)
+      (if (and (>= (char-code (car chrs)) 32)
+               (<= (char-code (car chrs)) 126))
+          (cons (car chrs) (visibilize-txt (cdr chrs)))
+          (cons #\Space (visibilize-txt (cdr chrs))))
+      nil))
+
+(defun txt->vis (chrs)
+  (if (consp chrs)
+      (cons (- (char-code (car chrs)) 32) (txt->vis (cdr chrs)))
+      nil))
+
+(defun vis->txt (viscs)
+  (if (consp viscs)
+      (cons (code-char (+ 32 (car viscs))) (vis->txt (cdr viscs)))
+      nil))
+
+(defun plainvis->codevis (viscs)
+  (encode 95 viscs))
+
+(defun codevis->plainvis (viscs)
+  (decode 95 viscs))
+
+(defun visible-txt-listp (chrs)
+  (or (endp chrs)
+      (and (>= (char-code (car chrs)) 32)
+           (<= (char-code (car chrs)) 126)
+           (visible-txt-listp (cdr chrs)))))
+
+(defun viscode-listp (vals)
+  (code-listp 95 vals))

Cryptography/.DS_Store

@@ -0,0 +1,25 @@
+(IN-PACKAGE "ACL2")
+(include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)
+
+(defun encode (m xs)
+  (if (consp (cdr xs))
+      (cons (mod (+ (car xs) (cadr xs)) m) (encode m (cdr xs)))
+      (list (mod (+ (car xs) (1- m)) m))))
+
+(defun decode (m ys)
+  (if (consp (cdr ys))
+      (let* ((cdr-xs (decode m (cdr ys)))
+             (car-xs (mod (- (car ys) (car cdr-xs)) m)))
+        (cons car-xs cdr-xs))
+      (list (mod (- (car ys) (1- m)) m))))
+
+(defun basep (m)
+  (and (natp m) (>= m 2)))
+
+(defun codep (m x)
+  (and (natp x) (> m x)))
+
+(defun code-listp (m xs)
+  (and (true-listp xs)
+       (or (endp xs)
+           (and (codep m (car xs)) (code-listp m (cdr xs))))))

Cryptography/codevis-plainvis-inverts-plainvis-codevis.lisp

@@ -0,0 +1,9 @@
+(include-book "cryptography-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty nth-character-is-nth-element
+  (vals :value (random-list-of (random-between 0 94))
+        :where (and (viscode-listp vals) (consp vals))
+      n :value (random-between 0 (1- (len vals)))
+        :where (and (natp n) (<= n (1- (len vals)))))
+  (equal (code-char (+ 32 (nth n vals))) (nth n (vis->txt vals))))

Cryptography/cryptography-defs.lisp

@@ -0,0 +1,10 @@
+(include-book "cryptography-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty nth-viscode-is-nth-element
+  (codes :value (random-list-of (random-between 0 255))
+    chrs :value (visibilize-txt (codes->chrs codes))
+         :where (and (visible-txt-listp chrs) (consp chrs))
+       n :value (random-between 0 (1- (len chrs)))
+         :where (and (natp n) (<= n (1- (len chrs)))))
+  (equal (- (char-code (nth n chrs)) 32) (nth n (txt->vis chrs))))

Cryptography/linear-encoding-defs.lisp

@@ -0,0 +1,8 @@
+(include-book "cryptography-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty txt->vis-delivers-list-of-viscodes
+  (codes :value (random-list-of (random-between 0 255))
+    chrs :value (visibilize-txt (codes->chrs codes))
+         :where (visible-txt-listp chrs))
+  (viscode-listp (txt->vis chrs)))

Cryptography/nth-character-is-nth-element.lisp

@@ -0,0 +1,7 @@
+(include-book "cryptography-defs")
+(include-book "doublecheck" :dir :teachpacks)
+
+(defproperty vis->txt-delivers-list-of-characters
+  (vals :value (random-list-of (random-between 0 94))
+        :where (viscode-listp vals))
+  (character-listp (vis->txt vals)))