File: stobj-find-n-free-clusters.lisp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
  • links: PTS
  • area: main
  • in suites: trixie
  • size: 1,111,420 kB
  • sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (157 lines) | stat: -rw-r--r-- 4,855 bytes parent folder | download | duplicates (3)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
(in-package "ACL2")

;  stobj-find-n-free-clusters.lisp                      Mihir Mehta

(include-book "update-data-region")

(defund-nx
  effective-fat (fat32$c)
  (declare
   (xargs :stobjs fat32$c
          :guard (lofat-fs-p fat32$c)
          :guard-hints
          (("goal" :in-theory (enable fat32$c-p)))))
  (take (+ (count-of-clusters fat32$c)
           *ms-first-data-cluster*)
        (nth *fati* fat32$c)))

(defthm len-of-effective-fat
  (equal (len (effective-fat fat32$c))
         (nfix (+ (count-of-clusters fat32$c)
                  *ms-first-data-cluster*)))
  :hints (("goal" :in-theory (enable effective-fat))))

(defthm
  fat32-entry-list-p-of-effective-fat
  (implies (and (fat32$c-p fat32$c)
                (<= (+ (count-of-clusters fat32$c)
                       *ms-first-data-cluster*)
                    (fat-length fat32$c)))
           (fat32-entry-list-p (effective-fat fat32$c)))
  :hints
  (("goal" :in-theory (enable effective-fat
                              fat-length fat32$c-p)))
  :rule-classes
  ((:rewrite
    :corollary
    (implies (lofat-fs-p fat32$c)
             (fat32-entry-list-p (effective-fat fat32$c))))))

(defthm
  nth-of-effective-fat
  (equal (nth n (effective-fat fat32$c))
         (if (< (nfix n)
                (nfix (+ (count-of-clusters fat32$c)
                         *ms-first-data-cluster*)))
             (fati n fat32$c)
           nil))
  :hints (("goal" :in-theory (enable fati effective-fat nth))))

(defthm
  effective-fat-of-update-data-regioni
  (equal
   (effective-fat (update-data-regioni i v fat32$c))
   (effective-fat fat32$c))
  :hints (("goal" :in-theory (enable effective-fat))))

(defthm
  effective-fat-of-update-fati
  (equal (effective-fat (update-fati i v fat32$c))
         (if (< (nfix i)
                (+ (count-of-clusters fat32$c)
                   *ms-first-data-cluster*))
             (update-nth i v (effective-fat fat32$c))
           (effective-fat fat32$c)))
  :hints (("goal" :in-theory (enable effective-fat update-fati))))

(defund
  stobj-find-n-free-clusters-helper
  (fat32$c n start)
  (declare
   (xargs
    :guard (and (lofat-fs-p fat32$c)
                (natp n)
                (natp start))
    :stobjs fat32$c
    :measure (nfix (- (+ (count-of-clusters fat32$c)
                         *ms-first-data-cluster*)
                      start))))
  (if
      (or (zp n)
          (mbe :logic (zp (- (+ (count-of-clusters fat32$c)
                                *ms-first-data-cluster*)
                             start))
               :exec (>= start
                         (+ (count-of-clusters fat32$c)
                            *ms-first-data-cluster*))))
      nil
    (if
        (not (equal (fat32-entry-mask (fati start fat32$c))
                    0))
        (stobj-find-n-free-clusters-helper
         fat32$c n (+ start 1))
      (cons
       (mbe :exec start :logic (nfix start))
       (stobj-find-n-free-clusters-helper fat32$c (- n 1)
                                          (+ start 1))))))

(defthm
  nat-listp-of-stobj-find-n-free-clusters-helper
  (nat-listp
   (stobj-find-n-free-clusters-helper fat32$c n start))
  :hints
  (("goal"
    :in-theory (enable stobj-find-n-free-clusters-helper)))
  :rule-classes
  (:rewrite
   (:rewrite
    :corollary (integer-listp (stobj-find-n-free-clusters-helper
                               fat32$c n start)))))

(defthm
  stobj-find-n-free-clusters-helper-correctness-1
  (implies
   (and (natp start)
        (lofat-fs-p fat32$c))
   (equal
    (stobj-find-n-free-clusters-helper fat32$c n start)
    (find-n-free-clusters-helper
     (nthcdr start (effective-fat fat32$c))
     n start)))
  :hints
  (("goal" :in-theory (enable stobj-find-n-free-clusters-helper
                              find-n-free-clusters-helper)
    :induct (stobj-find-n-free-clusters-helper
             fat32$c n start))))

(defund
  stobj-find-n-free-clusters
  (fat32$c n)
  (declare
   (xargs :guard (and (lofat-fs-p fat32$c)
                      (natp n))
          :stobjs fat32$c))
  (stobj-find-n-free-clusters-helper
   fat32$c n *ms-first-data-cluster*))

(defthm
  nat-listp-of-stobj-find-n-free-clusters
  (nat-listp (stobj-find-n-free-clusters fat32$c n))
  :hints
  (("goal" :in-theory (enable stobj-find-n-free-clusters)))
  :rule-classes
  (:rewrite
   (:rewrite
    :corollary (integer-listp (stobj-find-n-free-clusters-helper
                               fat32$c n start)))))

(defthm
  stobj-find-n-free-clusters-correctness-1
  (implies
   (lofat-fs-p fat32$c)
   (equal (stobj-find-n-free-clusters fat32$c n)
          (find-n-free-clusters (effective-fat fat32$c)
                                n)))
  :hints (("goal" :in-theory (enable stobj-find-n-free-clusters
                                     find-n-free-clusters)))
  :rule-classes :definition)