← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/workshops/2003/toma-borrione/support/sha-functions.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/workshops/2003/toma-borrione/support/sha-functions.lisp
 
1
;------------------------------------------
 
2
;
 
3
; Author:  Diana Toma
 
4
; TIMA-VDS, Grenoble, France 
 
5
; March 2003
 
6
; ACL2 formalization of SHAs
 
7
; Logic functions (and theorems) needed for all four SHA
 
8
;------------------------------------------
 
9
 
 
10
 
 
11
 
 
12
(IN-PACKAGE "ACL2")
 
13
 
 
14
(include-book "bv-op-defthms")
 
15
 
 
16
 
 
17
;logic functions for SHAs
 
18
 
 
19
(defun Ch (x y z)
 
20
  (if (and  (bvp x)
 
21
          (bvp y)
 
22
          (bvp z))
 
23
       (bv-xor (bv-and x y) (bv-and (bv-not x) z))
 
24
       nil))
 
25
 
 
26
(defthm bvp-Ch
 
27
  (implies (and  (bvp x) (bvp y) (bvp z))
 
28
         (bvp (Ch x y z)))) 
 
29
 
 
30
(defthm wordp-Ch
 
31
  (implies (and  (wordp x w) (wordp y w) (wordp z w))
 
32
         (wordp (Ch x y z) w)))
 
33
 
 
34
 
 
35
(defun Parity (x y z)
 
36
  (if (and  (bvp x)
 
37
          (bvp y)
 
38
          (bvp z))
 
39
      (bv-xor  x y z) 
 
40
       nil))
 
41
 
 
42
(defthm bvp-Parity
 
43
  (implies (and  (bvp x) (bvp y) (bvp z))
 
44
         (bvp (Parity x y z)))) 
 
45
 
 
46
(defthm wordp-Parity
 
47
  (implies (and  (wordp x w) (wordp y w) (wordp z w))
 
48
         (wordp (Parity x y z) w)))
 
49
 
 
50
(defun Maj (x y z)
 
51
  (if (and  (bvp x)
 
52
          (bvp y)
 
53
          (bvp z))
 
54
      (bv-xor  (bv-and x y) (bv-and x z) (bv-and y z))
 
55
       nil))
 
56
 
 
57
(defthm bvp-Maj
 
58
  (implies (and  (bvp x) (bvp y) (bvp z))
 
59
         (bvp (Maj x y z)))) 
 
60
 
 
61
(defthm wordp-Maj
 
62
  (implies (and  (wordp x w) (wordp y w) (wordp z w))
 
63
         (wordp (Maj x y z) w)))
 
64
           
 
65
(defun Ft (i x y z)
 
66
 (if (and (integerp i)
 
67
          (<= 0 i)
 
68
          (wordp x 32)
 
69
          (wordp y 32)
 
70
          (wordp z 32))
 
71
      (cond ((and (<= 0 i) (<= i 19)) 
 
72
            (Ch x y z))
 
73
            ((or (and (<= 20 i) (<= i 39)) (and (<= 60 i) (<= i 79)))  
 
74
            (Parity x y z))
 
75
            ((and (<= 40 i) (<= i 59)) 
 
76
            (Maj x y z)))
 
77
      nil))
 
78
 
 
79
(defthm wordp-Ft
 
80
  (implies (and (integerp i) (<= 0 i)  (wordp x 32) (<= 0 i) (< i 80)
 
81
          (wordp y 32) (wordp z 32))
 
82
         (wordp (Ft i x y z) 32))
 
83
:hints (("goal" :in-theory (disable ch parity maj) ))) 
 
84
           
 
85
(defun sigma-0-256 (x)
 
86
     (if  (wordp x 32)
 
87
          (bv-xor  (rotr 2 x 32) (rotr 13 x 32) (rotr 22 x 32))
 
88
          nil))
 
89
 
 
90
 
 
91
(defthm wordp-sigma-0-256
 
92
(implies (wordp x 32)
 
93
   ( wordp  (sigma-0-256 x) 32))
 
94
:hints (("goal" :in-theory (disable binary-bv-xor rotr rotr->rotl  ))))
 
95
 
 
96
(defun sigma-1-256 (x)
 
97
     (if  (wordp x 32)
 
98
          (bv-xor (rotr 6 x 32) (rotr 11 x 32) (rotr 25 x 32))
 
99
          nil))
 
100
 
 
101
(defthm wordp-sigma-1-256
 
102
(implies (wordp x 32)
 
103
   ( wordp  (sigma-1-256 x) 32))
 
104
:hints (("goal" :in-theory (disable binary-bv-xor rotr rotr->rotl  ))))
 
105
 
 
106
(defun s-0-256 (x)
 
107
     (if  (wordp x 32)
 
108
          (bv-xor (rotr 7 x 32) (rotr 18 x 32) (shr 3 x 32))
 
109
          nil))
 
110
 
 
111
(defthm wordp-s-0-256
 
112
(implies (wordp x 32)
 
113
   ( wordp  (s-0-256 x) 32))
 
114
:hints (("goal" :in-theory (disable binary-bv-xor rotr rotr->rotl shr  ))))
 
115
 
 
116
(defun s-1-256 (x)
 
117
     (if  (wordp x 32)
 
118
          (bv-xor  (rotr 17 x 32) (rotr 19 x 32) (shr 10 x 32))
 
119
          nil))
 
120
 
 
121
(defthm wordp-s-1-256
 
122
(implies (wordp x 32)
 
123
   ( wordp  (s-1-256 x) 32))
 
124
:hints (("goal" :in-theory (disable binary-bv-xor rotr rotr->rotl shr  ))))
 
125
 
 
126
(defun sigma-0-512 (x)
 
127
     (if  (wordp x 64)
 
128
          (bv-xor  (rotr 28 x 64) (rotr 34 x 64) (rotr 39 x 64))
 
129
          nil))
 
130
 
 
131
(defthm wordp-sigma-0-512
 
132
(implies (wordp x 64)
 
133
   ( wordp  (sigma-0-512 x) 64))
 
134
:hints (("goal" :in-theory (disable binary-bv-xor rotr rotr->rotl  ))))
 
135
 
 
136
(defun sigma-1-512 (x)
 
137
     (if  (wordp x 64)
 
138
          (bv-xor  (rotr 14 x 64) (rotr 18 x 64) (rotr 41 x 64))
 
139
          nil))
 
140
 
 
141
(defthm wordp-sigma-1-512
 
142
(implies (wordp x 64)
 
143
   ( wordp  (sigma-1-512 x) 64))
 
144
:hints (("goal" :in-theory (disable binary-bv-xor rotr rotr->rotl  ))))
 
145
 
 
146
(defun s-0-512 (x)
 
147
     (if  (wordp x 64)
 
148
          (bv-xor  (rotr 1 x 64) (rotr 8 x 64) (shr 7 x 64))
 
149
          nil))
 
150
 
 
151
(defthm wordp-s-0-512
 
152
(implies (wordp x 64)
 
153
   ( wordp  (s-0-512 x) 64))
 
154
:hints (("goal" :in-theory (disable binary-bv-xor rotr rotr->rotl shr  ))))
 
155
 
 
156
(defun s-1-512 (x)
 
157
     (if  (wordp x 64)
 
158
          (bv-xor  (rotr 19 x 64) (rotr 61 x 64) (shr 6 x 64))
 
159
          nil))
 
160
 
 
161
(defthm wordp-s-1-512
 
162
(implies (wordp x 64)
 
163
   ( wordp  (s-1-512 x) 64))
 
164
:hints (("goal" :in-theory (disable binary-bv-xor rotr rotr->rotl shr  ))))