Skip to content

Fix various rules necessary to prove progress (and some preservation) #8

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
ivg merged 3 commits into from
Jul 25, 2018
Merged

Fix various rules necessary to prove progress (and some preservation) #8

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
badc474
Fix various rules necessary to prove progress (and some preservation)
Jul 24, 2018
1a93aab
Change ite rules to evaluate branches. Add missing rule.
Jul 25, 2018
29f2433
Commit on wrong branch.
Jul 25, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
90 changes: 61 additions & 29 deletions bil.ott
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,12 +125,20 @@ grammar
| w1 .<$ w2 :: S :: signed_less
{{ tex [[w1]] \stackrel{sbv} < [[w2]] }}
{{ com -- signed less than }}
| .- w :: S :: lneg
{{ tex \stackrel{bv} - [[w]] }}
{{ com -- integer negation }}
| .~ w :: S :: lnot
{{ tex \stackrel{bv}{\sim} [[w]] }}
{{ com -- logical negation }}
| w1 .@ w2 :: S :: concat
{{ tex [[w1]] \stackrel{bv} . [[w2]] }}
{{ com -- concatenation }}
| ext word ~hi : sz1 ~lo : sz2 :: S :: extend_extract
| ext w ~ hi : sz1 ~ lo : sz2 :: S :: extend_extract
{{ tex [[ext]]\; [[w]] \sim [[hi]] : [[sz1]] \sim [[lo]] : [[sz2]] }}
{{ com -- extract/extend }}
| exts word ~hi : sz1 ~lo : sz2 :: S :: extend_extract_signed
| exts w ~ hi : sz1 ~ lo : sz2 :: S :: extend_extract_signed
{{ tex [[exts]]\; [[w]] \sim [[hi]] : [[sz1]] \sim [[lo]] : [[sz2]] }}
{{ com -- signed extract/extend }}


Expand Down Expand Up @@ -193,6 +201,14 @@ grammar
| unsigned :: :: unsigned
{{ com -- extend with zero}}

widen_cast :: wcast_ ::=
| signed :: :: signed
| unsigned :: :: unsigned

narrow_cast :: ncast_ ::=
| low :: :: low
| high :: :: high

type,t :: type_ ::=
| imm < sz > :: :: imm
{{ com -- immediate of size $sz$}}
Expand All @@ -217,6 +233,8 @@ formula :: formula_ ::=
| ( formula ) :: M :: paren {{ coq ([[formula]]) }}
| v1 <> v2 :: M :: exp_neq {{ coq ([[v1]] <> [[v2]]) }}
| var1 <> var2 :: M :: exp_var {{ coq ([[var1]] <> [[var2]]) }}
| w1 .<> w2 :: M :: word_neq
{{ tex [[w1]] <> [[w2]] }}
| nat1 > nat2 :: M :: nat_gt {{ coq ([[nat1]] > [[nat2]])}}
| nat1 = nat2 :: M :: nat_eq {{ coq ([[nat1]] = [[nat2]])}}
| nat1 >= nat2 :: M :: nat_ge {{ coq ([[nat1]] >= [[nat2]])}}
Expand Down Expand Up @@ -250,6 +268,8 @@ terminals :: terminals_ ::=

subrules
val <:: exp
widen_cast <:: cast
narrow_cast <:: cast

funs
Compute ::=
Expand Down Expand Up @@ -337,12 +357,17 @@ defns typing_exp :: '' ::=
---------------------------------- :: uop
G |- uop e1 :: imm<sz>


sz > 0
sz >= nat
G |- e :: imm<nat>
--------------------- :: cast
G |- cast:sz[e] :: imm<sz>
------------------------------------- :: cast_widen
G |- widen_cast:sz[e] :: imm<sz>

sz > 0
nat >= sz
G |- e :: imm<nat>
------------------------------------- :: cast_narrow
G |- narrow_cast:sz[e] :: imm<sz>

G |- e1 :: t
G, id:t |- e2 :: t'
Expand Down Expand Up @@ -479,15 +504,18 @@ defns reduce_exp :: '' ::=
delta |- e1[v2,ed]:sz ~> e1'[v2,ed]:sz

------------------------------------------------------ :: load_byte
delta |- v[w <- w':sz][w,ed']:sz ~> w'
delta |- v[w <- v':sz][w,ed']:sz ~> v'

