Commit 996cae87 authored by Marc Schoolderman's avatar Marc Schoolderman
Browse files

added compute_specified to avrmodel_alt

parent c25c68c1
...@@ -50,6 +50,8 @@ function (?) (x: cpu_flag): int = if x.value then 1 else 0 ...@@ -50,6 +50,8 @@ function (?) (x: cpu_flag): int = if x.value then 1 else 0
let (?) (x: cpu_flag) ensures { result = ?x } = if x.value then 1 else 0 let (?) (x: cpu_flag) ensures { result = ?x } = if x.value then 1 else 0
meta rewrite_def function (?)
val cf: cpu_flag val cf: cpu_flag
type byte = < range 0 255 > type byte = < range 0 255 >
...@@ -99,35 +101,40 @@ val reg: address_space ...@@ -99,35 +101,40 @@ val reg: address_space
the notion of "not computable" and "computable"; however, we can still use non-computable stuff the notion of "not computable" and "computable"; however, we can still use non-computable stuff
in non-ghost code by conjuring it into existence using the 'any' expression. in Why3 1.x, this is in non-ghost code by conjuring it into existence using the 'any' expression. in Why3 1.x, this is
safe (a witness must be provided), whereas in Why3 0.8x it would not be safe. safe (a witness must be provided), whereas in Why3 0.8x it would not be safe.
note: this may no longer work in future versions of Why3
this comment can be removed at any time.*) this comment can be removed at any time.*)
let data_set (m: map int byte) (i: register) (v: int): map int byte let data_set (m: map int byte) (i: register) (v: int): map int byte
requires { 0 <= v < 256 } requires { 0 <= v < 256 }
ensures { result = Map.set m i ($v) } ensures { result = Map.set m i ($v) }
= let v' = any byte ensures { result = v } in = any map int byte ensures { result = Map.set m i ($v) }
any map int byte ensures { result = Map.set m i v' }
let read (m: address_space) (i: int): int let read (m: address_space) (i: int): int
= any int ensures { m[i] = result } = any int ensures { m[i] = result }
(* WIP COMMENT: the 'consistency proof' here requires this existentiality axiom, unless
'let mov' is rewritten. regardless, I think the axiom is (logically) a good one, as it
affirms that there are exactly 256 type inhabitants. *)
axiom byte_existentiality:
forall x y: byte. byte'int x = byte'int y -> x = y
let mov (dst src: register): unit let mov (dst src: register): unit
writes { reg } writes { reg }
ensures { reg = old reg[dst<-reg[src]] } ensures { reg = old reg[dst<-reg[src]] }
= reg.data <- data_set reg.data dst (read reg src) = reg.data <- data_set reg.data dst (read reg src)
(* WIP: mul,add,adc,made abstract for now; other instructions disabled *) let mul (dst src: register): unit
val mul (dst src: register): unit
writes { cf } writes { cf }
writes { reg } writes { reg }
ensures { let p = old (reg[src]*reg[dst]) in reg = (old reg)[0 <- lo8 p][1 <- hi8 p] } ensures { let p = old (reg[src]*reg[dst]) in reg = (old reg)[0 <- lo8 p][1 <- hi8 p] }
ensures { let p = old (reg[src]*reg[dst]) in ?cf = div p (pow2 15) } ensures { let p = old (reg[src]*reg[dst]) in ?cf = div p (pow2 15) }
(* ensures { reg[1] < 255 } *) (* ensures { reg[1] < 255 } *)
(*
= let prod = read reg dst*read reg src in = let prod = read reg dst*read reg src in
reg.data <- data_set (data_set reg.data 0 (mod prod 256)) 1 (div prod 256); reg.data <- data_set (data_set reg.data 0 (mod prod 256)) 1 (div prod 256);
cf.value <- (div prod 0x8000 <> 0); cf.value <- (div prod 0x8000 <> 0);
() ()
*)
let add (dst src: register): unit let add (dst src: register): unit
writes { cf } writes { cf }
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="5">
<prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" alternative="noBV" timelimit="13" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC3" version="2.4.1" timelimit="13" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/>
<path name="avrmodel_alt.mlw"/>
<theory name="AVRbyte" proved="true">
<goal name="VC prefix ?" expl="VC for prefix ?" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC uint_sum" expl="VC for uint_sum" proved="true">
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="B.Sum_def_empty" proved="true">
<proof prover="4"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="B.Sum_def_non_empty" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC prefix $" expl="VC for prefix $" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC lo8" expl="VC for lo8" proved="true">
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC hi8" expl="VC for hi8" proved="true">
<proof prover="4"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="VC data_set" expl="VC for data_set" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC read" expl="VC for read" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mov" expl="VC for mov" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC mul" expl="VC for mul" proved="true">
<proof prover="2"><result status="valid" time="0.98" steps="170"/></proof>
</goal>
<goal name="VC add" expl="VC for add" proved="true">
<proof prover="4"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC adc" expl="VC for adc" proved="true">
<proof prover="4"><result status="valid" time="1.30"/></proof>
</goal>
<goal name="VC sub" expl="VC for sub" proved="true">
<proof prover="4"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="VC sbc" expl="VC for sbc" proved="true">
<proof prover="4"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="VC neg" expl="VC for neg" proved="true">
<proof prover="4"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="VC subi" expl="VC for subi" proved="true">
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC sbci" expl="VC for sbci" proved="true">
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC inc" expl="VC for inc" proved="true">
<proof prover="4"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="VC dec" expl="VC for dec" proved="true">
<proof prover="4"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="VC ld_inc" expl="VC for ld_inc" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC ld_inc.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC ld_inc.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC ld_inc.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC ld_inc.3" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC ld_inc.4" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC ld_inc.5" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.10"/></proof>
</goal>
<goal name="VC ld_inc.6" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.70" steps="172"/></proof>
</goal>
<goal name="VC ld_inc.7" expl="postcondition" proved="true">
<proof prover="2"><result status="valid" time="2.87" steps="167"/></proof>
</goal>
</transf>
</goal>
<goal name="VC ldd" expl="VC for ldd" proved="true">
<proof prover="2"><result status="valid" time="0.40" steps="136"/></proof>
</goal>
<goal name="VC std" expl="VC for std" proved="true">
<proof prover="2"><result status="valid" time="0.31" steps="137"/></proof>
</goal>
<goal name="VC push" expl="VC for push" proved="true">
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC pop" expl="VC for pop" proved="true">
<proof prover="4"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="eq_narrow" proved="true">
<proof prover="4"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="eq_combine" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="eq_uint" proved="true">
<proof prover="5"><result status="valid" time="0.24"/></proof>
</goal>
<goal name="uint_0" proved="true">
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="uint_1" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_1.0" proved="true">
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_2" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_2.0" proved="true">
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_3" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_3.0" proved="true">
<proof prover="5"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_4" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_4.0" proved="true">
<proof prover="5"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_5" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_5.0" proved="true">
<proof prover="5"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_6" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_6.0" proved="true">
<proof prover="5"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_7" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_7.0" proved="true">
<proof prover="5"><result status="valid" time="0.12"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_8" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_8.0" proved="true">
<proof prover="5"><result status="valid" time="0.14"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_9" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_9.0" proved="true">
<proof prover="5"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_10" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_10.0" proved="true">
<proof prover="5"><result status="valid" time="0.18"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_11" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_11.0" proved="true">
<proof prover="5"><result status="valid" time="0.28"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_12" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_12.0" proved="true">
<proof prover="5"><result status="valid" time="0.31"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_13" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_13.0" proved="true">
<proof prover="5"><result status="valid" time="0.36"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_14" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_14.0" proved="true">
<proof prover="5"><result status="valid" time="0.51"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_15" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_15.0" proved="true">
<proof prover="5"><result status="valid" time="0.57"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_16" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_16.0" proved="true">
<proof prover="5"><result status="valid" time="0.66"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_17" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_17.0" proved="true">
<proof prover="5"><result status="valid" time="0.76"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_18" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_18.0" proved="true">
<proof prover="5"><result status="valid" time="0.92"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_19" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_19.0" proved="true">
<proof prover="5"><result status="valid" time="1.04"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_20" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_20.0" proved="true">
<proof prover="5"><result status="valid" time="1.04"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_21" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_21.0" proved="true">
<proof prover="5"><result status="valid" time="1.04"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_22" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_22.0" proved="true">
<proof prover="5"><result status="valid" time="1.21"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_23" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_23.0" proved="true">
<proof prover="5"><result status="valid" time="1.18"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_24" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_24.0" proved="true">
<proof prover="5"><result status="valid" time="1.78"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_25" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_25.0" proved="true">
<proof prover="5"><result status="valid" time="2.12"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_26" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_26.0" proved="true">
<proof prover="5"><result status="valid" time="2.08"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_27" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_27.0" proved="true">
<proof prover="5"><result status="valid" time="2.68"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_28" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_28.0" proved="true">
<proof prover="5"><result status="valid" time="2.91"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_29" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_29.0" proved="true">
<proof prover="5"><result status="valid" time="3.38"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_30" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_30.0" proved="true">
<proof prover="5"><result status="valid" time="4.20"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_31" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_31.0" proved="true">
<proof prover="5"><result status="valid" time="4.36"/></proof>
</goal>
</transf>
</goal>
<goal name="uint_32" proved="true">
<transf name="inline_all" proved="true" >
<goal name="uint_32.0" proved="true">
<proof prover="5"><result status="valid" time="4.72"/></proof>
</goal>
</transf>
</goal>
<goal name="VC movw" expl="VC for movw" proved="true">
<proof prover="4"><result status="valid" time="0.64"/></proof>
</goal>
<goal name="VC adiw" expl="VC for adiw" proved="true">
<proof prover="2"><result status="valid" time="4.68" steps="616"/></proof>
</goal>
<goal name="VC sbiw" expl="VC for sbiw" proved="true">
<proof prover="2"><result status="valid" time="4.88" steps="155"/></proof>
</goal>
</theory>
<theory name="Shadow" proved="true">
<goal name="VC modify_r0" expl="VC for modify_r0" proved="true">
<proof prover="2"><result status="valid" time="0.12" steps="69"/></proof>
</goal>
<goal name="VC modify_r1" expl="VC for modify_r1" proved="true">
<proof prover="2"><result status="valid" time="0.12" steps="69"/></proof>
</goal>
<goal name="VC modify_r2" expl="VC for modify_r2" proved="true">
<proof prover="2"><result status="valid" time="0.10" steps="69"/></proof>
</goal>
<goal name="VC modify_r3" expl="VC for modify_r3" proved="true">
<proof prover="2"><result status="valid" time="0.12" steps="69"/></proof>
</goal>
<goal name="VC modify_r4" expl="VC for modify_r4" proved="true">
<proof prover="2"><result status="valid" time="0.12" steps="69"/></proof>
</goal>
<goal name="VC modify_r5" expl="VC for modify_r5" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="69"/></proof>
</goal>
<goal name="VC modify_r6" expl="VC for modify_r6" proved="true">
<proof prover="2"><result status="valid" time="0.12" steps="69"/></proof>
</goal>
<goal name="VC modify_r7" expl="VC for modify_r7" proved="true">
<proof prover="2"><result status="valid" time="0.12" steps="69"/></proof>
</goal>
<goal name="VC modify_r8" expl="VC for modify_r8" proved="true">
<proof prover="2"><result status="valid" time="0.10" steps="69"/></proof>
</goal>
<goal name="VC modify_r9" expl="VC for modify_r9" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="69"/></proof>
</goal>
<goal name="VC modify_r10" expl="VC for modify_r10" proved="true">
<proof prover="2"><result status="valid" time="0.11" steps="69"/></proof>
</goal>
<goal name="VC modify_r11" expl="VC for modify_r11" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="69"/></proof>
</goal>
<goal name="VC modify_r12" expl="VC for modify_r12" proved="true">
<proof prover="2"><result status="valid" time="0.12" steps="69"/></proof>
</goal>
<goal name="VC modify_r13" expl="VC for modify_r13" proved="true">
<proof prover="2"><result status="valid" time="0.11" steps="69"/></proof>
</goal>
<goal name="VC modify_r14" expl="VC for modify_r14" proved="true">
<proof prover="2"><result status="valid" time="0.15" steps="69"/></proof>
</goal>
<goal name="VC modify_r15" expl="VC for modify_r15" proved="true">
<proof prover="2"><result status="valid" time="0.15" steps="69"/></proof>
</goal>
<goal name="VC modify_r16" expl="VC for modify_r16" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="69"/></proof>
</goal>
<goal name="VC modify_r17" expl="VC for modify_r17" proved="true">
<proof prover="2"><result status="valid" time="0.16" steps="69"/></proof>
</goal>
<goal name="VC modify_r18" expl="VC for modify_r18" proved="true">
<proof prover="2"><result status="valid" time="0.14" steps="69"/></proof>
</goal>
<goal name="VC modify_r19" expl="VC for modify_r19" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="69"/></proof>
</goal>
<goal name="VC modify_r20" expl="VC for modify_r20" proved="true">
<proof prover="2"><result status="valid" time="0.15" steps="69"/></proof>
</goal>
<goal name="VC modify_r21" expl="VC for modify_r21" proved="true">
<proof prover="2"><result status="valid" time="0.14" steps="69"/></proof>
</goal>
<goal name="VC modify_r22" expl="VC for modify_r22" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="69"/></proof>
</goal>
<goal name="VC modify_r23" expl="VC for modify_r23" proved="true">
<proof prover="2"><result status="valid" time="0.14" steps="69"/></proof>
</goal>
<goal name="VC modify_r24" expl="VC for modify_r24" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="69"/></proof>
</goal>
<goal name="VC modify_r25" expl="VC for modify_r25" proved="true">
<proof prover="2"><result status="valid" time="0.11" steps="69"/></proof>
</goal>
<goal name="VC modify_r26" expl="VC for modify_r26" proved="true">
<proof prover="2"><result status="valid" time="0.14" steps="69"/></proof>
</goal>
<goal name="VC modify_r27" expl="VC for modify_r27" proved="true">
<proof prover="2"><result status="valid" time="0.14" steps="69"/></proof>
</goal>
<goal name="VC modify_r28" expl="VC for modify_r28" proved="true">
<proof prover="2"><result status="valid" time="0.14" steps="69"/></proof>
</goal>
<goal name="VC modify_r29" expl="VC for modify_r29" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="69"/></proof>
</goal>
<goal name="VC modify_r30" expl="VC for modify_r30" proved="true">
<proof prover="2"><result status="valid" time="0.13" steps="69"/></proof>
</goal>
<goal name="VC modify_r31" expl="VC for modify_r31" proved="true">
<proof prover="2"><result status="valid" time="0.14" steps="69"/></proof>
</goal>
<goal name="VC init" expl="VC for init" proved="true">
<proof prover="5"><result status="valid" time="0.88"/></proof>
</goal>
</theory>
</file>
</why3session>
...@@ -53,50 +53,24 @@ let mul8 (): unit ...@@ -53,50 +53,24 @@ let mul8 (): unit
= mul r3 r8; = mul r3 r8;
movw r12 r0 movw r12 r0
(* WIP: i've left the checks in for possible future debugging, for now *)
let mul16 (): unit let mul16 (): unit
requires { forall i. 0 <= reg[i] < 256 } requires { forall i. 0 <= reg[i] < 256 }
ensures { uint 4 reg 12 = old(uint 2 reg 2 * uint 2 reg 7) } ensures { uint 4 reg 12 = old(uint 2 reg 2 * uint 2 reg 7) }
= =
clr r23; clr r23;
label Before in
mul r3 r8; mul r3 r8;
check { reg[0] = mod ((reg[8]*reg[3]) at Before) 256 };
check { reg[1] = div ((reg[8]*reg[3]) at Before) 256 };
check { reg[0] + reg[1]*256 = (reg[3]*reg[8]) at Before };
movw r14 r0; movw r14 r0;
check { reg[14] + reg[15]*256 = (reg[3]*reg[8]) at Before };
mul r2 r7; mul r2 r7;
movw r12 r0; movw r12 r0;
check { reg[12] + reg[13]*256 = (reg[2]*reg[7]) at Before };
mul r2 r8; mul r2 r8;
check { reg[0] + reg[1]*256 = (reg[2]*reg[8]) at Before };
label B in
check { reg[23] = 0 };
add r13 r0; add r13 r0;
adc r14 r1; adc r14 r1;
adc r15 r23; adc r15 r23;
check { uint 3 reg 13 + ?cf*pow2 24 = uint 3 reg 13 at B + uint 2 reg 0 at B = uint 3 reg 13 at B + (reg[2]*reg[8]) at B };
check { uint 4 reg 12 + ?cf*pow2 32 = uint 4 reg 12 at B + pow2 8*uint 2 reg 0 at B = uint 4 reg 12 at B + pow2 8*(reg[2]*reg[8]) at B };
check { uint 4 reg 12 + ?cf*pow2 32 = (pow2 16*reg[3]*reg[8]+reg[2]*reg[7]+pow2 8*reg[2]*reg[8]) at Before };
(*
begin ensures { ?cf = 0 }
assert { forall i. 0 <= reg[i] < 256 };
assert { reg[3]*reg[8] <= 255*255 by 0 <= reg[3] <= 255 /\ 0 <= reg[8] <= 255 };
assert { 0 <= uint 4 reg 12 + ?cf*pow2 32 = (pow2 16*reg[3]*reg[8]+reg[2]*reg[7]+pow2 8*reg[2]*reg[8]) at Before < pow2 32 };
assert { 0 <= uint 4 reg 12 + ?cf*pow2 32 < pow2 32 };
end;
*)
mul r3 r7; mul r3 r7;
check { reg[0] + reg[1]*256 = reg[3]*reg[7] };
add r13 r0; add r13 r0;
adc r14 r1; adc r14 r1;
adc r15 r23; adc r15 r23;
(* ()
begin ensures { ?cf = 0 }
assert { 0 <= uint 4 reg 12 + ?cf*pow2 32 = (uint 2 reg 2 * uint 2 reg 7) at Before < pow2 32 };
end
*) ()
(* NOTE: by changing (some of) the checks into asserts, we can test the impact on performance (* NOTE: by changing (some of) the checks into asserts, we can test the impact on performance
of having vs. not having an explicit mention of the 8bit-ness of the AVR architecture in the proof context. of having vs. not having an explicit mention of the 8bit-ness of the AVR architecture in the proof context.
......
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN" <!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd"> "http://why3.lri.fr/why3session.dtd">