bigint_subp_j.mlw 6.98 KB
Newer Older
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
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
(*
general TODO:
- memory stack invariance

labels to investigate
'AD
'Q1
*)
module BV_asr_Lemmas

use import bv.BV8
use import int.Int
use import bv.Pow2int
use import int.EuclideanDivision

lemma asr_0: eq (asr zeros 1) zeros
lemma asr_1: eq (asr (of_int 1) 1) zeros
lemma asr_f: eq (asr ones 1) ones

lemma lsr_0: eq (lsr zeros 1) zeros
lemma lsr_1: eq (lsr (of_int 1) 1) zeros

lemma xor_0: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) zeros) = w
lemma xor_1: forall w. 0 <= w < 256 -> t'int (bw_xor (of_int w) ones) = 255 - w

lemma or_0: forall w. bw_or zeros w = w

lemma pow2_72: pow2 72 = 0x1000000000000000000
lemma pow2_80: pow2 80 = 0x100000000000000000000
lemma pow2_88: pow2 88 = 0x10000000000000000000000
lemma pow2_96: pow2 96 = 0x1000000000000000000000000
lemma pow2_104: pow2 104 = 0x100000000000000000000000000
lemma pow2_112: pow2 112 = 0x10000000000000000000000000000
lemma pow2_120: pow2 120 = 0x1000000000000000000000000000000
lemma pow2_128: pow2 128 = 0x100000000000000000000000000000000
lemma pow2_136: pow2 136 = 0x10000000000000000000000000000000000
lemma pow2_144: pow2 144 = 0x1000000000000000000000000000000000000
lemma pow2_152: pow2 152 = 0x100000000000000000000000000000000000000
lemma pow2_160: pow2 160 = 0x10000000000000000000000000000000000000000
lemma pow2_168: pow2 168 = 0x1000000000000000000000000000000000000000000
lemma pow2_176: pow2 176 = 0x100000000000000000000000000000000000000000000
lemma pow2_184: pow2 184 = 0x10000000000000000000000000000000000000000000000
lemma pow2_192: pow2 192 = 0x1000000000000000000000000000000000000000000000000
lemma pow2_200: pow2 200 = 0x100000000000000000000000000000000000000000000000000
lemma pow2_208: pow2 208 = 0x10000000000000000000000000000000000000000000000000000
lemma pow2_216: pow2 216 = 0x1000000000000000000000000000000000000000000000000000000
lemma pow2_224: pow2 224 = 0x100000000000000000000000000000000000000000000000000000000
lemma pow2_232: pow2 232 = 0x10000000000000000000000000000000000000000000000000000000000
lemma pow2_240: pow2 240 = 0x1000000000000000000000000000000000000000000000000000000000000
lemma pow2_248: pow2 248 = 0x100000000000000000000000000000000000000000000000000000000000000
lemma pow2_256: pow2 256 = 0x10000000000000000000000000000000000000000000000000000000000000000

end

module AvrModelLemmas

use import int.Int
use import map.Map
use import int.EuclideanDivision
use import bv.Pow2int

