machine-code/graph/GraphLangScript.sml

22   | VarWord ('a word)
23   | VarMem ('a word -> word8)
24   | VarDom ('a word set)
161   jump = Jump ('a word) | Return`
169   inst = Inst ('a word) ('a assert) ('a next) (* name, inv, what happens *)`
172   func = Func string ('a word) ('a inst list) (* name, entry point, insts *)`;
403   IMPL_INST code locs (Inst (n:'a word) assert next) =
758       ?a t. find_inst ((n2w n) :'a word) l = SOME (Inst (n2w n) a t)``,
919       (find_inst (n2w i) l = SOME (Inst ((n2w i) :'a word) a next)) ==>
933   \\ Cases_on `next_trans (w2n (c:'a word)) k1 n`
968   \\ MP_TAC (next_trans_IMP |> Q.SPECL [`nn`,`w2n (c:'a word)`] |> SPEC_ALL)
1015   \\ MP_TAC (next_trans_IMP |> Q.SPECL [`n`,`w2n (c:'a word)`,`k`,`q`,`r`])
1585   READ8 a mem = (mem:'a word -> word8) a`;
1606   WRITE8 (a:'a word) (w:word8) (mem:'a word->word8) = (a =+ w) mem`;
1639   ``n2w (w2n ((w:'a word) >>> m)):'a word``
1658     (((h1:word16) @@ (b2:word8)):24 word = w2w h1 << 8 || w2w b2) /\
1659     (((b1:word8) @@ (h2:word16)):24 word = w2w b1 << 16 || w2w h2) /\
1810   count_leading_zero_bits (w:'a word) =
1811     (n2w (arm$CountLeadingZeroBits w)):'a word`;
1822   word_add_with_carry (w1:'a word) w2 c =
1846   ShiftLeft (w:'a word) (y:'a word) = word_lsl w (w2n y)`;
1849   ShiftRight (w:'a word) (y:'a word) = word_lsr w (w2n y)`;
1852   SignedShiftRight (w:'a word) (y:'a word) = word_asr w (w2n y)`;
1855   ``((w2w:word32 -> 33 word) (w1:word32) << w2n ((w2w (w2:word32)):word8)) ' 32 <=>
1871   ``EVERY (\i. (((w2w (w:word32) << i):33 word) ' 32) <=>
1962   ``word_add_with_carry (x:'a word) y z =
2036   ``(((w2w:word32 -> 31 word) w @@ (0w:word1)) : word32 = w << 1) /\
2037     (((w2w:word32 -> 30 word) w @@ (0w:word2)) : word32 = w << 2)``,
2088   ``arm$Aligned (w,n) ==> (arm$Align (w:'a word,n) = w)``,
2319   ``fixwidth (dimindex (:'a)) (w2v (w:'a word)) = w2v w``,
2343   ``(w + x ��� w = x:'a word) /\
2344     (w + x ��� (w + y) = x - y:'a word) /\
2345     (w + x ��� (w - y) = x + y:'a word)``,