diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/coq/Sail2_prompt.v | 38 | ||||
| -rw-r--r-- | lib/isabelle/output/document/Sail2_operators_bitlists.tex | 1810 |
2 files changed, 1833 insertions, 15 deletions
diff --git a/lib/coq/Sail2_prompt.v b/lib/coq/Sail2_prompt.v index 8efd66f0..5ab93cbc 100644 --- a/lib/coq/Sail2_prompt.v +++ b/lib/coq/Sail2_prompt.v @@ -136,19 +136,29 @@ Definition Zwf_guarded (z:Z) : Acc (Zwf 0) z := end). (*val whileM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> - ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e -let rec whileM vars cond body = - cond vars >>= fun cond_val -> - if cond_val then - body vars >>= fun vars -> whileM vars cond body - else return vars - -val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> - ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e -let rec untilM vars cond body = - body vars >>= fun vars -> - cond vars >>= fun cond_val -> - if cond_val then return vars else untilM vars cond body + ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*) +Fixpoint whileMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E := + if Z_ge_dec limit 0 then + cond vars >>= fun cond_val => + if cond_val then + body vars >>= fun vars => whileMT' (limit - 1) vars cond body (_limit_reduces acc) + else returnm vars + else Fail "Termination limit reached". + +Definition whileMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := + whileMT' limit vars cond body (Zwf_guarded limit). + +(*val untilM : forall 'rv 'vars 'e. 'vars -> ('vars -> monad 'rv bool 'e) -> + ('vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e*) +Fixpoint untilMT' {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) (acc : Acc (Zwf 0) limit) : monad RV Vars E := + if Z_ge_dec limit 0 then + body vars >>= fun vars => + cond vars >>= fun cond_val => + if cond_val then returnm vars else untilMT' (limit - 1) vars cond body (_limit_reduces acc) + else Fail "Termination limit reached". + +Definition untilMT {RV Vars E} limit (vars : Vars) (cond : Vars -> monad RV bool E) (body : Vars -> monad RV Vars E) : monad RV Vars E := + untilMT' limit vars cond body (Zwf_guarded limit). (*let write_two_regs r1 r2 vec = let is_inc = @@ -171,8 +181,6 @@ let rec untilM vars cond body = else slice vec (start_vec - size_r1) (start_vec - size_vec) in write_reg r1 r1_v >> write_reg r2 r2_v*) -*) - (* If we need to build an existential after a monadic operation, assume that we can do it entirely from the type. *) diff --git a/lib/isabelle/output/document/Sail2_operators_bitlists.tex b/lib/isabelle/output/document/Sail2_operators_bitlists.tex new file mode 100644 index 00000000..a676b7bf --- /dev/null +++ b/lib/isabelle/output/document/Sail2_operators_bitlists.tex @@ -0,0 +1,1810 @@ +% +\begin{isabellebody}% +\setisabellecontext{Sail{\isadigit{2}}{\isacharunderscore}operators{\isacharunderscore}bitlists}% +% +\isadelimdocument +% +\endisadelimdocument +% +\isatagdocument +% +\isamarkupchapter{Generated by Lem from \isa{{\isachardot}{\isachardot}{\isacharslash}{\isachardot}{\isachardot}{\isacharslash}src{\isacharslash}gen{\isacharunderscore}lib{\isacharslash}sail{\isadigit{2}}{\isacharunderscore}operators{\isacharunderscore}bitlists{\isachardot}lem}.% +} +\isamarkuptrue% +% +\endisatagdocument +{\isafolddocument}% +% +\isadelimdocument +% +\endisadelimdocument +% +\isadelimtheory +% +\endisadelimtheory +% +\isatagtheory +\isacommand{theory}\isamarkupfalse% +\ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}operators{\isacharunderscore}bitlists{\isachardoublequoteclose}\ \isanewline +\isanewline +\isakeyword{imports}\isanewline +\ \ Main\isanewline +\ \ {\isachardoublequoteopen}LEM{\isachardot}Lem{\isacharunderscore}pervasives{\isacharunderscore}extra{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}LEM{\isachardot}Lem{\isacharunderscore}machine{\isacharunderscore}word{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}values{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}operators{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}prompt{\isacharunderscore}monad{\isachardoublequoteclose}\isanewline +\ \ {\isachardoublequoteopen}Sail{\isadigit{2}}{\isacharunderscore}prompt{\isachardoublequoteclose}\isanewline +\isanewline +\isakeyword{begin}\ \isanewline +\isanewline +% +\isamarkupcmt{\isa{open\ import\ Pervasives{\isacharunderscore}extra}% +}\isanewline +% +\isamarkupcmt{\isa{open\ import\ Machine{\isacharunderscore}word}% +}\isanewline +% +\isamarkupcmt{\isa{open\ import\ Sail{\isadigit{2}}{\isacharunderscore}values}% +}\isanewline +% +\isamarkupcmt{\isa{open\ import\ Sail{\isadigit{2}}{\isacharunderscore}operators}% +}\isanewline +% +\isamarkupcmt{\isa{open\ import\ Sail{\isadigit{2}}{\isacharunderscore}prompt{\isacharunderscore}monad}% +}\isanewline +% +\isamarkupcmt{\isa{open\ import\ Sail{\isadigit{2}}{\isacharunderscore}prompt}% +}\isanewline +\isanewline +% +\isamarkupcmt{\isa{Specialisation\ of\ operators\ to\ bit\ lists}% +}\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ uint{\isacharunderscore}maybe\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ integer}% +}% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +\isacommand{definition}\isamarkupfalse% +\ uint{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}int{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ uint{\isacharunderscore}maybe\ v\ {\isacharequal}\ {\isacharparenleft}\ unsigned{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ uint{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}c{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}b{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ uint{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}uint{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}\isanewline +\ \ {\isacharparenleft}unsigned{\isacharunderscore}method\ \ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a{\isacharparenright}\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ uint{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ uint{\isacharunderscore}nondet\ v\ {\isacharequal}\ {\isacharparenleft}\isanewline +\ \ bools{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}nondet\ v\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ bs\ {\isachardot}\ \isanewline +\ \ return\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}bools\ False\ bs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ uint\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ uint\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}failwith\ {\isacharparenleft}uint{\isacharunderscore}maybe\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ sint{\isacharunderscore}maybe\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ integer}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ sint{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}int{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sint{\isacharunderscore}maybe\ v\ {\isacharequal}\ {\isacharparenleft}\ signed{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sint{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}c{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}b{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sint{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}sint{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}\isanewline +\ \ {\isacharparenleft}signed{\isacharunderscore}method\ \ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a{\isacharparenright}\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sint{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sint{\isacharunderscore}nondet\ v\ {\isacharequal}\ {\isacharparenleft}\isanewline +\ \ bools{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}nondet\ v\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ bs\ {\isachardot}\ \isanewline +\ \ return\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}bools\ True\ bs{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sint\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sint\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}failwith\ {\isacharparenleft}sint{\isacharunderscore}maybe\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ extz{\isacharunderscore}vec\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ extz{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ extz{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ extz{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ exts{\isacharunderscore}vec\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ exts{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ exts{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ exts{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ zero{\isacharunderscore}extend\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ zero{\isacharunderscore}extend\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ zero{\isacharunderscore}extend\ bits\ len\ {\isacharequal}\ {\isacharparenleft}\ extz{\isacharunderscore}bits\ len\ bits\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ sign{\isacharunderscore}extend\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ sign{\isacharunderscore}extend\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sign{\isacharunderscore}extend\ bits\ len\ {\isacharequal}\ {\isacharparenleft}\ exts{\isacharunderscore}bits\ len\ bits\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ zeros\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ zeros\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ zeros\ len\ {\isacharequal}\ {\isacharparenleft}\ repeat\ {\isacharbrackleft}B{\isadigit{0}}{\isacharbrackright}\ len\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ vector{\isacharunderscore}truncate\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ vector{\isacharunderscore}truncate\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ vector{\isacharunderscore}truncate\ bs\ len\ {\isacharequal}\ {\isacharparenleft}\ extz{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ len\ bs\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}maybe\ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}% +}\isanewline +% +\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}fail\ \ \ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +% +\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}nondet\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +% +\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}failwith\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bits\ \ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ access{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ access{\isacharunderscore}vec{\isacharunderscore}inc\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ access{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ access{\isacharunderscore}bv{\isacharunderscore}inc\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ access{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ access{\isacharunderscore}vec{\isacharunderscore}dec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ access{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ access{\isacharunderscore}bv{\isacharunderscore}dec\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ update{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}vec{\isacharunderscore}inc\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ update{\isacharunderscore}bv{\isacharunderscore}inc\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}maybe\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}inc\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}fail\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}inc\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}inc{\isacharunderscore}nondet\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}inc\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ update{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}vec{\isacharunderscore}dec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ update{\isacharunderscore}bv{\isacharunderscore}dec\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}maybe\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}dec\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}fail\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}dec\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}vec{\isacharunderscore}dec{\isacharunderscore}nondet\ v\ i\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}update{\isacharunderscore}vec{\isacharunderscore}dec\ v\ i\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ subrange{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ subrange{\isacharunderscore}vec{\isacharunderscore}inc\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ subrange{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ subrange{\isacharunderscore}bv{\isacharunderscore}inc\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ subrange{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ subrange{\isacharunderscore}vec{\isacharunderscore}dec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ subrange{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ subrange{\isacharunderscore}bv{\isacharunderscore}dec\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}inc\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}inc\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ update{\isacharunderscore}subrange{\isacharunderscore}bv{\isacharunderscore}inc\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}dec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}dec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ update{\isacharunderscore}subrange{\isacharunderscore}bv{\isacharunderscore}dec\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ concat{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ concat{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ concat{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ concat{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ cons{\isacharunderscore}vec\ {\isacharcolon}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ cons{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ cons{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ cons{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ cons{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ cons{\isacharunderscore}vec{\isacharunderscore}maybe\ b\ v\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}cons{\isacharunderscore}vec\ b\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ cons{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ cons{\isacharunderscore}vec{\isacharunderscore}fail\ b\ v\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}cons{\isacharunderscore}vec\ b\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ cons{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ cons{\isacharunderscore}vec{\isacharunderscore}nondet\ b\ v\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}cons{\isacharunderscore}vec\ b\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ cast{\isacharunderscore}unit{\isacharunderscore}vec\ {\isacharcolon}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ cast{\isacharunderscore}unit{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ cast{\isacharunderscore}unit{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ cast{\isacharunderscore}unit{\isacharunderscore}bv\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}maybe\ b\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}cast{\isacharunderscore}unit{\isacharunderscore}vec\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}fail\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}cast{\isacharunderscore}unit{\isacharunderscore}vec\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ cast{\isacharunderscore}unit{\isacharunderscore}vec{\isacharunderscore}nondet\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}cast{\isacharunderscore}unit{\isacharunderscore}vec\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ vec{\isacharunderscore}of{\isacharunderscore}bit\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ vec{\isacharunderscore}of{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ vec{\isacharunderscore}of{\isacharunderscore}bit\ {\isacharequal}\ {\isacharparenleft}\ bv{\isacharunderscore}of{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}maybe\ len\ b\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}vec{\isacharunderscore}of{\isacharunderscore}bit\ len\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}fail\ len\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}vec{\isacharunderscore}of{\isacharunderscore}bit\ len\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ vec{\isacharunderscore}of{\isacharunderscore}bit{\isacharunderscore}nondet\ len\ b\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}vec{\isacharunderscore}of{\isacharunderscore}bit\ len\ b{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ msb\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ msb\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ msb\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ most{\isacharunderscore}significant\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ {\isacharcolon}\ bool\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ integer}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bool\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}int{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ int{\isacharunderscore}of{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bool\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}fail\ sign\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}int{\isacharunderscore}of{\isacharunderscore}vec{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ sign\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bool\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}int{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}nondet\ sign\ v\ {\isacharequal}\ {\isacharparenleft}\ bools{\isacharunderscore}of{\isacharunderscore}bits{\isacharunderscore}nondet\ v\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ v\ {\isachardot}\ \ return\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}bools\ sign\ v{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ int{\isacharunderscore}of{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bool\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ int{\isacharunderscore}of{\isacharunderscore}vec\ sign\ v\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}failwith\ {\isacharparenleft}int{\isacharunderscore}of{\isacharunderscore}vec{\isacharunderscore}maybe\ sign\ v{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ string{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ string}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ string{\isacharunderscore}of{\isacharunderscore}bits\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ string\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ string{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ string{\isacharunderscore}of{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ decimal{\isacharunderscore}string{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ string}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ decimal{\isacharunderscore}string{\isacharunderscore}of{\isacharunderscore}bits\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ string\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ decimal{\isacharunderscore}string{\isacharunderscore}of{\isacharunderscore}bits\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ decimal{\isacharunderscore}string{\isacharunderscore}of{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ and{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ or{\isacharunderscore}vec\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ xor{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ not{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ and{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ and{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ binop{\isacharunderscore}list\ and{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ or{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ or{\isacharunderscore}vec\ \ {\isacharequal}\ {\isacharparenleft}\ binop{\isacharunderscore}list\ or{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ xor{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ xor{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ binop{\isacharunderscore}list\ xor{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ not{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ not{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ List{\isachardot}map\ not{\isacharunderscore}bit\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ {\isacharcolon}\ forall\ {\isacharprime}a\ {\isacharprime}b{\isachardot}\ Bitvector\ {\isacharprime}a\ {\isacharequal}{\isachargreater}\ {\isacharparenleft}integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer{\isacharparenright}\ {\isacharminus}{\isachargreater}\ bool\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ {\isacharprime}a\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}{\isacharparenleft}int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int{\isacharparenright}{\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ op{\isadigit{1}}\ sign\ l\ r\ {\isacharequal}\ {\isacharparenleft}\isanewline +\ \ {\isacharparenleft}let\ len\ {\isacharequal}{\isacharparenleft}{\isacharparenleft}\ {\isadigit{2}}\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}\ {\isacharasterisk}\isanewline +\ \ {\isacharparenleft}length{\isacharunderscore}method\ \ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a{\isacharparenright}\ l{\isacharparenright}\ in\isanewline +\ \ {\isacharparenleft}let\ l{\isacharprime}\ {\isacharequal}\ {\isacharparenleft}if\ sign\ then\ exts{\isacharunderscore}bv\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ len\ l\ else\ extz{\isacharunderscore}bv\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ len\ l{\isacharparenright}\ in\isanewline +\ \ {\isacharparenleft}let\ r{\isacharprime}\ {\isacharequal}\ {\isacharparenleft}if\ sign\ then\ exts{\isacharunderscore}bv\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ len\ r\ else\ extz{\isacharunderscore}bv\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ len\ r{\isacharparenright}\ in\isanewline +\ \ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ op{\isadigit{1}}\ sign\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharprime}{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharprime}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ add{\isacharunderscore}vec\ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ adds{\isacharunderscore}vec\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ sub{\isacharunderscore}vec\ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ subs{\isacharunderscore}vec\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mult{\isacharunderscore}vec\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mults{\isacharunderscore}vec\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ add{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec\ \ \ {\isacharequal}\ {\isacharparenleft}\ {\isacharparenleft}{\isasymlambda}\ l\ r{\isachardot}\ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ adds{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec\ \ {\isacharequal}\ {\isacharparenleft}\ {\isacharparenleft}{\isasymlambda}\ l\ r{\isachardot}\ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ True\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sub{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec\ \ \ {\isacharequal}\ {\isacharparenleft}\ {\isacharparenleft}{\isasymlambda}\ l\ r{\isachardot}\ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ subs{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec\ \ {\isacharequal}\ {\isacharparenleft}\ {\isacharparenleft}{\isasymlambda}\ l\ r{\isachardot}\ List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}arith{\isacharunderscore}op{\isacharunderscore}bits\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ True\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ l{\isacharparenright}\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mult{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mult{\isacharunderscore}vec\ \ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}\ {\isacharasterisk}\ {\isacharparenright}\ False\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mults{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mults{\isacharunderscore}vec\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}\ {\isacharasterisk}\ {\isacharparenright}\ True\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ add{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ sub{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mult{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ add{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}int\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sub{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}int\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mult{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mult{\isacharunderscore}vec{\isacharunderscore}int\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}\ {\isacharasterisk}\ {\isacharparenright}\ False\ l\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}bits{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ add{\isacharunderscore}int{\isacharunderscore}vec\ \ \ \ \ \ \ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ sub{\isacharunderscore}int{\isacharunderscore}vec\ \ \ \ \ \ \ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mult{\isacharunderscore}int{\isacharunderscore}vec\ \ \ \ \ \ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ add{\isacharunderscore}int{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}int{\isacharunderscore}vec\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}int{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sub{\isacharunderscore}int{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}int{\isacharunderscore}vec\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}int{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mult{\isacharunderscore}int{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mult{\isacharunderscore}int{\isacharunderscore}vec\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}double{\isacharunderscore}bl\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}\ {\isacharasterisk}\ {\isacharparenright}\ False\ {\isacharparenleft}List{\isachardot}map\ {\isacharparenleft}{\isasymlambda}\ b{\isachardot}\ b{\isacharparenright}\ {\isacharparenleft}bits{\isacharunderscore}of{\isacharunderscore}int\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ r{\isacharparenright}{\isacharparenright}\ l{\isacharparenright}{\isacharparenright}\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ add{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ adds{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ sub{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ subs{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ add{\isacharunderscore}vec{\isacharunderscore}bool\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bool\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bool\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bit\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ r\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ r\ {\isachardot}\ \ return\ {\isacharparenleft}add{\isacharunderscore}vec{\isacharunderscore}bool\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ add{\isacharunderscore}vec{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ add{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}add{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ adds{\isacharunderscore}vec{\isacharunderscore}bool\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bool\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bool\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ True\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bit\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharplus}{\isacharparenright}\ True\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ r\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ r\ {\isachardot}\ \ return\ {\isacharparenleft}adds{\isacharunderscore}vec{\isacharunderscore}bool\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ adds{\isacharunderscore}vec{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ adds{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}adds{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sub{\isacharunderscore}vec{\isacharunderscore}bool\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bool\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bool\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bit\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ False\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ r\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ r\ {\isachardot}\ \ return\ {\isacharparenleft}sub{\isacharunderscore}vec{\isacharunderscore}bool\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ sub{\isacharunderscore}vec{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ sub{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ subs{\isacharunderscore}vec{\isacharunderscore}bool\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ {\isacharprime}a\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bool\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bool\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ True\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}\ {\isacharprime}a\ option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ arith{\isacharunderscore}op{\isacharunderscore}bv{\isacharunderscore}bit\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ {\isacharparenleft}{\isacharminus}{\isacharparenright}\ True\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}fail\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}sub{\isacharunderscore}vec{\isacharunderscore}bit{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ {\isacharprime}a\ Bitvector{\isacharunderscore}class\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}d{\isacharcomma}{\isacharprime}a{\isacharcomma}{\isacharprime}c{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}nondet\ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ r\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ r\ {\isachardot}\ \ return\ {\isacharparenleft}subs{\isacharunderscore}vec{\isacharunderscore}bool\ \isanewline +\ \ dict{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}a\ l\ r{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ subs{\isacharunderscore}vec{\isacharunderscore}bit\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bitU\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ subs{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}subs{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}maybe\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ add{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ sub{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ mult{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ mult{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ let\ add{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ \ {\isacharequal}\ add{\isacharunderscore}overflow{\isacharunderscore}bv\ let\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ \ {\isacharequal}\ add{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}signed\ let\ sub{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ \ {\isacharequal}\ sub{\isacharunderscore}overflow{\isacharunderscore}bv\ let\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ \ {\isacharequal}\ sub{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}signed\ let\ mult{\isacharunderscore}overflow{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharequal}\ mult{\isacharunderscore}overflow{\isacharunderscore}bv\ let\ mult{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}signed\ {\isacharequal}\ mult{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}signed\ \ val\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}signed\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ val\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}signed\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bitU\ {\isacharminus}{\isachargreater}\ {\isacharparenleft}list\ bitU\ {\isacharasterisk}\ bitU\ {\isacharasterisk}\ bitU{\isacharparenright}\ let\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ {\isacharequal}\ add{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}bit\ let\ add{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}signed\ \ {\isacharequal}\ add{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}bit{\isacharunderscore}signed\ let\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit\ \ \ \ \ \ \ \ \ {\isacharequal}\ sub{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}bit\ let\ sub{\isacharunderscore}overflow{\isacharunderscore}vec{\isacharunderscore}bit{\isacharunderscore}signed\ \ {\isacharequal}\ sub{\isacharunderscore}overflow{\isacharunderscore}bv{\isacharunderscore}bit{\isacharunderscore}signed}% +}\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ shiftl\ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ shiftr\ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ arith{\isacharunderscore}shiftr\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ rotl\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ rotr\ \ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ shiftl\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \ \ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ shiftl\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ shiftl{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ shiftr\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \ \ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ shiftr\ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ shiftr{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ arith{\isacharunderscore}shiftr\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ arith{\isacharunderscore}shiftr\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ arith{\isacharunderscore}shiftr{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ rotl\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ rotl\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ rotl{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ rotr\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \ \ \ \ \ \ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ rotr\ \ \ \ \ \ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ rotr{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ mod{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}mod{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mod{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ mod{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mod{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}mod{\isacharunderscore}vec{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}mod{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mod{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}mod{\isacharunderscore}vec\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}% +}\isanewline +% +\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +% +\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ quot{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}quot{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ quot{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ quot{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ quot{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}quot{\isacharunderscore}vec{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}quot{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ quot{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}quot{\isacharunderscore}vec\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ quots{\isacharunderscore}vec\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ quots{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}% +}\isanewline +% +\isamarkupcmt{\isa{val\ quots{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +% +\isamarkupcmt{\isa{val\ quots{\isacharunderscore}vec{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ quots{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quots{\isacharunderscore}vec\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}quots{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ quots{\isacharunderscore}vec{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quots{\isacharunderscore}vec{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ quots{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ quots{\isacharunderscore}vec{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quots{\isacharunderscore}vec{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}quots{\isacharunderscore}vec{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}quots{\isacharunderscore}bv\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ quots{\isacharunderscore}vec{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quots{\isacharunderscore}vec{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}quots{\isacharunderscore}vec\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +% +\isamarkupcmt{\isa{val\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ mod{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}mod{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ mod{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}mod{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ mod{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}mod{\isacharunderscore}vec{\isacharunderscore}int\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +% +\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ maybe\ {\isacharparenleft}list\ bitU{\isacharparenright}}% +}\isanewline +% +\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ \ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +% +\isamarkupcmt{\isa{val\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ {\isacharcolon}\ forall\ {\isacharprime}rv\ {\isacharprime}e{\isachardot}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ monad\ {\isacharprime}rv\ {\isacharparenleft}list\ bitU{\isacharparenright}\ {\isacharprime}e}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ quot{\isacharunderscore}vec{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}int\ \ \ \ \ \ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ case{\isacharunderscore}option\ {\isacharparenleft}repeat\ {\isacharbrackleft}BU{\isacharbrackright}\ {\isacharparenleft}int\ {\isacharparenleft}List{\isachardot}length\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ id\ {\isacharparenleft}quot{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}maybe\ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ quot{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}fail\ \ \ l\ r\ {\isacharequal}\ {\isacharparenleft}\ maybe{\isacharunderscore}fail\ {\isacharparenleft}{\isacharprime}{\isacharprime}quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharprime}{\isacharprime}{\isacharparenright}\ {\isacharparenleft}quot{\isacharunderscore}bv{\isacharunderscore}int\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}rv{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}e{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ quot{\isacharunderscore}vec{\isacharunderscore}int{\isacharunderscore}nondet\ l\ r\ {\isacharequal}\ {\isacharparenleft}\ of{\isacharunderscore}bits{\isacharunderscore}nondet\ \isanewline +\ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenleft}quot{\isacharunderscore}vec{\isacharunderscore}int\ l\ r{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ replicate{\isacharunderscore}bits\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ replicate{\isacharunderscore}bits\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ replicate{\isacharunderscore}bits\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ replicate{\isacharunderscore}bits{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ duplicate\ {\isacharcolon}\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ duplicate\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ duplicate\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ duplicate{\isacharunderscore}bit{\isacharunderscore}bv\ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ duplicate{\isacharunderscore}maybe\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}option\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ duplicate{\isacharunderscore}maybe\ b\ n\ {\isacharequal}\ {\isacharparenleft}\ Some\ {\isacharparenleft}duplicate\ b\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ duplicate{\isacharunderscore}fail\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ duplicate{\isacharunderscore}fail\ b\ n\ {\isacharequal}\ {\isacharparenleft}\ return\ {\isacharparenleft}duplicate\ b\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ duplicate{\isacharunderscore}nondet\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ bitU\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}{\isacharprime}b{\isacharcomma}{\isacharparenleft}{\isacharparenleft}bitU{\isacharparenright}list{\isacharparenright}{\isacharcomma}{\isacharprime}a{\isacharparenright}monad\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ duplicate{\isacharunderscore}nondet\ b\ n\ {\isacharequal}\ {\isacharparenleft}\isanewline +\ \ bool{\isacharunderscore}of{\isacharunderscore}bitU{\isacharunderscore}nondet\ b\ {\isasymbind}\ {\isacharparenleft}{\isasymlambda}\ b\ {\isachardot}\ \isanewline +\ \ return\ {\isacharparenleft}duplicate\ {\isacharparenleft}bitU{\isacharunderscore}of{\isacharunderscore}bool\ b{\isacharparenright}\ n{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ reverse{\isacharunderscore}endianness\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ reverse{\isacharunderscore}endianness\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ reverse{\isacharunderscore}endianness\ v\ {\isacharequal}\ {\isacharparenleft}\ reverse{\isacharunderscore}endianness{\isacharunderscore}list\ v\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ get{\isacharunderscore}slice{\isacharunderscore}int\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ get{\isacharunderscore}slice{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ get{\isacharunderscore}slice{\isacharunderscore}int\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ get{\isacharunderscore}slice{\isacharunderscore}int{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ set{\isacharunderscore}slice{\isacharunderscore}int\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ set{\isacharunderscore}slice{\isacharunderscore}int\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ set{\isacharunderscore}slice{\isacharunderscore}int\ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ set{\isacharunderscore}slice{\isacharunderscore}int{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ slice\ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ slice\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ slice\ v\ lo\ len\ {\isacharequal}\ {\isacharparenleft}\isanewline +\ \ subrange{\isacharunderscore}vec{\isacharunderscore}dec\ v\ {\isacharparenleft}{\isacharparenleft}lo\ {\isacharplus}\ len{\isacharparenright}\ {\isacharminus}{\isacharparenleft}\ {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isacharparenright}\ lo\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ set{\isacharunderscore}slice\ {\isacharcolon}\ integer\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ integer\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ set{\isacharunderscore}slice\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}\ int\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ int\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isachardoublequoteclose}\ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ set{\isacharunderscore}slice\ {\isacharparenleft}out{\isacharunderscore}len{\isacharcolon}{\isacharcolon}ii{\isacharparenright}\ {\isacharparenleft}slice{\isacharunderscore}len{\isacharcolon}{\isacharcolon}ii{\isacharparenright}\ out\ {\isacharparenleft}n{\isacharcolon}{\isacharcolon}ii{\isacharparenright}\ v\ {\isacharequal}\ {\isacharparenleft}\isanewline +\ \ update{\isacharunderscore}subrange{\isacharunderscore}vec{\isacharunderscore}dec\ out\ {\isacharparenleft}{\isacharparenleft}n\ {\isacharplus}\ slice{\isacharunderscore}len{\isacharparenright}\ {\isacharminus}{\isacharparenleft}\ {\isadigit{1}}\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isacharparenright}\ n\ v\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isanewline +% +\isamarkupcmt{\isa{val\ eq{\isacharunderscore}vec\ \ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bool}% +}\isanewline +% +\isamarkupcmt{\isa{val\ neq{\isacharunderscore}vec\ \ \ {\isacharcolon}\ list\ bitU\ {\isacharminus}{\isachargreater}\ list\ bitU\ {\isacharminus}{\isachargreater}\ bool}% +}\isanewline +\isacommand{definition}\isamarkupfalse% +\ eq{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bool\ {\isachardoublequoteclose}\ \ \ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ eq{\isacharunderscore}vec\ \ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ eq{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +\isanewline +\isacommand{definition}\isamarkupfalse% +\ neq{\isacharunderscore}vec\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}{\isacharparenleft}bitU{\isacharparenright}list\ {\isasymRightarrow}\ bool\ {\isachardoublequoteclose}\ \ \ \ \isakeyword{where}\ \isanewline +\ \ \ \ \ {\isachardoublequoteopen}\ neq{\isacharunderscore}vec\ \ \ {\isacharequal}\ {\isacharparenleft}\ \isanewline +\ \ neq{\isacharunderscore}bv\isanewline +\ \ \ \ {\isacharparenleft}instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}Bitvector{\isacharunderscore}list{\isacharunderscore}dict\isanewline +\ \ \ \ \ \ \ instance{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}BitU{\isacharunderscore}Sail{\isadigit{2}}{\isacharunderscore}values{\isacharunderscore}bitU{\isacharunderscore}dict{\isacharparenright}\ {\isacharparenright}{\isachardoublequoteclose}\isanewline +% +\isadelimtheory +\isanewline +% +\endisadelimtheory +% +\isatagtheory +\isacommand{end}\isamarkupfalse% +% +\endisatagtheory +{\isafoldtheory}% +% +\isadelimtheory +% +\endisadelimtheory +% +\end{isabellebody}% +\endinput +%:%file=~/workspace/uni/rems/github/sail/lib/isabelle/Sail2_operators_bitlists.thy%:% +%:%11=1%:% +%:%27=3%:% +%:%28=3%:% +%:%29=4%:% +%:%30=5%:% +%:%31=6%:% +%:%32=7%:% +%:%33=8%:% +%:%34=9%:% +%:%35=10%:% +%:%36=11%:% +%:%37=12%:% +%:%38=13%:% +%:%39=14%:% +%:%40=15%:% +%:%43=16%:% +%:%46=17%:% +%:%49=18%:% +%:%52=19%:% +%:%55=20%:% +%:%58=21%:% +%:%59=22%:% +%:%62=23%:% +%:%63=24%:% +%:%71=25%:% +%:%74=26%:% +%:%75=26%:% +%:%76=27%:% +%:%77=28%:% +%:%78=29%:% +%:%79=29%:% +%:%80=30%:% +%:%81=31%:% +%:%82=32%:% +%:%83=33%:% +%:%84=33%:% +%:%85=34%:% +%:%87=36%:% +%:%88=37%:% +%:%89=38%:% +%:%90=38%:% +%:%91=39%:% +%:%92=40%:% +%:%93=41%:% +%:%96=42%:% +%:%97=43%:% +%:%98=43%:% +%:%99=44%:% +%:%100=45%:% +%:%101=46%:% +%:%102=46%:% +%:%103=47%:% +%:%104=48%:% +%:%105=49%:% +%:%106=50%:% +%:%107=50%:% +%:%108=51%:% +%:%110=53%:% +%:%111=54%:% +%:%112=55%:% +%:%113=55%:% +%:%114=56%:% +%:%115=57%:% +%:%116=58%:% +%:%119=59%:% +%:%120=60%:% +%:%121=60%:% +%:%122=61%:% +%:%125=64%:% +%:%126=65%:% +%:%127=66%:% +%:%130=67%:% +%:%131=68%:% +%:%132=68%:% +%:%133=69%:% +%:%136=72%:% +%:%137=73%:% +%:%138=74%:% +%:%141=75%:% +%:%142=76%:% +%:%143=76%:% +%:%144=77%:% +%:%145=78%:% +%:%146=79%:% +%:%149=80%:% +%:%150=81%:% +%:%151=81%:% +%:%152=82%:% +%:%153=83%:% +%:%154=84%:% +%:%157=85%:% +%:%158=86%:% +%:%159=86%:% +%:%160=87%:% +%:%161=88%:% +%:%162=89%:% +%:%165=90%:% +%:%166=91%:% +%:%167=91%:% +%:%168=92%:% +%:%170=94%:% +%:%171=95%:% +%:%172=96%:% +%:%175=97%:% +%:%178=98%:% +%:%181=99%:% +%:%184=100%:% +%:%187=101%:% +%:%188=102%:% +%:%191=103%:% +%:%192=104%:% +%:%193=104%:% +%:%194=105%:% +%:%197=108%:% +%:%198=109%:% +%:%199=110%:% +%:%202=111%:% +%:%203=112%:% +%:%204=112%:% +%:%205=113%:% +%:%208=116%:% +%:%209=117%:% +%:%210=118%:% +%:%213=119%:% +%:%214=120%:% +%:%215=120%:% +%:%216=121%:% +%:%219=124%:% +%:%220=125%:% +%:%221=126%:% +%:%222=126%:% +%:%223=127%:% +%:%224=128%:% +%:%225=129%:% +%:%226=129%:% +%:%227=130%:% +%:%228=131%:% +%:%229=132%:% +%:%230=132%:% +%:%231=133%:% +%:%232=134%:% +%:%233=135%:% +%:%236=136%:% +%:%237=137%:% +%:%238=137%:% +%:%239=138%:% +%:%242=141%:% +%:%243=142%:% +%:%244=143%:% +%:%245=143%:% +%:%246=144%:% +%:%247=145%:% +%:%248=146%:% +%:%249=146%:% +%:%250=147%:% +%:%251=148%:% +%:%252=149%:% +%:%253=149%:% +%:%254=150%:% +%:%255=151%:% +%:%256=152%:% +%:%259=153%:% +%:%260=154%:% +%:%261=154%:% +%:%262=155%:% +%:%265=158%:% +%:%266=159%:% +%:%267=160%:% +%:%270=161%:% +%:%271=162%:% +%:%272=162%:% +%:%273=163%:% +%:%276=166%:% +%:%277=167%:% +%:%278=168%:% +%:%281=169%:% +%:%282=170%:% +%:%283=170%:% +%:%284=171%:% +%:%289=176%:% +%:%290=177%:% +%:%291=178%:% +%:%294=179%:% +%:%295=180%:% +%:%296=180%:% +%:%297=181%:% +%:%302=186%:% +%:%303=187%:% +%:%304=188%:% +%:%307=189%:% +%:%308=190%:% +%:%309=190%:% +%:%310=191%:% +%:%315=196%:% +%:%316=197%:% +%:%317=198%:% +%:%320=199%:% +%:%321=200%:% +%:%322=200%:% +%:%323=201%:% +%:%326=204%:% +%:%327=205%:% +%:%328=206%:% +%:%329=206%:% +%:%330=207%:% +%:%331=208%:% +%:%332=209%:% +%:%333=209%:% +%:%334=210%:% +%:%335=211%:% +%:%336=212%:% +%:%337=212%:% +%:%338=213%:% +%:%339=214%:% +%:%340=215%:% +%:%343=216%:% +%:%344=217%:% +%:%345=217%:% +%:%346=218%:% +%:%347=219%:% +%:%348=220%:% +%:%349=220%:% +%:%350=221%:% +%:%351=222%:% +%:%352=223%:% +%:%353=223%:% +%:%354=224%:% +%:%355=225%:% +%:%356=226%:% +%:%357=226%:% +%:%358=227%:% +%:%359=228%:% +%:%360=229%:% +%:%363=230%:% +%:%364=231%:% +%:%365=231%:% +%:%366=232%:% +%:%367=233%:% +%:%368=234%:% +%:%369=234%:% +%:%370=235%:% +%:%371=236%:% +%:%372=237%:% +%:%373=237%:% +%:%374=238%:% +%:%375=239%:% +%:%376=240%:% +%:%377=240%:% +%:%378=241%:% +%:%379=242%:% +%:%380=243%:% +%:%383=244%:% +%:%384=245%:% +%:%385=245%:% +%:%386=246%:% +%:%389=249%:% +%:%390=250%:% +%:%391=251%:% +%:%394=252%:% +%:%395=253%:% +%:%396=253%:% +%:%397=254%:% +%:%400=257%:% +%:%401=258%:% +%:%402=259%:% +%:%403=259%:% +%:%404=260%:% +%:%405=261%:% +%:%406=262%:% +%:%407=262%:% +%:%408=263%:% +%:%409=264%:% +%:%410=265%:% +%:%411=265%:% +%:%412=266%:% +%:%413=267%:% +%:%414=268%:% +%:%417=269%:% +%:%418=270%:% +%:%419=270%:% +%:%420=271%:% +%:%423=274%:% +%:%424=275%:% +%:%425=276%:% +%:%428=277%:% +%:%429=278%:% +%:%430=278%:% +%:%431=279%:% +%:%434=282%:% +%:%435=283%:% +%:%436=284%:% +%:%439=285%:% +%:%442=286%:% +%:%445=287%:% +%:%448=288%:% +%:%449=289%:% +%:%450=289%:% +%:%451=290%:% +%:%452=291%:% +%:%453=292%:% +%:%454=292%:% +%:%455=293%:% +%:%456=294%:% +%:%457=295%:% +%:%458=295%:% +%:%459=296%:% +%:%460=297%:% +%:%461=298%:% +%:%462=298%:% +%:%463=299%:% +%:%464=300%:% +%:%465=301%:% +%:%468=303%:% +%:%469=304%:% +%:%470=304%:% +%:%471=305%:% +%:%478=312%:% +%:%479=313%:% +%:%480=314%:% +%:%483=315%:% +%:%486=316%:% +%:%489=317%:% +%:%492=318%:% +%:%495=319%:% +%:%498=320%:% +%:%499=321%:% +%:%500=321%:% +%:%501=322%:% +%:%502=323%:% +%:%503=324%:% +%:%504=324%:% +%:%505=325%:% +%:%506=326%:% +%:%507=327%:% +%:%508=327%:% +%:%509=328%:% +%:%510=329%:% +%:%511=330%:% +%:%512=330%:% +%:%513=331%:% +%:%514=332%:% +%:%515=333%:% +%:%516=333%:% +%:%517=334%:% +%:%519=336%:% +%:%520=337%:% +%:%521=338%:% +%:%522=338%:% +%:%523=339%:% +%:%525=341%:% +%:%526=342%:% +%:%527=343%:% +%:%530=344%:% +%:%533=345%:% +%:%536=346%:% +%:%537=347%:% +%:%538=347%:% +%:%539=348%:% +%:%541=350%:% +%:%542=351%:% +%:%543=352%:% +%:%544=352%:% +%:%545=353%:% +%:%547=355%:% +%:%548=356%:% +%:%549=357%:% +%:%550=357%:% +%:%551=358%:% +%:%553=360%:% +%:%554=361%:% +%:%555=362%:% +%:%558=363%:% +%:%561=364%:% +%:%564=365%:% +%:%565=366%:% +%:%566=366%:% +%:%567=367%:% +%:%569=369%:% +%:%570=370%:% +%:%571=371%:% +%:%572=371%:% +%:%573=372%:% +%:%575=374%:% +%:%576=375%:% +%:%577=376%:% +%:%578=376%:% +%:%579=377%:% +%:%581=379%:% +%:%582=380%:% +%:%583=381%:% +%:%586=382%:% +%:%589=383%:% +%:%592=384%:% +%:%595=385%:% +%:%596=386%:% +%:%597=387%:% +%:%598=387%:% +%:%599=388%:% +%:%600=389%:% +%:%601=390%:% +%:%602=391%:% +%:%603=391%:% +%:%604=392%:% +%:%605=393%:% +%:%606=394%:% +%:%607=395%:% +%:%608=395%:% +%:%609=396%:% +%:%610=397%:% +%:%611=398%:% +%:%612=399%:% +%:%613=399%:% +%:%614=400%:% +%:%615=401%:% +%:%616=402%:% +%:%617=403%:% +%:%618=403%:% +%:%619=404%:% +%:%621=406%:% +%:%622=407%:% +%:%623=408%:% +%:%624=409%:% +%:%625=409%:% +%:%626=410%:% +%:%627=411%:% +%:%628=412%:% +%:%629=413%:% +%:%630=413%:% +%:%631=414%:% +%:%632=415%:% +%:%633=416%:% +%:%634=417%:% +%:%635=417%:% +%:%636=418%:% +%:%637=419%:% +%:%638=420%:% +%:%639=421%:% +%:%640=421%:% +%:%641=422%:% +%:%642=423%:% +%:%643=424%:% +%:%644=425%:% +%:%645=425%:% +%:%646=426%:% +%:%648=428%:% +%:%649=429%:% +%:%650=430%:% +%:%651=431%:% +%:%652=431%:% +%:%653=432%:% +%:%654=433%:% +%:%655=434%:% +%:%656=435%:% +%:%657=435%:% +%:%658=436%:% +%:%659=437%:% +%:%660=438%:% +%:%661=439%:% +%:%662=439%:% +%:%663=440%:% +%:%664=441%:% +%:%665=442%:% +%:%666=443%:% +%:%667=443%:% +%:%668=444%:% +%:%669=445%:% +%:%670=446%:% +%:%671=447%:% +%:%672=447%:% +%:%673=448%:% +%:%675=450%:% +%:%676=451%:% +%:%677=452%:% +%:%678=453%:% +%:%679=453%:% +%:%680=454%:% +%:%681=455%:% +%:%682=456%:% +%:%683=457%:% +%:%684=457%:% +%:%685=458%:% +%:%686=459%:% +%:%687=460%:% +%:%688=461%:% +%:%689=461%:% +%:%690=462%:% +%:%691=463%:% +%:%692=464%:% +%:%693=465%:% +%:%694=465%:% +%:%695=466%:% +%:%696=467%:% +%:%697=468%:% +%:%698=469%:% +%:%699=469%:% +%:%700=470%:% +%:%702=472%:% +%:%703=473%:% +%:%704=474%:% +%:%707=495%:% +%:%708=496%:% +%:%711=497%:% +%:%714=498%:% +%:%717=499%:% +%:%720=500%:% +%:%723=501%:% +%:%724=502%:% +%:%725=502%:% +%:%726=503%:% +%:%729=506%:% +%:%730=507%:% +%:%731=508%:% +%:%732=508%:% +%:%733=509%:% +%:%736=512%:% +%:%737=513%:% +%:%738=514%:% +%:%739=514%:% +%:%740=515%:% +%:%743=518%:% +%:%744=519%:% +%:%745=520%:% +%:%746=520%:% +%:%747=521%:% +%:%750=524%:% +%:%751=525%:% +%:%752=526%:% +%:%753=526%:% +%:%754=527%:% +%:%757=530%:% +%:%758=531%:% +%:%759=532%:% +%:%762=533%:% +%:%765=534%:% +%:%768=535%:% +%:%771=536%:% +%:%772=537%:% +%:%773=537%:% +%:%774=538%:% +%:%777=541%:% +%:%778=542%:% +%:%779=543%:% +%:%780=543%:% +%:%781=544%:% +%:%784=547%:% +%:%785=548%:% +%:%786=549%:% +%:%787=549%:% +%:%788=550%:% +%:%791=553%:% +%:%792=554%:% +%:%793=555%:% +%:%794=555%:% +%:%795=556%:% +%:%797=558%:% +%:%798=559%:% +%:%799=560%:% +%:%802=561%:% +%:%805=562%:% +%:%808=563%:% +%:%811=564%:% +%:%812=565%:% +%:%813=565%:% +%:%814=566%:% +%:%817=569%:% +%:%818=570%:% +%:%819=571%:% +%:%820=571%:% +%:%821=572%:% +%:%824=575%:% +%:%825=576%:% +%:%826=577%:% +%:%827=577%:% +%:%828=578%:% +%:%831=581%:% +%:%832=582%:% +%:%833=583%:% +%:%834=583%:% +%:%835=584%:% +%:%837=586%:% +%:%838=587%:% +%:%839=588%:% +%:%842=589%:% +%:%845=590%:% +%:%848=591%:% +%:%851=592%:% +%:%852=593%:% +%:%853=593%:% +%:%854=594%:% +%:%857=597%:% +%:%858=598%:% +%:%859=599%:% +%:%860=599%:% +%:%861=600%:% +%:%864=603%:% +%:%865=604%:% +%:%866=605%:% +%:%867=605%:% +%:%868=606%:% +%:%871=609%:% +%:%872=610%:% +%:%873=611%:% +%:%874=611%:% +%:%875=612%:% +%:%877=614%:% +%:%878=615%:% +%:%879=616%:% +%:%882=617%:% +%:%885=618%:% +%:%888=619%:% +%:%891=620%:% +%:%892=621%:% +%:%893=621%:% +%:%894=622%:% +%:%897=625%:% +%:%898=626%:% +%:%899=627%:% +%:%900=627%:% +%:%901=628%:% +%:%904=631%:% +%:%905=632%:% +%:%906=633%:% +%:%907=633%:% +%:%908=634%:% +%:%911=637%:% +%:%912=638%:% +%:%913=639%:% +%:%914=639%:% +%:%915=640%:% +%:%917=642%:% +%:%918=643%:% +%:%919=644%:% +%:%922=645%:% +%:%925=646%:% +%:%928=647%:% +%:%931=648%:% +%:%932=649%:% +%:%933=649%:% +%:%934=650%:% +%:%937=653%:% +%:%938=654%:% +%:%939=655%:% +%:%940=655%:% +%:%941=656%:% +%:%944=659%:% +%:%945=660%:% +%:%946=661%:% +%:%947=661%:% +%:%948=662%:% +%:%951=665%:% +%:%952=666%:% +%:%953=667%:% +%:%954=667%:% +%:%955=668%:% +%:%957=670%:% +%:%958=671%:% +%:%959=672%:% +%:%962=673%:% +%:%963=674%:% +%:%964=674%:% +%:%965=675%:% +%:%968=678%:% +%:%969=679%:% +%:%970=680%:% +%:%973=681%:% +%:%974=682%:% +%:%975=682%:% +%:%976=683%:% +%:%977=684%:% +%:%978=685%:% +%:%979=686%:% +%:%980=686%:% +%:%981=687%:% +%:%982=688%:% +%:%983=689%:% +%:%984=689%:% +%:%985=690%:% +%:%986=691%:% +%:%987=692%:% +%:%988=692%:% +%:%989=693%:% +%:%991=695%:% +%:%992=696%:% +%:%993=697%:% +%:%996=698%:% +%:%997=699%:% +%:%998=699%:% +%:%999=700%:% +%:%1000=701%:% +%:%1001=702%:% +%:%1004=703%:% +%:%1005=704%:% +%:%1006=704%:% +%:%1007=705%:% +%:%1010=708%:% +%:%1011=709%:% +%:%1012=710%:% +%:%1015=711%:% +%:%1016=712%:% +%:%1017=712%:% +%:%1018=713%:% +%:%1021=716%:% +%:%1022=717%:% +%:%1023=718%:% +%:%1026=719%:% +%:%1027=720%:% +%:%1028=720%:% +%:%1029=721%:% +%:%1030=722%:% +%:%1031=723%:% +%:%1032=724%:% +%:%1035=725%:% +%:%1036=726%:% +%:%1037=726%:% +%:%1038=727%:% +%:%1039=728%:% +%:%1040=729%:% +%:%1041=730%:% +%:%1044=731%:% +%:%1047=732%:% +%:%1048=733%:% +%:%1049=733%:% +%:%1050=734%:% +%:%1053=737%:% +%:%1054=738%:% +%:%1055=739%:% +%:%1056=739%:% +%:%1057=740%:% +%:%1060=743%:% +%:%1063=744%:% +%:%1068=745%:%
\ No newline at end of file |