w1 <> w2
----------------------------------------------------------- :: load_byte_from_next
delta |- v[w1 <- w':sz][w2,ed]:sz ~> v[w2,ed]:sz
delta |- v[w1 <- v':sz][w2,ed]:sz ~> v[w2,ed]:sz

---------------------------------------------------------- :: load_un_mem
delta |- (unknown[str]:t)[v,ed]:sz ~> unknown[str]:imm<sz>

------------------------------------------------------------------------- :: load_un_addr
delta |- (v[w1 <- v':sz])[unknown[str]:t,ed]:sz' ~> unknown[str]:imm<sz'>

sz' > sz
succ w = w'
type(v) = mem<nat,sz>
Expand Down Expand Up @@ -534,17 +562,13 @@ defns reduce_exp :: '' ::=
-------------------------------------------------------------------------------- :: store_word_el
delta |- v with [w,el]:sz' <- val ~> e1 with [w',el]:(sz'-sz) <- high:(sz'-sz)[val]

type(v) = mem<nat,sz'>
-------------------------------------------------------------- :: store_val
delta |- v with [num:sz,ed] : sz' <- w' ~> v[num:sz <- w' : sz']

type(v) = mem<nat,sz'>
----------------------------------------------------------------------------------------- :: store_un
delta |- v with [num:sz,ed] : sz' <- unknown[str]:t ~> v[num:sz <- unknown[str]:t : sz']

type(v) = mem<nat,sz>
--------------------------------------------------------------------------------- :: store_un_addr
delta |- v with [unknown[str]:imm<nat>,ed] : sz' <- v2 ~> unknown[str]:mem<nat,sz>
--------------------------------------------------------- :: store_val
delta |- v with [w,ed] : sz <- v' ~> v[w <- v' : sz]

type(v) = t
----------------------------------------------------------------------- :: store_un_addr
delta |- v with [unknown[str]:t',ed] : sz' <- v2 ~> unknown[str]:t

delta |- e1 ~> e1'
------------------------------------------------ :: let_step
Expand All @@ -566,7 +590,6 @@ defns reduce_exp :: '' ::=
------------------------------------------------ :: ite_false
delta |- if false then e2 else e3 ~> e3


delta |- e2 ~> e2'
------------------------------------------ :: bop_rhs
delta |- v1 bop e2 ~> v1 bop e2'
Expand Down Expand Up @@ -633,14 +656,20 @@ defns reduce_exp :: '' ::=
----------------------------------------------- :: xor
delta |- w1 xor w2 ~> w1 .xor w2


----------------------------------------------- :: eq
----------------------------------------------- :: eq_same
delta |- w = w ~> true

w1 .<> w2
----------------------------------------------- :: eq_diff
delta |- w1 = w2 ~> false


----------------------------------------------- :: neq
----------------------------------------------- :: neq_same
delta |- w <> w ~> false

w1 .<> w2
----------------------------------------------- :: neq_diff
delta |- w1 <> w2 ~> true

----------------------------------------------- :: less
delta |- w1 < w2 ~> w1 .< w2
Expand All @@ -663,13 +692,14 @@ defns reduce_exp :: '' ::=
---------------------------------------- :: uop
delta |- uop e ~> uop e'

---------------------------------------- :: not_true
delta |- ~true ~> false

------------------------------------------------ :: uop_unk
delta |- uop unknown[str] : t ~> unknown[str] : t

---------------------------------------- :: not_false
delta |- ~false ~> true
---------------------------------------- :: not
delta |- ~ w ~> .~ w

---------------------------------------- :: neg
delta |- - w ~> .- w

delta |- e2 ~> e2'
---------------------------------------- :: concat_rhs
Expand Down Expand Up @@ -706,20 +736,22 @@ defns reduce_exp :: '' ::=
--------------------------------- :: cast_reduce
delta |- cast:sz[e] ~> cast:sz[e']

------------------------------------------------------------ :: cast_unk
delta |- cast:sz[unknown[str] : t] ~> unknown[str] : imm<sz>

-------------------------------------------- :: cast_low
delta |- low:sz[w] ~> ext w ~hi:(sz-1) ~lo:0


----------------------------------------------------------- :: cast_high
delta |- high:sz[num:sz'] ~> ext num:sz' ~hi:sz' ~lo:(sz'-sz)
delta |- high:sz[num:sz'] ~> ext num:sz' ~hi:(sz'-1) ~lo:(sz'-sz)


-------------------------------------------- :: cast_signed
delta |- signed:sz[w] ~> exts w ~hi:(sz-1) ~lo:0

-------------------------------------------- :: cast_unsigned
delta |- unsigned:sz[w] ~> low:sz[w]
-------------------------------------------------- :: cast_unsigned
delta |- unsigned:sz[w] ~> ext w ~hi:(sz-1) ~lo:0


defns reduce_stmt :: '' ::=
Expand Down