arm6-verification/correctness/multScript.sml

64   `!n rs. 2 * n <= 32 ==>
65       (BORROW2 rs n =
66        ~(n = 0) /\ (((2 * (n - 1) + 1) >< (2 * (n - 1))) rs):word2 %% 1)`,
72   `!n rs.  2 * (SUC n) <= 32 ==>
73      (MULX mla_mul tn (MULZ mla_mul tn ((31 -- (2 * SUC n)) rs))
74         (BORROW2 rs (SUC n))
75         (MSHIFT mla_mul (BORROW2 rs n)
76            ((1 >< 0) ((31 -- (2 * n)) rs)) (n2w n)) =
77       MLA_MUL_DONE rs (SUC n))`,
98   `!rs. ?n. MLA_MUL_DONE rs n`,
103   SPECL [`\x. 2 * x <= WL`,`MLA_MUL_DONE rs`]) LEAST_ELIM;
120   `!n. (!m. m < n ==> ~MLA_MUL_DONE rs m) /\
121         MLA_MUL_DONE rs n ==> 2 * n <= 32`,
137   `!rs. 2 * (MLA_MUL_DUR rs) <= 32`,
144            SPECL [`\x. ~(x = 0)`,`MLA_MUL_DONE rs`]) LEAST_ELIM;
147   `!rs. ~(MLA_MUL_DUR rs = 0)`,
154   `!rs. MLA_MUL_DONE rs (MLA_MUL_DUR rs)`,
160   `!rs n. SUC n <= MLA_MUL_DUR rs ==> ~MLA_MUL_DONE rs n`,
172   `!n x rs. ~(n = 0) ==>
173      (((x - 2) -- 0) ((x -- (2 * n)) rs) = (x -- (2 * n)) rs)`,
181   `!n rs. n <= MLA_MUL_DUR rs ==> 2 * n <= 32`,
187   `!rs n. SUC n <= MLA_MUL_DUR rs ==>
188      ((1 >< 0) ((31 -- (2 * n)) rs):word2 = ((2 * n + 1) >< (2 * n)) rs)`,
194   `!n x. (x -- 2) ((x -- (2 * (n + 1))) rs) =
195          (x -- (2 * (n + 2))) rs`,
211               (SPECL [`SUC n`,`rs`] LEQ_MLA_MUL_DUR)] o
212    DISCH `SUC n <= MLA_MUL_DUR rs` o
216   `!rs. ~MLA_MUL_DONE rs 0`,
258   SPECL [`\x. 2 * x < 32 ==> ~(BORROW2 rs x)`,`MLA_MUL_DONE rs`]) LEAST_ELIM;
261   `!n. (!m. m < n ==> ~MLA_MUL_DONE rs m) /\ MLA_MUL_DONE rs n ==>
263           ~BORROW2 rs n`,
268   `!rs. 2 * (MLA_MUL_DUR rs) < 32 ==> ~BORROW2 rs (MLA_MUL_DUR rs)`,
274   `!rs. BORROW2 rs (MLA_MUL_DUR rs) ==> (2 * (MLA_MUL_DUR rs) = 32)`,
276     \\ Cases_on `2 * (MLA_MUL_DUR rs) < 32`
278     \\ ASSUME_TAC (SPEC `rs` DUR_LT_EQ_HWL)
282   SPECL [`\x. w2n rs MOD 2 ** (2 * x) = w2n rs`,`MLA_MUL_DONE rs`]) LEAST_ELIM;
285   `!n. (!m. m < n ==> ~MLA_MUL_DONE rs m) /\ MLA_MUL_DONE rs n ==>
286         (w2n rs MOD 2 ** (2 * n) = w2n rs)`,
287   Cases_on `rs`
319   `!rs. w2n rs MOD 2 ** (2 * (MLA_MUL_DUR rs)) = w2n rs`,
329   RD_INVARIANT A (rm:word32) rs rn n =
330     (if BORROW2 rs n then
331        rm * n2w (w2n rs MOD 2 ** (2 * n)) - rm << (2 * n)
333        rm * n2w (w2n rs MOD 2 ** (2 * n))) +
337   `!rs:word32. rs %% 1 = ((1 >< 0) rs):word2 %% 1`,
360   `!a rm rs rn.
361      RD_INVARIANT a rm rs rn (MLA_MUL_DUR rs) =
362        rm * rs + (if a then rn else 0w)`,
445   `!rs n. 2 * (n + 1) <= 32 ==>
446           ((((2 * n + 1) >< (2 * n)) rs = 0w:word2) \/
447            (((2 * n + 1) >< (2 * n)) rs = 1w:word2) ==> ~BORROW2 rs (n + 1)) /\
448           ((((2 * n + 1) >< (2 * n)) rs = 2w:word2) \/
449            (((2 * n + 1) >< (2 * n)) rs = 3w:word2) ==> BORROW2 rs (n + 1))`,
512   TRY (armLib.RES_MP1_TAC [`w` |-> `(2 * n + 1 >< 2 * n) (rs:word32)`] th
522   `!n a rm rs rn. 2 * (n + 1) <= 32 ==>
523      (RD_INVARIANT a rm rs rn (n + 1) =
524         let borrow2 = BORROW2 rs n
525         and mul = ((2 * n + 1) >< (2 * n)) rs
527           ALU6_MUL borrow2 mul (RD_INVARIANT a rm rs rn n)
545   `!n a rs.
546     ~(n = 0) /\ SUC n <= MLA_MUL_DUR rs ==>
547     (((2 * n + 1) >< (2 * n)) rs = mul) ==>
548     ((if ~BORROW2 rs n /\ (mul = 0w:word2) \/ BORROW2 rs n /\ (mul = 3w) then
549         RD_INVARIANT a rm rs rn n
551         (if BORROW2 rs n /\ (mul = 0w) \/ (mul = 1w) then
552            RD_INVARIANT a rm rs rn n +
554                        (if BORROW2 rs n /\ (mul = 1w) \/
555                           ~BORROW2 rs n /\ (mul = 2w) then 1w else 0w))
557            RD_INVARIANT a rm rs rn n -
559                        (if ~BORROW2 rs n /\ (mul = 2w) then 1w else 0w)))) =
560       RD_INVARIANT a rm rs rn (n + 1))`,
573   `!rs n. SUC n <= MLA_MUL_DUR rs ==>
574       (((2 * n + 1 >< 2 * n) rs):word2 %% 1 = BORROW2 rs (n + 1))`,
625   `SUC n <= MLA_MUL_DUR rs ==> n < 16`,
647       and rs = REG_READ6 reg nbs ((11 >< 8) ireg)
659               aregn2 F T F sctrl psrfb ((1 >< 0) pc) ARB ARB orp ((1 >< 0) rs)
660               ((31 -- 2) rs) F (if (1 >< 0) rs = 2w:word2 then 1w else 0w));
662         (let mul = (1 >< 0) ((31 -- (2 * (n - 1))) rs) in
663          let rd = RD_INVARIANT (ireg %% 21) rm rs rn (n - 1)
664          and mshift = MSHIFT mla_mul (BORROW2 rs (n - 1)) mul (n2w (n - 1))
665          and mul' = (1 >< 0) ((31 -- (2 * n)) rs)
666          and borrow2 = BORROW2 rs n in
667          let rd' = RD_INVARIANT (ireg %% 21) rm rs rn n
668          and newinst = MLA_MUL_DONE rs n in
702                 ARB (if n = 0 then orp else ARB) mul' ((31 -- (2 * (n + 1))) rs)
709     \\ ABBREV_TAC `rs = REG_READ6 reg nbs ((11 >< 8) ireg)`
787             \\ ABBREV_TAC `mul:word2 = ((2 * n + 1) >< (2 * n)) rs`