lemma register_file_invariant_strengthen:
  forall m m': map int int. (forall i. 0 <= m[i] < 256) -> (forall i. 0 <= m'[i] < 256) -> (forall i j. 0 <= m[i]*m'[j] <= 255*255)
(*
lemma register_file_invariant_strengthen:
  forall m: map int int. (forall i. 0 <= m[i] < 256) -> (forall i j. 0 <= m[i]*m[j] <= 255*255)
*)

lemma pow_split: forall k. k >= 0 -> pow2 (2*k) = pow2 k*pow2 k

end

module AVRcode

use import avrmodel.AVRint
use import int.Int
use import int.EuclideanDivision
use import bv.Pow2int
use import AvrModelLemmas
use BV_asr_Lemmas
use bv.BV8
use import ref.Ref

use import int.Abs

use avrmodel.Shadow as S

lemma mul_bound_preserve:
  forall x y l. 0 <= x <= l -> 0 <= y <= l -> x*y <= l*l

constant p25519: int = 0x7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffed

let bigint_subp ()
  requires { 32 <= uint 2 reg 22 < pow2 15 }
  requires { 32 <= uint 2 reg 24 < pow2 15 }
  requires { uint 2 reg 24 <= uint 2 reg 22 \/ uint 2 reg 24 >= uint 2 reg 22 + 32 }
  ensures { uint 32 mem (old (uint 2 reg 24)) - pow2 256*reg[24] = old (uint 32 mem (uint 2 reg 22)) - p25519 }
=
  movw r26 r22; (* load operand address a to x *)
  movw r30 r24; (* load address of result to z *)
'S:

  ldi r21 0xed;
  ld_inc r20 rX;
  sub r20 r21;
  st_inc rZ  r20;

  ldi r21 0xff;

  S.init();
  for i = 1 to 30 do
    invariant { S.synchronized S.shadow reg }
    invariant { forall i. 0 <= reg[i] < 256 }
    invariant { forall i. 0 <= mem[i] < 256 }
    invariant { uint 2 reg rX = at(uint 2 reg rX+i)'S }
    invariant { uint 2 reg rZ = at(uint 2 reg rZ+i)'S }
    invariant { forall j. mem[j] <> (at mem 'S)[j] -> at(uint 2 reg rZ)'S <= j < at(uint 2 reg rZ)'S+i }
    invariant { uint i mem (at (uint 2 reg rZ)'S) = ?cf*pow2 (8*i) + at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) }
    (* this is an on-the-fly proof by induction *)
    invariant { forall mem mem', o. eq i mem mem' o -> uint i mem o = uint i mem' o }
    let ghost i = i in
    
'B:
    assert { pow2 8*pow2 (8*i) = pow2 (8*i+8) };
    assert { mem[uint 2 reg rX] = (at mem 'S)[uint 2 reg rX] };
    ld_inc r20 rX;
    sbc r20 r21;
    st_inc rZ  r20;
(*
    check { eq i mem (at mem 'B) (at(uint 2 reg rZ)'S) };
*)
    (* apply the inductive proof *)
    assert { uint i mem (at (uint 2 reg rZ)'S) = uint i (at mem 'B) (at(uint 2 reg rZ)'S) };
    assert { mem[at(uint 2 reg rZ)'B] = ?cf*pow2 8 + at(mem[uint 2 reg rX])'B - 0xff - at (?cf) 'B };
    assert { forall o, mem. uint (i+1) mem o = uint i mem o + pow2 (8*i)*mem[o+i] };
(*
  check { uint (i+1) mem (at (uint 2 reg rZ)'S) 
         = uint i mem (at (uint 2 reg rZ)'S) + pow2 (8*i)*mem[at(uint 2 reg rZ)'S+i]
         = uint i mem (at (uint 2 reg rZ)'S) + pow2 (8*i)*mem[at(uint 2 reg rZ)'B]
         = uint i (at mem 'B) (at (uint 2 reg rZ)'S) + pow2 (8*i)*mem[at(uint 2 reg rZ)'B]
         = at(?cf)'B*pow2 (8*i) + at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) 
           + pow2 (8*i)*mem[at(uint 2 reg rZ)'B]
         = at(?cf)'B*pow2 (8*i) + at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) 
           + pow2 (8*i)*at(mem[uint 2 reg rX])'B + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i) - pow2 (8*i)*at(?cf)'B
         = at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + pow2 (8*i)*at(mem[uint 2 reg rX])'B + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
         = at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + pow2 (8*i)*at((at mem 'S)[uint 2 reg rX])'B + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
         = at(uint i mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + pow2 (8*i)*at(mem[uint 2 reg rX+i])'S + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i)
         = at(uint (i+1) mem (uint 2 reg rX))'S - (pow2 (8*i)-19) + ?cf*pow2 8*pow2 (8*i) - 0xff*pow2 (8*i) 
         = ?cf*pow2 (8*i)*pow2 8 + at(uint (i+1) mem (uint 2 reg rX))'S - (pow2 8*pow2 (8*i)-19)
         = ?cf*pow2 (8*(i+1)) + at(uint (i+1) mem (uint 2 reg rX))'S - (pow2 (8*(i+1))-19) };
*)
    S.modify_r20();
    S.modify_r26(); S.modify_r27();
    S.modify_r30(); S.modify_r31();
      assert { forall mem mem', o. eq (i+1) mem mem' o -> uint i mem o = uint i mem' o /\ mem[o+i] = mem'[o+i] };
(*
      assert { forall mem mem', o. eq (i+1) mem mem' o -> eq i mem mem' o };
      assert { forall mem mem', o. eq (i+1) mem mem' o -> uint i mem' o = uint i mem o };
      assert { forall mem mem', o. eq (i+1) mem mem' o -> mem[o+i] = mem'[o+i] };
      assert { forall mem mem', o. eq (i+1) mem mem' o -> uint i mem o + pow2 (8*i)*mem[o+i] = uint i mem' o + pow2 (8*i)*mem'[o+i] };
*)
  done;

  ldi r21 0x7f;
  ld_inc r20 rX;
  sbc r20 r21;
  st_inc rZ  r20;
(*
  check { uint 32 mem (at (uint 2 reg rZ)'S) = ?cf*pow2 256 + at(uint 32 mem (uint 2 reg rX))'S - p25519 };
*)

  clr r24;
  adc r24 r24;

end