diff options
| author | Peter Sewell | 2018-07-27 18:16:52 +0100 |
|---|---|---|
| committer | Peter Sewell | 2018-07-27 18:16:52 +0100 |
| commit | 4c84c70eafbbf9bea475e3264f21eedc3555021f (patch) | |
| tree | 549c7898e945144e032c3c8e2f21ef943dfeddce /cheri/sail_latexcc | |
| parent | 6e80b938e5e72edebb1953602ba4d40f668e7426 (diff) | |
wib
Diffstat (limited to 'cheri/sail_latexcc')
272 files changed, 0 insertions, 1165 deletions
diff --git a/cheri/sail_latexcc/commands.tex b/cheri/sail_latexcc/commands.tex deleted file mode 100644 index 8b9678a1..00000000 --- a/cheri/sail_latexcc/commands.tex +++ /dev/null @@ -1,544 +0,0 @@ -\newcommand{\sailccsailccregderefv}{\label{zregzyderef} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccregderefv.tex}} - -\newcommand{\sailccregderef}{\label{zzyregzyderef} \lstinputlisting[language=sail]{sail_latexcc/sailccregderef.tex}} - -\newcommand{\sailcceqbittwo}{\label{zeqzybittwo} \lstinputlisting[language=sail]{sail_latexcc/sailcceqbittwo.tex}} - -\newcommand{\sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv}{\label{zzeightoperatorzzerozJzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv.tex}} - -\newcommand{\sailccdiv}{\label{zdiv} \lstinputlisting[language=sail]{sail_latexcc/sailccdiv.tex}} - -\newcommand{\sailccsailccsailcczeightoperatorzzerozFzninevv}{\label{zzeightoperatorzzerozFznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailcczeightoperatorzzerozFzninevv.tex}} - -\newcommand{\sailccmod}{\label{zmod} \lstinputlisting[language=sail]{sail_latexcc/sailccmod.tex}} - -\newcommand{\sailccsailccsailcczeightoperatorzzerozfivezninevv}{\label{zzeightoperatorzzerozfiveznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailcczeightoperatorzzerozfivezninevv.tex}} - -\newcommand{\sailccabsatom}{\label{zabszyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccabsatom.tex}} - -\newcommand{\sailccnotbool}{\label{znotzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccnotbool.tex}} - -\newcommand{\sailccandbool}{\label{zandzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccandbool.tex}} - -\newcommand{\sailccorbool}{\label{zorzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccorbool.tex}} - -\newcommand{\sailcceqatom}{\label{zeqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailcceqatom.tex}} - -\newcommand{\sailccneqatom}{\label{zneqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccneqatom.tex}} - -\newcommand{\sailccfnneqatom}{\label{zneqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqatom.tex}} - -\newcommand{\sailcclteqatom}{\label{zlteqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailcclteqatom.tex}} - -\newcommand{\sailccgteqatom}{\label{zgteqzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccgteqatom.tex}} - -\newcommand{\sailccltatom}{\label{zltzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccltatom.tex}} - -\newcommand{\sailccgtatom}{\label{zgtzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccgtatom.tex}} - -\newcommand{\sailccltrangeatom}{\label{zltzyrangezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccltrangeatom.tex}} - -\newcommand{\sailcclteqrangeatom}{\label{zlteqzyrangezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailcclteqrangeatom.tex}} - -\newcommand{\sailccgtrangeatom}{\label{zgtzyrangezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccgtrangeatom.tex}} - -\newcommand{\sailccgteqrangeatom}{\label{zgteqzyrangezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccgteqrangeatom.tex}} - -\newcommand{\sailccltatomrange}{\label{zltzyatomzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccltatomrange.tex}} - -\newcommand{\sailcclteqatomrange}{\label{zlteqzyatomzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailcclteqatomrange.tex}} - -\newcommand{\sailccgtatomrange}{\label{zgtzyatomzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccgtatomrange.tex}} - -\newcommand{\sailccgteqatomrange}{\label{zgteqzyatomzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccgteqatomrange.tex}} - -\newcommand{\sailcceqrange}{\label{zeqzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailcceqrange.tex}} - -\newcommand{\sailcceqint}{\label{zeqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailcceqint.tex}} - -\newcommand{\sailcceqbool}{\label{zeqzybool} \lstinputlisting[language=sail]{sail_latexcc/sailcceqbool.tex}} - -\newcommand{\sailccneqrange}{\label{zneqzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccneqrange.tex}} - -\newcommand{\sailccfnneqrange}{\label{zneqzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqrange.tex}} - -\newcommand{\sailccneqint}{\label{zneqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccneqint.tex}} - -\newcommand{\sailccfnneqint}{\label{zneqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqint.tex}} - -\newcommand{\sailccneqbool}{\label{zneqzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccneqbool.tex}} - -\newcommand{\sailccfnneqbool}{\label{zneqzybool} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqbool.tex}} - -\newcommand{\sailcclteqint}{\label{zlteqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailcclteqint.tex}} - -\newcommand{\sailccgteqint}{\label{zgteqzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccgteqint.tex}} - -\newcommand{\sailccltint}{\label{zltzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccltint.tex}} - -\newcommand{\sailccgtint}{\label{zgtzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccgtint.tex}} - -\newcommand{\sailccsailccsailcczeightoperatorzzerozJzJzninevv}{\label{zzeightoperatorzzerozJzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozonezJzninev}{\label{zzeightoperatorzzerozonezJznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozUzninev}{\label{zzeightoperatorzzerozUznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozsixzninev}{\label{zzeightoperatorzzerozsixznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozsixzninev.tex}} - -\newcommand{\sailcczeightoperatorzzerozIzJznine}{\label{zzeightoperatorzzerozIzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIzJznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozIznine}{\label{zzeightoperatorzzerozIznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozKzJznine}{\label{zzeightoperatorzzerozKzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzJznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozKznine}{\label{zzeightoperatorzzerozKznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKznine.tex}} - -\newcommand{\sailccaddatom}{\label{zaddzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccaddatom.tex}} - -\newcommand{\sailccaddint}{\label{zaddzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccaddint.tex}} - -\newcommand{\sailccsailccsailcczeightoperatorzzerozBzninevv}{\label{zzeightoperatorzzerozBznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex}} - -\newcommand{\sailccsubatom}{\label{zsubzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccsubatom.tex}} - -\newcommand{\sailccsubint}{\label{zsubzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccsubint.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozDzninev}{\label{zzeightoperatorzzerozDznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozDzninev.tex}} - -\newcommand{\sailccnegateatom}{\label{znegatezyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccnegateatom.tex}} - -\newcommand{\sailccnegateint}{\label{znegatezyint} \lstinputlisting[language=sail]{sail_latexcc/sailccnegateint.tex}} - -\newcommand{\sailccsailccnegatev}{\label{znegate} \lstinputlisting[language=sail]{sail_latexcc/sailccsailccnegatev.tex}} - -\newcommand{\sailccmultatom}{\label{zmultzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccmultatom.tex}} - -\newcommand{\sailccmultint}{\label{zmultzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccmultint.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozAzninev}{\label{zzeightoperatorzzerozAznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex}} - -\newcommand{\sailccprintint}{\label{zprintzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccprintint.tex}} - -\newcommand{\sailccprerrint}{\label{zprerrzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccprerrint.tex}} - -\newcommand{\sailccshlint}{\label{zshlzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccshlint.tex}} - -\newcommand{\sailccshrint}{\label{zshrzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccshrint.tex}} - -\newcommand{\sailccdivint}{\label{zdivzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccdivint.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozFzninev}{\label{zzeightoperatorzzerozFznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozFzninev.tex}} - -\newcommand{\sailccmodint}{\label{zmodzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccmodint.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozfivezninev}{\label{zzeightoperatorzzerozfiveznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex}} - -\newcommand{\sailccabsint}{\label{zabszyint} \lstinputlisting[language=sail]{sail_latexcc/sailccabsint.tex}} - -\newcommand{\sailccisnone}{\label{ziszynone} \lstinputlisting[language=sail]{sail_latexcc/sailccisnone.tex}} - -\newcommand{\sailccfnisnone}{\label{ziszynone} \lstinputlisting[language=sail]{sail_latexcc/sailccfnisnone.tex}} - -\newcommand{\sailccissome}{\label{ziszysome} \lstinputlisting[language=sail]{sail_latexcc/sailccissome.tex}} - -\newcommand{\sailccfnissome}{\label{ziszysome} \lstinputlisting[language=sail]{sail_latexcc/sailccfnissome.tex}} - -\newcommand{\sailccbits}{\label{zbits} \lstinputlisting[language=sail]{sail_latexcc/sailccbits.tex}} - -\newcommand{\sailcceqbit}{\label{zeqzybit} \lstinputlisting[language=sail]{sail_latexcc/sailcceqbit.tex}} - -\newcommand{\sailcceqbits}{\label{zeqzybits} \lstinputlisting[language=sail]{sail_latexcc/sailcceqbits.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozJzJzninev}{\label{zzeightoperatorzzerozJzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex}} - -\newcommand{\sailccbitvectorlength}{\label{zbitvectorzylength} \lstinputlisting[language=sail]{sail_latexcc/sailccbitvectorlength.tex}} - -\newcommand{\sailccvectorlength}{\label{zvectorzylength} \lstinputlisting[language=sail]{sail_latexcc/sailccvectorlength.tex}} - -\newcommand{\sailcclength}{\label{zlength} \lstinputlisting[language=sail]{sail_latexcc/sailcclength.tex}} - -\newcommand{\sailccsailzzeros}{\label{zsailzyzzeros} \lstinputlisting[language=sail]{sail_latexcc/sailccsailzzeros.tex}} - -\newcommand{\sailccprintbits}{\label{zprintzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccprintbits.tex}} - -\newcommand{\sailccprerrbits}{\label{zprerrzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccprerrbits.tex}} - -\newcommand{\sailccsailsignextend}{\label{zsailzysignzyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccsailsignextend.tex}} - -\newcommand{\sailccsailzzeroextend}{\label{zsailzyzzerozyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccsailzzeroextend.tex}} - -\newcommand{\sailcctruncate}{\label{ztruncate} \lstinputlisting[language=sail]{sail_latexcc/sailcctruncate.tex}} - -\newcommand{\sailccsailmask}{\label{zsailzymask} \lstinputlisting[language=sail]{sail_latexcc/sailccsailmask.tex}} - -\newcommand{\sailccfnsailmask}{\label{zsailzymask} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsailmask.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozQzninev}{\label{zzeightoperatorzzerozQznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozQzninev.tex}} - -\newcommand{\sailccbitvectorconcat}{\label{zbitvectorzyconcat} \lstinputlisting[language=sail]{sail_latexcc/sailccbitvectorconcat.tex}} - -\newcommand{\sailccappend}{\label{zappend} \lstinputlisting[language=sail]{sail_latexcc/sailccappend.tex}} - -\newcommand{\sailccappendsixfour}{\label{zappendzysixfour} \lstinputlisting[language=sail]{sail_latexcc/sailccappendsixfour.tex}} - -\newcommand{\sailccbitvectoraccess}{\label{zbitvectorzyaccess} \lstinputlisting[language=sail]{sail_latexcc/sailccbitvectoraccess.tex}} - -\newcommand{\sailccplainvectoraccess}{\label{zplainzyvectorzyaccess} \lstinputlisting[language=sail]{sail_latexcc/sailccplainvectoraccess.tex}} - -\newcommand{\sailccvectoraccess}{\label{zvectorzyaccess} \lstinputlisting[language=sail]{sail_latexcc/sailccvectoraccess.tex}} - -\newcommand{\sailccbitvectorupdate}{\label{zbitvectorzyupdate} \lstinputlisting[language=sail]{sail_latexcc/sailccbitvectorupdate.tex}} - -\newcommand{\sailccplainvectorupdate}{\label{zplainzyvectorzyupdate} \lstinputlisting[language=sail]{sail_latexcc/sailccplainvectorupdate.tex}} - -\newcommand{\sailccvectorupdate}{\label{zvectorzyupdate} \lstinputlisting[language=sail]{sail_latexcc/sailccvectorupdate.tex}} - -\newcommand{\sailccaddbits}{\label{zaddzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccaddbits.tex}} - -\newcommand{\sailccaddbitsint}{\label{zaddzybitszyint} \lstinputlisting[language=sail]{sail_latexcc/sailccaddbitsint.tex}} - -\newcommand{\sailccsailcczeightoperatorzzerozBzninev}{\label{zzeightoperatorzzerozBznine} \lstinputlisting[language=sail]{sail_latexcc/sailccsailcczeightoperatorzzerozBzninev.tex}} - -\newcommand{\sailccvectorsubrange}{\label{zvectorzysubrange} \lstinputlisting[language=sail]{sail_latexcc/sailccvectorsubrange.tex}} - -\newcommand{\sailccvectorupdatesubrange}{\label{zvectorzyupdatezysubrange} \lstinputlisting[language=sail]{sail_latexcc/sailccvectorupdatesubrange.tex}} - -\newcommand{\sailccgetsliceint}{\label{zgetzyslicezyint} \lstinputlisting[language=sail]{sail_latexcc/sailccgetsliceint.tex}} - -\newcommand{\sailccsetsliceint}{\label{zsetzyslicezyint} \lstinputlisting[language=sail]{sail_latexcc/sailccsetsliceint.tex}} - -\newcommand{\sailccsetslicebits}{\label{zsetzyslicezybits} \lstinputlisting[language=sail]{sail_latexcc/sailccsetslicebits.tex}} - -\newcommand{\sailccslice}{\label{zslice} \lstinputlisting[language=sail]{sail_latexcc/sailccslice.tex}} - -\newcommand{\sailccreplicatebits}{\label{zreplicatezybits} \lstinputlisting[language=sail]{sail_latexcc/sailccreplicatebits.tex}} - -\newcommand{\sailccunsigned}{\label{zunsigned} \lstinputlisting[language=sail]{sail_latexcc/sailccunsigned.tex}} - -\newcommand{\sailccsigned}{\label{zsigned} \lstinputlisting[language=sail]{sail_latexcc/sailccsigned.tex}} - -\newcommand{\sailcceqanything}{\label{zeqzyanything} \lstinputlisting[language=sail]{sail_latexcc/sailcceqanything.tex}} - -\newcommand{\sailcczeightoperatorzzerozJzJznine}{\label{zzeightoperatorzzerozJzJznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozJzJznine.tex}} - -\newcommand{\sailccnotvec}{\label{znotzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccnotvec.tex}} - -\newcommand{\sailcczW}{\label{zzW} \lstinputlisting[language=sail]{sail_latexcc/sailcczW.tex}} - -\newcommand{\sailccnot}{\label{znot} \lstinputlisting[language=sail]{sail_latexcc/sailccnot.tex}} - -\newcommand{\sailccneqvec}{\label{zneqzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccneqvec.tex}} - -\newcommand{\sailccfnneqvec}{\label{zneqzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqvec.tex}} - -\newcommand{\sailccneqanything}{\label{zneqzyanything} \lstinputlisting[language=sail]{sail_latexcc/sailccneqanything.tex}} - -\newcommand{\sailccfnneqanything}{\label{zneqzyanything} \lstinputlisting[language=sail]{sail_latexcc/sailccfnneqanything.tex}} - -\newcommand{\sailcczeightoperatorzzerozonezJznine}{\label{zzeightoperatorzzerozonezJznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex}} - -\newcommand{\sailccandbits}{\label{zandzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccandbits.tex}} - -\newcommand{\sailcczeightoperatorzzerozsixznine}{\label{zzeightoperatorzzerozsixznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozsixznine.tex}} - -\newcommand{\sailccorbits}{\label{zorzybits} \lstinputlisting[language=sail]{sail_latexcc/sailccorbits.tex}} - -\newcommand{\sailcczeightoperatorzzerozUznine}{\label{zzeightoperatorzzerozUznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozUznine.tex}} - -\newcommand{\sailcccastunitvec}{\label{zcastzyunitzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailcccastunitvec.tex}} - -\newcommand{\sailccfncastunitvec}{\label{zcastzyunitzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccfncastunitvec.tex}} - -\newcommand{\sailccprint}{\label{zprint} \lstinputlisting[language=sail]{sail_latexcc/sailccprint.tex}} - -\newcommand{\sailccprerrendline}{\label{zprerrzyendline} \lstinputlisting[language=sail]{sail_latexcc/sailccprerrendline.tex}} - -\newcommand{\sailccprerrstring}{\label{zprerrzystring} \lstinputlisting[language=sail]{sail_latexcc/sailccprerrstring.tex}} - -\newcommand{\sailccputchar}{\label{zputchar} \lstinputlisting[language=sail]{sail_latexcc/sailccputchar.tex}} - -\newcommand{\sailccconcatstr}{\label{zconcatzystr} \lstinputlisting[language=sail]{sail_latexcc/sailccconcatstr.tex}} - -\newcommand{\sailccstringofint}{\label{zstringzyofzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccstringofint.tex}} - -\newcommand{\sailccBitStr}{\label{zBitStr} \lstinputlisting[language=sail]{sail_latexcc/sailccBitStr.tex}} - -\newcommand{\sailccxorvec}{\label{zxorzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccxorvec.tex}} - -\newcommand{\sailccintpower}{\label{zintzypower} \lstinputlisting[language=sail]{sail_latexcc/sailccintpower.tex}} - -\newcommand{\sailcczeightoperatorzzerozQznine}{\label{zzeightoperatorzzerozQznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozQznine.tex}} - -\newcommand{\sailccaddrange}{\label{zaddzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccaddrange.tex}} - -\newcommand{\sailccaddvec}{\label{zaddzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccaddvec.tex}} - -\newcommand{\sailccaddvecint}{\label{zaddzyveczyint} \lstinputlisting[language=sail]{sail_latexcc/sailccaddvecint.tex}} - -\newcommand{\sailcczeightoperatorzzerozBznine}{\label{zzeightoperatorzzerozBznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozBznine.tex}} - -\newcommand{\sailccsubrange}{\label{zsubzyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccsubrange.tex}} - -\newcommand{\sailccsubvec}{\label{zsubzyvec} \lstinputlisting[language=sail]{sail_latexcc/sailccsubvec.tex}} - -\newcommand{\sailccsubvecint}{\label{zsubzyveczyint} \lstinputlisting[language=sail]{sail_latexcc/sailccsubvecint.tex}} - -\newcommand{\sailccnegaterange}{\label{znegatezyrange} \lstinputlisting[language=sail]{sail_latexcc/sailccnegaterange.tex}} - -\newcommand{\sailcczeightoperatorzzerozDznine}{\label{zzeightoperatorzzerozDznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozDznine.tex}} - -\newcommand{\sailccnegate}{\label{znegate} \lstinputlisting[language=sail]{sail_latexcc/sailccnegate.tex}} - -\newcommand{\sailcczeightoperatorzzerozAznine}{\label{zzeightoperatorzzerozAznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozAznine.tex}} - -\newcommand{\sailccquotientnat}{\label{zquotientzynat} \lstinputlisting[language=sail]{sail_latexcc/sailccquotientnat.tex}} - -\newcommand{\sailccquotient}{\label{zquotient} \lstinputlisting[language=sail]{sail_latexcc/sailccquotient.tex}} - -\newcommand{\sailcczeightoperatorzzerozFznine}{\label{zzeightoperatorzzerozFznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozFznine.tex}} - -\newcommand{\sailccquotroundzzero}{\label{zquotzyroundzyzzero} \lstinputlisting[language=sail]{sail_latexcc/sailccquotroundzzero.tex}} - -\newcommand{\sailccremroundzzero}{\label{zremzyroundzyzzero} \lstinputlisting[language=sail]{sail_latexcc/sailccremroundzzero.tex}} - -\newcommand{\sailccmodulus}{\label{zmodulus} \lstinputlisting[language=sail]{sail_latexcc/sailccmodulus.tex}} - -\newcommand{\sailcczeightoperatorzzerozfiveznine}{\label{zzeightoperatorzzerozfiveznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozfiveznine.tex}} - -\newcommand{\sailccminnat}{\label{zminzynat} \lstinputlisting[language=sail]{sail_latexcc/sailccminnat.tex}} - -\newcommand{\sailccminint}{\label{zminzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccminint.tex}} - -\newcommand{\sailccmaxnat}{\label{zmaxzynat} \lstinputlisting[language=sail]{sail_latexcc/sailccmaxnat.tex}} - -\newcommand{\sailccmaxint}{\label{zmaxzyint} \lstinputlisting[language=sail]{sail_latexcc/sailccmaxint.tex}} - -\newcommand{\sailccminatom}{\label{zminzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccminatom.tex}} - -\newcommand{\sailccmaxatom}{\label{zmaxzyatom} \lstinputlisting[language=sail]{sail_latexcc/sailccmaxatom.tex}} - -\newcommand{\sailccmin}{\label{zmin} \lstinputlisting[language=sail]{sail_latexcc/sailccmin.tex}} - -\newcommand{\sailccmax}{\label{zmax} \lstinputlisting[language=sail]{sail_latexcc/sailccmax.tex}} - -\newcommand{\sailccWriteRAM}{\label{zzyzyWriteRAM} \lstinputlisting[language=sail]{sail_latexcc/sailccWriteRAM.tex}} - -\newcommand{\sailccMIPSwrite}{\label{zzyzyMIPSzywrite} \lstinputlisting[language=sail]{sail_latexcc/sailccMIPSwrite.tex}} - -\newcommand{\sailccfnMIPSwrite}{\label{zzyzyMIPSzywrite} \lstinputlisting[language=sail]{sail_latexcc/sailccfnMIPSwrite.tex}} - -\newcommand{\sailccReadRAM}{\label{zzyzyReadRAM} \lstinputlisting[language=sail]{sail_latexcc/sailccReadRAM.tex}} - -\newcommand{\sailccMIPSread}{\label{zzyzyMIPSzyread} \lstinputlisting[language=sail]{sail_latexcc/sailccMIPSread.tex}} - -\newcommand{\sailccfnMIPSread}{\label{zzyzyMIPSzyread} \lstinputlisting[language=sail]{sail_latexcc/sailccfnMIPSread.tex}} - -\newcommand{\sailcczeightoperatorzzerozQzQznine}{\label{zzeightoperatorzzerozQzQznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozQzQznine.tex}} - -\newcommand{\sailccfnzeightoperatorzzerozQzQznine}{\label{zzeightoperatorzzerozQzQznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozQzQznine.tex}} - -\newcommand{\sailccpowtwo}{\label{zpowtwo} \lstinputlisting[language=sail]{sail_latexcc/sailccpowtwo.tex}} - -\newcommand{\sailccmipssignextend}{\label{zmipszysignzyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccmipssignextend.tex}} - -\newcommand{\sailccmipszzeroextend}{\label{zmipszyzzerozyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccmipszzeroextend.tex}} - -\newcommand{\sailccfnmipssignextend}{\label{zmipszysignzyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmipssignextend.tex}} - -\newcommand{\sailccfnmipszzeroextend}{\label{zmipszyzzerozyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmipszzeroextend.tex}} - -\newcommand{\sailccsignextend}{\label{zsignzyextend} \lstinputlisting[language=sail]{sail_latexcc/sailccsignextend.tex}} - -\newcommand{\sailcczzeroextend}{\label{zzzerozyextend} \lstinputlisting[language=sail]{sail_latexcc/sailcczzeroextend.tex}} - -\newcommand{\sailcczzeros}{\label{zzzeros} \lstinputlisting[language=sail]{sail_latexcc/sailcczzeros.tex}} - -\newcommand{\sailccfnzzeros}{\label{zzzeros} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzzeros.tex}} - -\newcommand{\sailccones}{\label{zones} \lstinputlisting[language=sail]{sail_latexcc/sailccones.tex}} - -\newcommand{\sailccfnones}{\label{zones} \lstinputlisting[language=sail]{sail_latexcc/sailccfnones.tex}} - -\newcommand{\sailcczeightoperatorzzerozIsznine}{\label{zzeightoperatorzzerozIzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIsznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozKzJsznine}{\label{zzeightoperatorzzerozKzJzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozIuznine}{\label{zzeightoperatorzzerozIzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIuznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozKzJuznine}{\label{zzeightoperatorzzerozKzJzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzJuznine.tex}} - -\newcommand{\sailccfnzeightoperatorzzerozIsznine}{\label{zzeightoperatorzzerozIzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozIsznine.tex}} - -\newcommand{\sailccfnzeightoperatorzzerozKzJsznine}{\label{zzeightoperatorzzerozKzJzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozKzJsznine.tex}} - -\newcommand{\sailccfnzeightoperatorzzerozIuznine}{\label{zzeightoperatorzzerozIzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozIuznine.tex}} - -\newcommand{\sailccfnzeightoperatorzzerozKzJuznine}{\label{zzeightoperatorzzerozKzJzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailccfnzeightoperatorzzerozKzJuznine.tex}} - -\newcommand{\sailccbooltobits}{\label{zboolzytozybits} \lstinputlisting[language=sail]{sail_latexcc/sailccbooltobits.tex}} - -\newcommand{\sailccfnbooltobits}{\label{zboolzytozybits} \lstinputlisting[language=sail]{sail_latexcc/sailccfnbooltobits.tex}} - -\newcommand{\sailccbittobool}{\label{zbitzytozybool} \lstinputlisting[language=sail]{sail_latexcc/sailccbittobool.tex}} - -\newcommand{\sailccfnbittobool}{\label{zbitzytozybool} \lstinputlisting[language=sail]{sail_latexcc/sailccfnbittobool.tex}} - -\newcommand{\sailccbitstobool}{\label{zbitszytozybool} \lstinputlisting[language=sail]{sail_latexcc/sailccbitstobool.tex}} - -\newcommand{\sailccfnbitstobool}{\label{zbitszytozybool} \lstinputlisting[language=sail]{sail_latexcc/sailccfnbitstobool.tex}} - -\newcommand{\sailccshiftbitsright}{\label{zshiftzybitszyright} \lstinputlisting[language=sail]{sail_latexcc/sailccshiftbitsright.tex}} - -\newcommand{\sailccshiftbitsleft}{\label{zshiftzybitszyleft} \lstinputlisting[language=sail]{sail_latexcc/sailccshiftbitsleft.tex}} - -\newcommand{\sailccshiftl}{\label{zshiftl} \lstinputlisting[language=sail]{sail_latexcc/sailccshiftl.tex}} - -\newcommand{\sailccshiftr}{\label{zshiftr} \lstinputlisting[language=sail]{sail_latexcc/sailccshiftr.tex}} - -\newcommand{\sailcczeightoperatorzzerozKzKznine}{\label{zzeightoperatorzzerozKzKznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzKznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozIzIznine}{\label{zzeightoperatorzzerozIzIznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozIzIznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozKzKsznine}{\label{zzeightoperatorzzerozKzKzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozKzKsznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozAsznine}{\label{zzeightoperatorzzerozAzysznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozAsznine.tex}} - -\newcommand{\sailcczeightoperatorzzerozAuznine}{\label{zzeightoperatorzzerozAzyuznine} \lstinputlisting[language=sail]{sail_latexcc/sailcczeightoperatorzzerozAuznine.tex}} - -\newcommand{\sailcctobits}{\label{ztozybits} -\function{to\_bits} converts an integer to a bit vector of given length. If the integer is negative a twos-complement representation is used. If the integer is too large (or too negative) to fit in the requested length then it is truncated to the least significant bits. -\lstinputlisting[language=sail]{sail_latexcc/sailcctobits.tex}} - -\newcommand{\sailccfntobits}{\label{ztozybits} \lstinputlisting[language=sail]{sail_latexcc/sailccfntobits.tex}} - -\newcommand{\sailccmask}{\label{zmask} \lstinputlisting[language=sail]{sail_latexcc/sailccmask.tex}} - -\newcommand{\sailccfnmask}{\label{zmask} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmask.tex}} - -\newcommand{\sailccgettimens}{\label{zgetzytimezyns} \lstinputlisting[language=sail]{sail_latexcc/sailccgettimens.tex}} - -\newcommand{\sailccCapLen}{\label{zCapLen} \lstinputlisting[language=sail]{sail_latexcc/sailccCapLen.tex}} - -\newcommand{\sailccuintsixfour}{\label{zuintsixfour} \lstinputlisting[language=sail]{sail_latexcc/sailccuintsixfour.tex}} - -\newcommand{\sailccCPtrCmpOp}{\label{zCPtrCmpOp} \lstinputlisting[language=sail]{sail_latexcc/sailccCPtrCmpOp.tex}} - -\newcommand{\sailccCPtrCmpOpofnum}{\label{zCPtrCmpOpzyofzynum} \lstinputlisting[language=sail]{sail_latexcc/sailccCPtrCmpOpofnum.tex}} - -\newcommand{\sailccfnCPtrCmpOpofnum}{\label{zCPtrCmpOpzyofzynum} \lstinputlisting[language=sail]{sail_latexcc/sailccfnCPtrCmpOpofnum.tex}} - -\newcommand{\sailccnumofCPtrCmpOp}{\label{znumzyofzyCPtrCmpOp} \lstinputlisting[language=sail]{sail_latexcc/sailccnumofCPtrCmpOp.tex}} - -\newcommand{\sailccfnnumofCPtrCmpOp}{\label{znumzyofzyCPtrCmpOp} \lstinputlisting[language=sail]{sail_latexcc/sailccfnnumofCPtrCmpOp.tex}} - -\newcommand{\sailccClearRegSet}{\label{zClearRegSet} \lstinputlisting[language=sail]{sail_latexcc/sailccClearRegSet.tex}} - -\newcommand{\sailccClearRegSetofnum}{\label{zClearRegSetzyofzynum} \lstinputlisting[language=sail]{sail_latexcc/sailccClearRegSetofnum.tex}} - -\newcommand{\sailccfnClearRegSetofnum}{\label{zClearRegSetzyofzynum} \lstinputlisting[language=sail]{sail_latexcc/sailccfnClearRegSetofnum.tex}} - -\newcommand{\sailccnumofClearRegSet}{\label{znumzyofzyClearRegSet} \lstinputlisting[language=sail]{sail_latexcc/sailccnumofClearRegSet.tex}} - -\newcommand{\sailccfnnumofClearRegSet}{\label{znumzyofzyClearRegSet} \lstinputlisting[language=sail]{sail_latexcc/sailccfnnumofClearRegSet.tex}} - -\newcommand{\sailccCapReg}{\label{zCapReg} \lstinputlisting[language=sail]{sail_latexcc/sailccCapReg.tex}} - -\newcommand{\sailccCapStruct}{\label{zCapStruct} \lstinputlisting[language=sail]{sail_latexcc/sailccCapStruct.tex}} - -\newcommand{\sailcccapRegToCapStruct}{\label{zcapRegToCapStruct} \lstinputlisting[language=sail]{sail_latexcc/sailcccapRegToCapStruct.tex}} - -\newcommand{\sailccfncapRegToCapStruct}{\label{zcapRegToCapStruct} \lstinputlisting[language=sail]{sail_latexcc/sailccfncapRegToCapStruct.tex}} - -\newcommand{\sailccgetCapHardPerms}{\label{zgetCapHardPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapHardPerms.tex}} - -\newcommand{\sailccfngetCapHardPerms}{\label{zgetCapHardPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapHardPerms.tex}} - -\newcommand{\sailcccapStructToMemBitsonetwoeight}{\label{zcapStructToMemBitsonetwoeight} \lstinputlisting[language=sail]{sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex}} - -\newcommand{\sailccfncapStructToMemBitsonetwoeight}{\label{zcapStructToMemBitsonetwoeight} \lstinputlisting[language=sail]{sail_latexcc/sailccfncapStructToMemBitsonetwoeight.tex}} - -\newcommand{\sailcccapStructToCapReg}{\label{zcapStructToCapReg} \lstinputlisting[language=sail]{sail_latexcc/sailcccapStructToCapReg.tex}} - -\newcommand{\sailccfncapStructToCapReg}{\label{zcapStructToCapReg} \lstinputlisting[language=sail]{sail_latexcc/sailccfncapStructToCapReg.tex}} - -\newcommand{\sailccmemBitsToCapBitsonetwoeight}{\label{zmemBitsToCapBitsonetwoeight} \lstinputlisting[language=sail]{sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex}} - -\newcommand{\sailccfnmemBitsToCapBitsonetwoeight}{\label{zmemBitsToCapBitsonetwoeight} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmemBitsToCapBitsonetwoeight.tex}} - -\newcommand{\sailcccapStructToMemBits}{\label{zcapStructToMemBits} \lstinputlisting[language=sail]{sail_latexcc/sailcccapStructToMemBits.tex}} - -\newcommand{\sailccfncapStructToMemBits}{\label{zcapStructToMemBits} \lstinputlisting[language=sail]{sail_latexcc/sailccfncapStructToMemBits.tex}} - -\newcommand{\sailccmemBitsToCapBits}{\label{zmemBitsToCapBits} \lstinputlisting[language=sail]{sail_latexcc/sailccmemBitsToCapBits.tex}} - -\newcommand{\sailccfnmemBitsToCapBits}{\label{zmemBitsToCapBits} \lstinputlisting[language=sail]{sail_latexcc/sailccfnmemBitsToCapBits.tex}} - -\newcommand{\sailccgetCapPerms}{\label{zgetCapPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapPerms.tex}} - -\newcommand{\sailccfngetCapPerms}{\label{zgetCapPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapPerms.tex}} - -\newcommand{\sailccsetCapPerms}{\label{zsetCapPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccsetCapPerms.tex}} - -\newcommand{\sailccfnsetCapPerms}{\label{zsetCapPerms} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsetCapPerms.tex}} - -\newcommand{\sailccsealCap}{\label{zsealCap} \lstinputlisting[language=sail]{sail_latexcc/sailccsealCap.tex}} - -\newcommand{\sailccfnsealCap}{\label{zsealCap} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsealCap.tex}} - -\newcommand{\sailccatopcorrection}{\label{zazytopzycorrection} \lstinputlisting[language=sail]{sail_latexcc/sailccatopcorrection.tex}} - -\newcommand{\sailccfnatopcorrection}{\label{zazytopzycorrection} \lstinputlisting[language=sail]{sail_latexcc/sailccfnatopcorrection.tex}} - -\newcommand{\sailccgetCapBase}{\label{zgetCapBase} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapBase.tex}} - -\newcommand{\sailccfngetCapBase}{\label{zgetCapBase} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapBase.tex}} - -\newcommand{\sailccgetCapTop}{\label{zgetCapTop} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapTop.tex}} - -\newcommand{\sailccfngetCapTop}{\label{zgetCapTop} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapTop.tex}} - -\newcommand{\sailccgetCapOffset}{\label{zgetCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapOffset.tex}} - -\newcommand{\sailccfngetCapOffset}{\label{zgetCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapOffset.tex}} - -\newcommand{\sailccgetCapLength}{\label{zgetCapLength} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapLength.tex}} - -\newcommand{\sailccfngetCapLength}{\label{zgetCapLength} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapLength.tex}} - -\newcommand{\sailccgetCapCursor}{\label{zgetCapCursor} \lstinputlisting[language=sail]{sail_latexcc/sailccgetCapCursor.tex}} - -\newcommand{\sailccfngetCapCursor}{\label{zgetCapCursor} \lstinputlisting[language=sail]{sail_latexcc/sailccfngetCapCursor.tex}} - -\newcommand{\sailccfastRepCheck}{\label{zfastRepCheck} \lstinputlisting[language=sail]{sail_latexcc/sailccfastRepCheck.tex}} - -\newcommand{\sailccfnfastRepCheck}{\label{zfastRepCheck} \lstinputlisting[language=sail]{sail_latexcc/sailccfnfastRepCheck.tex}} - -\newcommand{\sailccsetCapOffset}{\label{zsetCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccsetCapOffset.tex}} - -\newcommand{\sailccfnsetCapOffset}{\label{zsetCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsetCapOffset.tex}} - -\newcommand{\sailccincCapOffset}{\label{zincCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccincCapOffset.tex}} - -\newcommand{\sailccfnincCapOffset}{\label{zincCapOffset} \lstinputlisting[language=sail]{sail_latexcc/sailccfnincCapOffset.tex}} - -\newcommand{\sailccHighestSetBit}{\label{zHighestSetBit} \lstinputlisting[language=sail]{sail_latexcc/sailccHighestSetBit.tex}} - -\newcommand{\sailccfnHighestSetBit}{\label{zHighestSetBit} \lstinputlisting[language=sail]{sail_latexcc/sailccfnHighestSetBit.tex}} - -\newcommand{\sailccroundUp}{\label{zroundUp} \lstinputlisting[language=sail]{sail_latexcc/sailccroundUp.tex}} - -\newcommand{\sailccfnroundUp}{\label{zroundUp} \lstinputlisting[language=sail]{sail_latexcc/sailccfnroundUp.tex}} - -\newcommand{\sailcccomputeE}{\label{zcomputeE} \lstinputlisting[language=sail]{sail_latexcc/sailcccomputeE.tex}} - -\newcommand{\sailccfncomputeE}{\label{zcomputeE} \lstinputlisting[language=sail]{sail_latexcc/sailccfncomputeE.tex}} - -\newcommand{\sailccsetCapBounds}{\label{zsetCapBounds} \lstinputlisting[language=sail]{sail_latexcc/sailccsetCapBounds.tex}} - -\newcommand{\sailccfnsetCapBounds}{\label{zsetCapBounds} \lstinputlisting[language=sail]{sail_latexcc/sailccfnsetCapBounds.tex}} - -\newcommand{\sailccinttocap}{\label{zintzytozycap} \lstinputlisting[language=sail]{sail_latexcc/sailccinttocap.tex}} - -\newcommand{\sailccfninttocap}{\label{zintzytozycap} \lstinputlisting[language=sail]{sail_latexcc/sailccfninttocap.tex}} - diff --git a/cheri/sail_latexcc/sailccBitStr.tex b/cheri/sail_latexcc/sailccBitStr.tex deleted file mode 100644 index a0d408ab..00000000 --- a/cheri/sail_latexcc/sailccBitStr.tex +++ /dev/null @@ -1 +0,0 @@ -val BitStr = "string_of_bits" : forall 'n. #\hyperref[zbits]{bits}#('n) -> string diff --git a/cheri/sail_latexcc/sailccCPtrCmpOp.tex b/cheri/sail_latexcc/sailccCPtrCmpOp.tex deleted file mode 100644 index cb0a73ae..00000000 --- a/cheri/sail_latexcc/sailccCPtrCmpOp.tex +++ /dev/null @@ -1,10 +0,0 @@ -enum CPtrCmpOp = { - CEQ, - CNE, - CLT, - CLE, - CLTU, - CLEU, - CEXEQ, - CNEXEQ -} diff --git a/cheri/sail_latexcc/sailccCPtrCmpOpofnum.tex b/cheri/sail_latexcc/sailccCPtrCmpOpofnum.tex deleted file mode 100644 index bd6ca31c..00000000 --- a/cheri/sail_latexcc/sailccCPtrCmpOpofnum.tex +++ /dev/null @@ -1 +0,0 @@ -val CPtrCmpOp_of_num : forall ('e : Int), 0 <= 'e & 'e <= 7. atom('e) -> CPtrCmpOp diff --git a/cheri/sail_latexcc/sailccCapLen.tex b/cheri/sail_latexcc/sailccCapLen.tex deleted file mode 100644 index 812f45ff..00000000 --- a/cheri/sail_latexcc/sailccCapLen.tex +++ /dev/null @@ -1 +0,0 @@ -type CapLen = range(0, 2 ^ 65) diff --git a/cheri/sail_latexcc/sailccCapReg.tex b/cheri/sail_latexcc/sailccCapReg.tex deleted file mode 100644 index 702141d9..00000000 --- a/cheri/sail_latexcc/sailccCapReg.tex +++ /dev/null @@ -1 +0,0 @@ -type CapReg = #\hyperref[zbits]{bits}#(129) diff --git a/cheri/sail_latexcc/sailccCapStruct.tex b/cheri/sail_latexcc/sailccCapStruct.tex deleted file mode 100644 index b1df7ec5..00000000 --- a/cheri/sail_latexcc/sailccCapStruct.tex +++ /dev/null @@ -1,22 +0,0 @@ -struct CapStruct = { - tag : bool , - uperms : #\hyperref[zbits]{bits}#(4) , - access_system_regs : bool , - permit_unseal : bool , - permit_ccall : bool , - permit_seal : bool , - permit_store_local_cap : bool , - permit_store_cap : bool , - permit_load_cap : bool , - permit_store : bool , - permit_load : bool , - permit_execute : bool , - global : bool , - reserved : #\hyperref[zbits]{bits}#(2) , - E : #\hyperref[zbits]{bits}#(6) , - sealed : bool , - B : #\hyperref[zbits]{bits}#(20), - T : #\hyperref[zbits]{bits}#(20), - otype : #\hyperref[zbits]{bits}#(24), - address : #\hyperref[zbits]{bits}#(64) -} diff --git a/cheri/sail_latexcc/sailccClearRegSet.tex b/cheri/sail_latexcc/sailccClearRegSet.tex deleted file mode 100644 index c04ea7d4..00000000 --- a/cheri/sail_latexcc/sailccClearRegSet.tex +++ /dev/null @@ -1,6 +0,0 @@ -enum ClearRegSet = { -GPLo, -GPHi, -CLo, -CHi -} diff --git a/cheri/sail_latexcc/sailccClearRegSetofnum.tex b/cheri/sail_latexcc/sailccClearRegSetofnum.tex deleted file mode 100644 index c73d36d9..00000000 --- a/cheri/sail_latexcc/sailccClearRegSetofnum.tex +++ /dev/null @@ -1 +0,0 @@ -val ClearRegSet_of_num : forall ('e : Int), 0 <= 'e & 'e <= 3. atom('e) -> ClearRegSet diff --git a/cheri/sail_latexcc/sailccHighestSetBit.tex b/cheri/sail_latexcc/sailccHighestSetBit.tex deleted file mode 100644 index eb8a5e36..00000000 --- a/cheri/sail_latexcc/sailccHighestSetBit.tex +++ /dev/null @@ -1 +0,0 @@ -val HighestSetBit : forall 'N , 'N >= 2. #\hyperref[zbits]{bits}#('N) -> {'n, 0 <= 'n < 'N . (bool, atom('n))} diff --git a/cheri/sail_latexcc/sailccMIPSread.tex b/cheri/sail_latexcc/sailccMIPSread.tex deleted file mode 100644 index 92ca59cc..00000000 --- a/cheri/sail_latexcc/sailccMIPSread.tex +++ /dev/null @@ -1 +0,0 @@ -val __MIPS_read : forall 'n, 'n >= 0. (#\hyperref[zbits]{bits}#(64), atom('n)) -> #\hyperref[zbits]{bits}#(8 * 'n) effect {rmem} diff --git a/cheri/sail_latexcc/sailccMIPSwrite.tex b/cheri/sail_latexcc/sailccMIPSwrite.tex deleted file mode 100644 index cc67fa20..00000000 --- a/cheri/sail_latexcc/sailccMIPSwrite.tex +++ /dev/null @@ -1 +0,0 @@ -val __MIPS_write : forall 'n. (#\hyperref[zbits]{bits}#(64), atom('n), #\hyperref[zbits]{bits}#(8 * 'n)) -> unit effect {wmv} diff --git a/cheri/sail_latexcc/sailccReadRAM.tex b/cheri/sail_latexcc/sailccReadRAM.tex deleted file mode 100644 index 68d629a6..00000000 --- a/cheri/sail_latexcc/sailccReadRAM.tex +++ /dev/null @@ -1,2 +0,0 @@ -val __ReadRAM = "read_ram" : forall 'n 'm, 'n >= 0. - (atom('m), atom('n), #\hyperref[zbits]{bits}#('m), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#(8 * 'n) effect {rmem} diff --git a/cheri/sail_latexcc/sailccWriteRAM.tex b/cheri/sail_latexcc/sailccWriteRAM.tex deleted file mode 100644 index 2ed4aca2..00000000 --- a/cheri/sail_latexcc/sailccWriteRAM.tex +++ /dev/null @@ -1,2 +0,0 @@ -val __WriteRAM = "write_ram" : forall 'n 'm. - (atom('m), atom('n), #\hyperref[zbits]{bits}#('m), #\hyperref[zbits]{bits}#('m), #\hyperref[zbits]{bits}#(8 * 'n)) -> bool effect {wmv} diff --git a/cheri/sail_latexcc/sailccabsatom.tex b/cheri/sail_latexcc/sailccabsatom.tex deleted file mode 100644 index 5164ef32..00000000 --- a/cheri/sail_latexcc/sailccabsatom.tex +++ /dev/null @@ -1,7 +0,0 @@ -val abs_atom = { - smt : "abs", - ocaml: "abs_int", - lem: "abs_int", - c: "abs_int", - coq: "abs_with_eq" -} : forall 'n. atom('n) -> {'o, 'o = #\hyperref[zabszyatom]{abs\_atom}#('n). atom('o)} diff --git a/cheri/sail_latexcc/sailccabsint.tex b/cheri/sail_latexcc/sailccabsint.tex deleted file mode 100644 index d3b67cfb..00000000 --- a/cheri/sail_latexcc/sailccabsint.tex +++ /dev/null @@ -1,6 +0,0 @@ -val abs_int = { - smt : "abs", - ocaml: "abs_int", - lem: "abs_int", - coq: "Z.abs" -} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccaddatom.tex b/cheri/sail_latexcc/sailccaddatom.tex deleted file mode 100644 index 8b6ac810..00000000 --- a/cheri/sail_latexcc/sailccaddatom.tex +++ /dev/null @@ -1,2 +0,0 @@ -val add_atom = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : forall 'n 'm. - (atom('n), atom('m)) -> atom('n + 'm) diff --git a/cheri/sail_latexcc/sailccaddbits.tex b/cheri/sail_latexcc/sailccaddbits.tex deleted file mode 100644 index 95f653d1..00000000 --- a/cheri/sail_latexcc/sailccaddbits.tex +++ /dev/null @@ -1,6 +0,0 @@ -val add_bits = { - ocaml: "add_vec", - lem: "add_vec", - c: "add_bits", - coq: "add_vec" -} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccaddbitsint.tex b/cheri/sail_latexcc/sailccaddbitsint.tex deleted file mode 100644 index ee9a8aa2..00000000 --- a/cheri/sail_latexcc/sailccaddbitsint.tex +++ /dev/null @@ -1,6 +0,0 @@ -val add_bits_int = { - ocaml: "add_vec_int", - lem: "add_vec_int", - c: "add_bits_int", - coq: "add_vec_int" -} : forall 'n. (#\hyperref[zbits]{bits}#('n), int) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccaddint.tex b/cheri/sail_latexcc/sailccaddint.tex deleted file mode 100644 index 9fe5b078..00000000 --- a/cheri/sail_latexcc/sailccaddint.tex +++ /dev/null @@ -1 +0,0 @@ -val add_int = {ocaml: "add_int", lem: "integerAdd", c: "add_int", coq: "Z.add"} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccaddrange.tex b/cheri/sail_latexcc/sailccaddrange.tex deleted file mode 100644 index fbf498b1..00000000 --- a/cheri/sail_latexcc/sailccaddrange.tex +++ /dev/null @@ -1,2 +0,0 @@ -val add_range = {ocaml: "add_int", lem: "integerAdd", coq: "add_range", c: "add_int"} : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n + 'o, 'm + 'p) diff --git a/cheri/sail_latexcc/sailccaddvec.tex b/cheri/sail_latexcc/sailccaddvec.tex deleted file mode 100644 index bb625afe..00000000 --- a/cheri/sail_latexcc/sailccaddvec.tex +++ /dev/null @@ -1 +0,0 @@ -val add_vec = "add_vec" : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccaddvecint.tex b/cheri/sail_latexcc/sailccaddvecint.tex deleted file mode 100644 index 189ad4aa..00000000 --- a/cheri/sail_latexcc/sailccaddvecint.tex +++ /dev/null @@ -1 +0,0 @@ -val add_vec_int = "add_vec_int" : forall 'n. (#\hyperref[zbits]{bits}#('n), int) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccandbits.tex b/cheri/sail_latexcc/sailccandbits.tex deleted file mode 100644 index 8e35bd5b..00000000 --- a/cheri/sail_latexcc/sailccandbits.tex +++ /dev/null @@ -1 +0,0 @@ -val and_bits = {c:"and_bits", _: "and_vec"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccandbool.tex b/cheri/sail_latexcc/sailccandbool.tex deleted file mode 100644 index 926dce9f..00000000 --- a/cheri/sail_latexcc/sailccandbool.tex +++ /dev/null @@ -1 +0,0 @@ -val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool diff --git a/cheri/sail_latexcc/sailccappend.tex b/cheri/sail_latexcc/sailccappend.tex deleted file mode 100644 index 56c12116..00000000 --- a/cheri/sail_latexcc/sailccappend.tex +++ /dev/null @@ -1 +0,0 @@ -overload append = {bitvector_concat}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccappendsixfour.tex b/cheri/sail_latexcc/sailccappendsixfour.tex deleted file mode 100644 index 633593b3..00000000 --- a/cheri/sail_latexcc/sailccappendsixfour.tex +++ /dev/null @@ -1 +0,0 @@ -val "append_64" : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#(64)) -> #\hyperref[zbits]{bits}#('n + 64) diff --git a/cheri/sail_latexcc/sailccatopcorrection.tex b/cheri/sail_latexcc/sailccatopcorrection.tex deleted file mode 100644 index 13bbaf7b..00000000 --- a/cheri/sail_latexcc/sailccatopcorrection.tex +++ /dev/null @@ -1 +0,0 @@ -val a_top_correction : (bits(20), bits(20), bits(20)) -> bits(65) diff --git a/cheri/sail_latexcc/sailccbits.tex b/cheri/sail_latexcc/sailccbits.tex deleted file mode 100644 index 88255b5a..00000000 --- a/cheri/sail_latexcc/sailccbits.tex +++ /dev/null @@ -1 +0,0 @@ -type #\hyperref[zbits]{bits}# ('n : Int) = vector('n, dec, bit) diff --git a/cheri/sail_latexcc/sailccbitstobool.tex b/cheri/sail_latexcc/sailccbitstobool.tex deleted file mode 100644 index 17cb3483..00000000 --- a/cheri/sail_latexcc/sailccbitstobool.tex +++ /dev/null @@ -1 +0,0 @@ -val cast bits_to_bool : #\hyperref[zbits]{bits}#(1) -> bool diff --git a/cheri/sail_latexcc/sailccbittobool.tex b/cheri/sail_latexcc/sailccbittobool.tex deleted file mode 100644 index 13a2dfb8..00000000 --- a/cheri/sail_latexcc/sailccbittobool.tex +++ /dev/null @@ -1 +0,0 @@ -val cast bit_to_bool : bit -> bool diff --git a/cheri/sail_latexcc/sailccbitvectoraccess.tex b/cheri/sail_latexcc/sailccbitvectoraccess.tex deleted file mode 100644 index 4bb98eb8..00000000 --- a/cheri/sail_latexcc/sailccbitvectoraccess.tex +++ /dev/null @@ -1,6 +0,0 @@ -val bitvector_access = { - ocaml: "access", - lem: "access_vec_dec", - coq: "access_vec_dec", - c: "vector_access" -} : forall ('n : Int), 'n >= 0. (#\hyperref[zbits]{bits}#('n), int) -> bit diff --git a/cheri/sail_latexcc/sailccbitvectorconcat.tex b/cheri/sail_latexcc/sailccbitvectorconcat.tex deleted file mode 100644 index afc03901..00000000 --- a/cheri/sail_latexcc/sailccbitvectorconcat.tex +++ /dev/null @@ -1,2 +0,0 @@ -val bitvector_concat = {ocaml: "append", lem: "concat_vec", c: "append", coq: "concat_vec"} : forall ('n : Int) ('m : Int). - (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n + 'm) diff --git a/cheri/sail_latexcc/sailccbitvectorlength.tex b/cheri/sail_latexcc/sailccbitvectorlength.tex deleted file mode 100644 index ac601acd..00000000 --- a/cheri/sail_latexcc/sailccbitvectorlength.tex +++ /dev/null @@ -1 +0,0 @@ -val bitvector_length = {coq: "length_mword", _:"length"} : forall 'n. #\hyperref[zbits]{bits}#('n) -> atom('n) diff --git a/cheri/sail_latexcc/sailccbitvectorupdate.tex b/cheri/sail_latexcc/sailccbitvectorupdate.tex deleted file mode 100644 index 6524146e..00000000 --- a/cheri/sail_latexcc/sailccbitvectorupdate.tex +++ /dev/null @@ -1,6 +0,0 @@ -val bitvector_update = { - ocaml: "update", - lem: "update_vec_dec", - coq: "update_vec_dec", - c: "vector_update" -} : forall 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('n), int, bit) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccbooltobits.tex b/cheri/sail_latexcc/sailccbooltobits.tex deleted file mode 100644 index 711ab763..00000000 --- a/cheri/sail_latexcc/sailccbooltobits.tex +++ /dev/null @@ -1 +0,0 @@ -val cast bool_to_bits : bool -> #\hyperref[zbits]{bits}#(1) diff --git a/cheri/sail_latexcc/sailcccapRegToCapStruct.tex b/cheri/sail_latexcc/sailcccapRegToCapStruct.tex deleted file mode 100644 index bd64d554..00000000 --- a/cheri/sail_latexcc/sailcccapRegToCapStruct.tex +++ /dev/null @@ -1 +0,0 @@ -val capRegToCapStruct : CapReg -> CapStruct diff --git a/cheri/sail_latexcc/sailcccapStructToCapReg.tex b/cheri/sail_latexcc/sailcccapStructToCapReg.tex deleted file mode 100644 index b5409845..00000000 --- a/cheri/sail_latexcc/sailcccapStructToCapReg.tex +++ /dev/null @@ -1 +0,0 @@ -val capStructToCapReg : CapStruct -> CapReg diff --git a/cheri/sail_latexcc/sailcccapStructToMemBits.tex b/cheri/sail_latexcc/sailcccapStructToMemBits.tex deleted file mode 100644 index 4a49e9c0..00000000 --- a/cheri/sail_latexcc/sailcccapStructToMemBits.tex +++ /dev/null @@ -1 +0,0 @@ -val capStructToMemBits : CapStruct -> bits(128) diff --git a/cheri/sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex b/cheri/sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex deleted file mode 100644 index 8f3a8d0f..00000000 --- a/cheri/sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex +++ /dev/null @@ -1 +0,0 @@ -val capStructToMemBits128 : CapStruct -> bits(128) diff --git a/cheri/sail_latexcc/sailcccastunitvec.tex b/cheri/sail_latexcc/sailcccastunitvec.tex deleted file mode 100644 index e0391ded..00000000 --- a/cheri/sail_latexcc/sailcccastunitvec.tex +++ /dev/null @@ -1 +0,0 @@ -val cast cast_unit_vec : bit -> #\hyperref[zbits]{bits}#(1) diff --git a/cheri/sail_latexcc/sailcccomputeE.tex b/cheri/sail_latexcc/sailcccomputeE.tex deleted file mode 100644 index 893cea49..00000000 --- a/cheri/sail_latexcc/sailcccomputeE.tex +++ /dev/null @@ -1 +0,0 @@ -val computeE : bits(65) -> range(0, 48) effect {escape} diff --git a/cheri/sail_latexcc/sailccconcatstr.tex b/cheri/sail_latexcc/sailccconcatstr.tex deleted file mode 100644 index 07556728..00000000 --- a/cheri/sail_latexcc/sailccconcatstr.tex +++ /dev/null @@ -1 +0,0 @@ -val concat_str = {lem: "stringAppend", coq: "String.append", _: "concat_str"} : (string, string) -> string diff --git a/cheri/sail_latexcc/sailccdiv.tex b/cheri/sail_latexcc/sailccdiv.tex deleted file mode 100644 index 58318fe9..00000000 --- a/cheri/sail_latexcc/sailccdiv.tex +++ /dev/null @@ -1,7 +0,0 @@ -val div = { - smt: "div", - ocaml: "quotient", - lem: "integerDiv", - c: "tdiv_int", - coq: "div_with_eq" -} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = #\hyperref[zdiv]{div}#('n, 'm). atom('o)} diff --git a/cheri/sail_latexcc/sailccdivint.tex b/cheri/sail_latexcc/sailccdivint.tex deleted file mode 100644 index 34ae6121..00000000 --- a/cheri/sail_latexcc/sailccdivint.tex +++ /dev/null @@ -1,7 +0,0 @@ -val div_int = { - smt: "div", - ocaml: "quotient", - lem: "integerDiv", - c: "tdiv_int", - coq: "Z.quot" -} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailcceqanything.tex b/cheri/sail_latexcc/sailcceqanything.tex deleted file mode 100644 index 9b5d3c92..00000000 --- a/cheri/sail_latexcc/sailcceqanything.tex +++ /dev/null @@ -1 +0,0 @@ -val eq_anything = {ocaml: "(#\hyperref[zfun]{fun}# (x, y) -> x = y)", lem: "eq", coq: "generic_eq", _:"eq_anything"} : forall ('a : Type). ('a, 'a) -> bool diff --git a/cheri/sail_latexcc/sailcceqatom.tex b/cheri/sail_latexcc/sailcceqatom.tex deleted file mode 100644 index 0325ab15..00000000 --- a/cheri/sail_latexcc/sailcceqatom.tex +++ /dev/null @@ -1 +0,0 @@ -val eq_atom = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : forall 'n 'm. (atom('n), atom('m)) -> bool diff --git a/cheri/sail_latexcc/sailcceqbit.tex b/cheri/sail_latexcc/sailcceqbit.tex deleted file mode 100644 index 205d3436..00000000 --- a/cheri/sail_latexcc/sailcceqbit.tex +++ /dev/null @@ -1 +0,0 @@ -val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool diff --git a/cheri/sail_latexcc/sailcceqbits.tex b/cheri/sail_latexcc/sailcceqbits.tex deleted file mode 100644 index e78ed19a..00000000 --- a/cheri/sail_latexcc/sailcceqbits.tex +++ /dev/null @@ -1,6 +0,0 @@ -val eq_bits = { - ocaml: "eq_list", - lem: "eq_vec", - c: "eq_bits", - coq: "eq_vec" -} : forall 'n. (vector('n, dec, bit), vector('n, dec, bit)) -> bool diff --git a/cheri/sail_latexcc/sailcceqbittwo.tex b/cheri/sail_latexcc/sailcceqbittwo.tex deleted file mode 100644 index 59353940..00000000 --- a/cheri/sail_latexcc/sailcceqbittwo.tex +++ /dev/null @@ -1 +0,0 @@ -val eq_bit2 = "eq_bit" : (bit, bit) -> bool diff --git a/cheri/sail_latexcc/sailcceqbool.tex b/cheri/sail_latexcc/sailcceqbool.tex deleted file mode 100644 index 4d2c346b..00000000 --- a/cheri/sail_latexcc/sailcceqbool.tex +++ /dev/null @@ -1 +0,0 @@ -val eq_bool = {ocaml: "eq_bool", lem: "eq", c: "eq_bool", coq: "Bool.eqb"} : (bool, bool) -> bool diff --git a/cheri/sail_latexcc/sailcceqint.tex b/cheri/sail_latexcc/sailcceqint.tex deleted file mode 100644 index 4c0462c1..00000000 --- a/cheri/sail_latexcc/sailcceqint.tex +++ /dev/null @@ -1 +0,0 @@ -val eq_int = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "Z.eqb"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailcceqrange.tex b/cheri/sail_latexcc/sailcceqrange.tex deleted file mode 100644 index 7f1cd5f2..00000000 --- a/cheri/sail_latexcc/sailcceqrange.tex +++ /dev/null @@ -1 +0,0 @@ -val eq_range = {ocaml: "eq_int", lem: "eq", c: "eq_int", coq: "eq_range"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool diff --git a/cheri/sail_latexcc/sailccfastRepCheck.tex b/cheri/sail_latexcc/sailccfastRepCheck.tex deleted file mode 100644 index 2dd665fb..00000000 --- a/cheri/sail_latexcc/sailccfastRepCheck.tex +++ /dev/null @@ -1 +0,0 @@ -val fastRepCheck : (CapStruct, bits(64)) -> bool diff --git a/cheri/sail_latexcc/sailccfnCPtrCmpOpofnum.tex b/cheri/sail_latexcc/sailccfnCPtrCmpOpofnum.tex deleted file mode 100644 index 6ab563f3..00000000 --- a/cheri/sail_latexcc/sailccfnCPtrCmpOpofnum.tex +++ /dev/null @@ -1,10 +0,0 @@ -function CPtrCmpOp_of_num arg# = match arg# { - 0 => CEQ, - 1 => CNE, - 2 => CLT, - 3 => CLE, - 4 => CLTU, - 5 => CLEU, - 6 => CEXEQ, - _ => CNEXEQ -} diff --git a/cheri/sail_latexcc/sailccfnClearRegSetofnum.tex b/cheri/sail_latexcc/sailccfnClearRegSetofnum.tex deleted file mode 100644 index edfe64e3..00000000 --- a/cheri/sail_latexcc/sailccfnClearRegSetofnum.tex +++ /dev/null @@ -1,6 +0,0 @@ -function ClearRegSet_of_num arg# = match arg# { - 0 => GPLo, - 1 => GPHi, - 2 => CLo, - _ => CHi -} diff --git a/cheri/sail_latexcc/sailccfnHighestSetBit.tex b/cheri/sail_latexcc/sailccfnHighestSetBit.tex deleted file mode 100644 index dbbc5b49..00000000 --- a/cheri/sail_latexcc/sailccfnHighestSetBit.tex +++ /dev/null @@ -1,5 +0,0 @@ -function HighestSetBit x = { - foreach (i #\hyperref[zfrom]{from}# ('N - 1) to 0 by 1 in dec) - if [x[i]] == 0b1 then return (true, i); - return (false, 0) -} diff --git a/cheri/sail_latexcc/sailccfnMIPSread.tex b/cheri/sail_latexcc/sailccfnMIPSread.tex deleted file mode 100644 index ee937856..00000000 --- a/cheri/sail_latexcc/sailccfnMIPSread.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zzyzyMIPSzyread]{\_\_MIPS\_read}# (addr, width) = #\hyperref[zzyzyReadRAM]{\_\_ReadRAM}#(64, width, 0x0000_0000_0000_0000, addr) diff --git a/cheri/sail_latexcc/sailccfnMIPSwrite.tex b/cheri/sail_latexcc/sailccfnMIPSwrite.tex deleted file mode 100644 index 5e81f335..00000000 --- a/cheri/sail_latexcc/sailccfnMIPSwrite.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zzyzyMIPSzywrite]{\_\_MIPS\_write}# (addr, width, data) = let _ = #\hyperref[zzyzyWriteRAM]{\_\_WriteRAM}#(64, width, 0x0000_0000_0000_0000, addr, data) in () diff --git a/cheri/sail_latexcc/sailccfnatopcorrection.tex b/cheri/sail_latexcc/sailccfnatopcorrection.tex deleted file mode 100644 index 3a6be173..00000000 --- a/cheri/sail_latexcc/sailccfnatopcorrection.tex +++ /dev/null @@ -1,7 +0,0 @@ -function #\hyperref[zazytopzycorrection]{a\_top\_correction}#(a_mid, R, bound) : (#\hyperref[zbits]{bits}#(20), #\hyperref[zbits]{bits}#(20), #\hyperref[zbits]{bits}#(20)) -> #\hyperref[zbits]{bits}#(65) = - match (a_mid <_u R, bound <_u R) { - (false, false) => #\hyperref[zzzeros]{zeros}#(), - (false, true) => #\hyperref[zzzerozyextend]{zero\_extend}#(0b1), - (true, false) => #\hyperref[zones]{ones}#(), - (true, true) => #\hyperref[zzzeros]{zeros}#() - } diff --git a/cheri/sail_latexcc/sailccfnbitstobool.tex b/cheri/sail_latexcc/sailccfnbitstobool.tex deleted file mode 100644 index 1cb33076..00000000 --- a/cheri/sail_latexcc/sailccfnbitstobool.tex +++ /dev/null @@ -1 +0,0 @@ -function bits_to_bool x = #\hyperref[zbitzytozybool]{bit\_to\_bool}#(x[0]) diff --git a/cheri/sail_latexcc/sailccfnbittobool.tex b/cheri/sail_latexcc/sailccfnbittobool.tex deleted file mode 100644 index a5eea578..00000000 --- a/cheri/sail_latexcc/sailccfnbittobool.tex +++ /dev/null @@ -1,4 +0,0 @@ -function bit_to_bool b = match b { - bitone => true, - _ => false -} diff --git a/cheri/sail_latexcc/sailccfnbooltobits.tex b/cheri/sail_latexcc/sailccfnbooltobits.tex deleted file mode 100644 index 99075369..00000000 --- a/cheri/sail_latexcc/sailccfnbooltobits.tex +++ /dev/null @@ -1 +0,0 @@ -function bool_to_bits x = if x then 0b1 else 0b0 diff --git a/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex b/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex deleted file mode 100644 index 4af338b9..00000000 --- a/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex +++ /dev/null @@ -1,27 +0,0 @@ -function #\hyperref[zcapRegToCapStruct]{capRegToCapStruct}#(c) : CapReg -> CapStruct = - let s : bool = c[104] in - let Bc : #\hyperref[zbits]{bits}#(20) = if s then c[103..96] @ 0x000 else c[103..84] in - let Tc : #\hyperref[zbits]{bits}#(20) = if s then c[83..76] @ 0x000 else c[83..64] in - let otype : #\hyperref[zbits]{bits}#(24) = if s then c[95..84] @ c[75..64] else #\hyperref[zzzeros]{zeros}#() in - struct { - tag = c[128], - uperms = c[127..124], - access_system_regs = c[123], - permit_unseal = c[122], - permit_ccall = c[121], - permit_seal = c[120], - permit_store_local_cap = c[119], - permit_store_cap = c[118], - permit_load_cap = c[117], - permit_store = c[116], - permit_load = c[115], - permit_execute = c[114], - global = c[113], - reserved = c[112..111], - E = c[110..105], - sealed = s, - B = Bc, - T = Tc, - otype = otype, - address = c[63..0] - } diff --git a/cheri/sail_latexcc/sailccfncapStructToCapReg.tex b/cheri/sail_latexcc/sailccfncapStructToCapReg.tex deleted file mode 100644 index f6b02365..00000000 --- a/cheri/sail_latexcc/sailccfncapStructToCapReg.tex +++ /dev/null @@ -1,2 +0,0 @@ -function #\hyperref[zcapStructToCapReg]{capStructToCapReg}#(cap) : CapStruct -> CapReg = - (cap.tag @ #\hyperref[zcapStructToMemBitsonetwoeight]{capStructToMemBits128}#(cap)) diff --git a/cheri/sail_latexcc/sailccfncapStructToMemBits.tex b/cheri/sail_latexcc/sailccfncapStructToMemBits.tex deleted file mode 100644 index ea19467f..00000000 --- a/cheri/sail_latexcc/sailccfncapStructToMemBits.tex +++ /dev/null @@ -1,2 +0,0 @@ -function #\hyperref[zcapStructToMemBits]{capStructToMemBits}#(cap) : CapStruct -> #\hyperref[zbits]{bits}#(128) = - #\hyperref[zcapStructToMemBitsonetwoeight]{capStructToMemBits128}#(cap) ^ null_cap_bits diff --git a/cheri/sail_latexcc/sailccfncapStructToMemBitsonetwoeight.tex b/cheri/sail_latexcc/sailccfncapStructToMemBitsonetwoeight.tex deleted file mode 100644 index 08da637f..00000000 --- a/cheri/sail_latexcc/sailccfncapStructToMemBitsonetwoeight.tex +++ /dev/null @@ -1,12 +0,0 @@ -function #\hyperref[zcapStructToMemBitsonetwoeight]{capStructToMemBits128}#(cap) : CapStruct -> #\hyperref[zbits]{bits}#(128) = - let b : #\hyperref[zbits]{bits}#(20) = if cap.sealed then (cap.B)[19..12] @ (cap.otype)[23..12] else cap.B in - let t : #\hyperref[zbits]{bits}#(20) = if cap.sealed then (cap.T)[19..12] @ (cap.otype)[11..0] else cap.T in - ( cap.uperms - @ #\hyperref[zgetCapHardPerms]{getCapHardPerms}#(cap) - @ cap.reserved - @ cap.E - @ cap.sealed - @ b - @ t - @ cap.address - ) diff --git a/cheri/sail_latexcc/sailccfncastunitvec.tex b/cheri/sail_latexcc/sailccfncastunitvec.tex deleted file mode 100644 index 1bb7a9e0..00000000 --- a/cheri/sail_latexcc/sailccfncastunitvec.tex +++ /dev/null @@ -1,4 +0,0 @@ -function cast_unit_vec b = match b { - bitzero => 0b0, - _ => 0b1 -} diff --git a/cheri/sail_latexcc/sailccfncomputeE.tex b/cheri/sail_latexcc/sailccfncomputeE.tex deleted file mode 100644 index ef4cb71b..00000000 --- a/cheri/sail_latexcc/sailccfncomputeE.tex +++ /dev/null @@ -1,7 +0,0 @@ -function #\hyperref[zcomputeE]{computeE}# (rlength) : #\hyperref[zbits]{bits}#(65) -> range(0, 48) = - let (nonzero, 'msb) = #\hyperref[zHighestSetBit]{HighestSetBit}#((rlength + (rlength >> 6)) >> 19) in - if nonzero then - /* above will always return <= 45 because 19 bits of zero are shifted in from right */ - {assert(0 <= msb & msb <= 45); #\hyperref[zroundUp]{roundUp}# (#\hyperref[zmin]{min}#(msb,45)) } - else - 0 diff --git a/cheri/sail_latexcc/sailccfnfastRepCheck.tex b/cheri/sail_latexcc/sailccfnfastRepCheck.tex deleted file mode 100644 index 3e4d2111..00000000 --- a/cheri/sail_latexcc/sailccfnfastRepCheck.tex +++ /dev/null @@ -1,23 +0,0 @@ -function #\hyperref[zfastRepCheck]{fastRepCheck}#(c, i) : (CapStruct, #\hyperref[zbits]{bits}#(64)) -> bool= - let 'E = #\hyperref[zunsigned]{unsigned}#(c.E) in - if (E >= 44) then - true /* in this case representable region is whole address space */ - else - let E' = #\hyperref[zmin]{min}#(E, 43) in - let i_top = #\hyperref[zsigned]{signed}#(i[63..E+20]) in - let i_mid : #\hyperref[zbits]{bits}#(20) = i[E+19..E] in - let a_mid : #\hyperref[zbits]{bits}#(20) = (c.address)[E+19..E] in - let R : #\hyperref[zbits]{bits}#(20) = (c.B) - 0x01000 in - let diff : #\hyperref[zbits]{bits}#(20) = R - a_mid in - let diff1 : #\hyperref[zbits]{bits}#(20) = diff - 1 in - /* i_top determines 1. whether the increment is inRange - i.e. less than the size of the representable region - (2**(E+20)) and 2. whether it is positive or negative. To - satisfy 1. all top bits must be the same so we are - interested in the cases i_top is 0 or -1 */ - if (i_top == 0) then - i_mid <_u diff1 - else if (i_top == -1) then - (i_mid >=_u diff) & (R != a_mid) - else - false diff --git a/cheri/sail_latexcc/sailccfngetCapBase.tex b/cheri/sail_latexcc/sailccfngetCapBase.tex deleted file mode 100644 index 51677965..00000000 --- a/cheri/sail_latexcc/sailccfngetCapBase.tex +++ /dev/null @@ -1,10 +0,0 @@ -function #\hyperref[zgetCapBase]{getCapBase}#(c) : CapStruct -> uint64 = - let E = #\hyperref[zmin]{min}#(#\hyperref[zunsigned]{unsigned}#(c.E), 48) in - let Bc : #\hyperref[zbits]{bits}#(20) = c.B in - let a : #\hyperref[zbits]{bits}#(65) = #\hyperref[zzzerozyextend]{zero\_extend}#(c.address) in - let R : #\hyperref[zbits]{bits}#(20) = Bc - 0x01000 in /* wraps */ - let a_mid : #\hyperref[zbits]{bits}#(20) = #\hyperref[zmask]{mask}#(a >> E) in - let correction = #\hyperref[zazytopzycorrection]{a\_top\_correction}#(a_mid, R, Bc) in - let a_top = a >> E+20 in - let base : #\hyperref[zbits]{bits}#(64) = #\hyperref[zmask]{mask}#(((a_top + correction) @ Bc) << E) in - #\hyperref[zunsigned]{unsigned}#(base) diff --git a/cheri/sail_latexcc/sailccfngetCapCursor.tex b/cheri/sail_latexcc/sailccfngetCapCursor.tex deleted file mode 100644 index 9f5d5757..00000000 --- a/cheri/sail_latexcc/sailccfngetCapCursor.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zgetCapCursor]{getCapCursor}#(cap) : CapStruct -> uint64 = #\hyperref[zunsigned]{unsigned}#(cap.address) diff --git a/cheri/sail_latexcc/sailccfngetCapHardPerms.tex b/cheri/sail_latexcc/sailccfngetCapHardPerms.tex deleted file mode 100644 index 0b86b980..00000000 --- a/cheri/sail_latexcc/sailccfngetCapHardPerms.tex +++ /dev/null @@ -1,12 +0,0 @@ -function #\hyperref[zgetCapHardPerms]{getCapHardPerms}#(cap) : CapStruct -> #\hyperref[zbits]{bits}#(11) = - (cap.access_system_regs - @ cap.permit_unseal - @ cap.permit_ccall - @ cap.permit_seal - @ cap.permit_store_local_cap - @ cap.permit_store_cap - @ cap.permit_load_cap - @ cap.permit_store - @ cap.permit_load - @ cap.permit_execute - @ cap.global) diff --git a/cheri/sail_latexcc/sailccfngetCapLength.tex b/cheri/sail_latexcc/sailccfngetCapLength.tex deleted file mode 100644 index e9ce6566..00000000 --- a/cheri/sail_latexcc/sailccfngetCapLength.tex +++ /dev/null @@ -1,6 +0,0 @@ -function #\hyperref[zgetCapLength]{getCapLength}#(c) : CapStruct -> CapLen = - let 'top = #\hyperref[zgetCapTop]{getCapTop}#(c) in - let 'base = #\hyperref[zgetCapBase]{getCapBase}#(c) in { - assert (top >= base); - top - base - } diff --git a/cheri/sail_latexcc/sailccfngetCapOffset.tex b/cheri/sail_latexcc/sailccfngetCapOffset.tex deleted file mode 100644 index 8bf83916..00000000 --- a/cheri/sail_latexcc/sailccfngetCapOffset.tex +++ /dev/null @@ -1,3 +0,0 @@ -function #\hyperref[zgetCapOffset]{getCapOffset}#(c) : CapStruct -> uint64 = - let base = #\hyperref[zgetCapBase]{getCapBase}#(c) in - (#\hyperref[zunsigned]{unsigned}#(c.address) - base) % #\hyperref[zpowtwo]{pow2}#(64) diff --git a/cheri/sail_latexcc/sailccfngetCapPerms.tex b/cheri/sail_latexcc/sailccfngetCapPerms.tex deleted file mode 100644 index 9701e163..00000000 --- a/cheri/sail_latexcc/sailccfngetCapPerms.tex +++ /dev/null @@ -1,5 +0,0 @@ -function #\hyperref[zgetCapPerms]{getCapPerms}#(cap) : CapStruct -> #\hyperref[zbits]{bits}#(31) = - let perms : #\hyperref[zbits]{bits}#(15) = #\hyperref[zzzerozyextend]{zero\_extend}#(#\hyperref[zgetCapHardPerms]{getCapHardPerms}#(cap)) in - (0x000 /* uperms 30-19 */ - @ cap.uperms - @ perms) diff --git a/cheri/sail_latexcc/sailccfngetCapTop.tex b/cheri/sail_latexcc/sailccfngetCapTop.tex deleted file mode 100644 index 1be5af24..00000000 --- a/cheri/sail_latexcc/sailccfngetCapTop.tex +++ /dev/null @@ -1,11 +0,0 @@ -function #\hyperref[zgetCapTop]{getCapTop}# (c) : CapStruct -> CapLen = - let E = #\hyperref[zmin]{min}#(#\hyperref[zunsigned]{unsigned}#(c.E), 48) in - let Bc : #\hyperref[zbits]{bits}#(20) = c.B in - let T : #\hyperref[zbits]{bits}#(20) = c.T in - let a : #\hyperref[zbits]{bits}#(65) = #\hyperref[zzzerozyextend]{zero\_extend}#(c.address) in - let R : #\hyperref[zbits]{bits}#(20) = Bc - 0x01000 in /* wraps */ - let a_mid : #\hyperref[zbits]{bits}#(20) = #\hyperref[zmask]{mask}#(a >> E) in - let correction = #\hyperref[zazytopzycorrection]{a\_top\_correction}#(a_mid, R, T) in - let a_top = a >> E+20 in - let top1 : #\hyperref[zbits]{bits}#(65) = #\hyperref[zmask]{mask}#((a_top + correction) @ T) in - #\hyperref[zunsigned]{unsigned}#(top1 << E) diff --git a/cheri/sail_latexcc/sailccfnincCapOffset.tex b/cheri/sail_latexcc/sailccfnincCapOffset.tex deleted file mode 100644 index 59d3237e..00000000 --- a/cheri/sail_latexcc/sailccfnincCapOffset.tex +++ /dev/null @@ -1,5 +0,0 @@ -function #\hyperref[zincCapOffset]{incCapOffset}#(c, delta) : (CapStruct, #\hyperref[zbits]{bits}#(64)) -> (bool, CapStruct) = - let newAddress : #\hyperref[zbits]{bits}#(64) = c.address + delta in - let newCap = { c with address = newAddress } in - let representable = #\hyperref[zfastRepCheck]{fastRepCheck}#(c, delta) in - (representable, newCap) diff --git a/cheri/sail_latexcc/sailccfninttocap.tex b/cheri/sail_latexcc/sailccfninttocap.tex deleted file mode 100644 index 31bb2bec..00000000 --- a/cheri/sail_latexcc/sailccfninttocap.tex +++ /dev/null @@ -1,2 +0,0 @@ -function #\hyperref[zintzytozycap]{int\_to\_cap}# (offset) : #\hyperref[zbits]{bits}#(64) -> CapStruct = - {null_cap with address = offset} diff --git a/cheri/sail_latexcc/sailccfnisnone.tex b/cheri/sail_latexcc/sailccfnisnone.tex deleted file mode 100644 index 877cc2a0..00000000 --- a/cheri/sail_latexcc/sailccfnisnone.tex +++ /dev/null @@ -1,4 +0,0 @@ -function is_none opt = match opt { - #\hyperref[zSome]{Some}#(_) => false, - #\hyperref[zNone]{None}#() => true -} diff --git a/cheri/sail_latexcc/sailccfnissome.tex b/cheri/sail_latexcc/sailccfnissome.tex deleted file mode 100644 index f1f5f655..00000000 --- a/cheri/sail_latexcc/sailccfnissome.tex +++ /dev/null @@ -1,4 +0,0 @@ -function is_some opt = match opt { - #\hyperref[zSome]{Some}#(_) => true, - #\hyperref[zNone]{None}#() => false -} diff --git a/cheri/sail_latexcc/sailccfnmask.tex b/cheri/sail_latexcc/sailccfnmask.tex deleted file mode 100644 index e62ea529..00000000 --- a/cheri/sail_latexcc/sailccfnmask.tex +++ /dev/null @@ -1 +0,0 @@ -function mask bs = bs['n - 1 .. 0] diff --git a/cheri/sail_latexcc/sailccfnmemBitsToCapBits.tex b/cheri/sail_latexcc/sailccfnmemBitsToCapBits.tex deleted file mode 100644 index 198cf984..00000000 --- a/cheri/sail_latexcc/sailccfnmemBitsToCapBits.tex +++ /dev/null @@ -1,2 +0,0 @@ -function #\hyperref[zmemBitsToCapBits]{memBitsToCapBits}#(tag, b) : (bool, #\hyperref[zbits]{bits}#(128)) -> #\hyperref[zbits]{bits}#(129) = - #\hyperref[zmemBitsToCapBitsonetwoeight]{memBitsToCapBits128}#(tag, b ^ null_cap_bits) diff --git a/cheri/sail_latexcc/sailccfnmemBitsToCapBitsonetwoeight.tex b/cheri/sail_latexcc/sailccfnmemBitsToCapBitsonetwoeight.tex deleted file mode 100644 index 723571e9..00000000 --- a/cheri/sail_latexcc/sailccfnmemBitsToCapBitsonetwoeight.tex +++ /dev/null @@ -1,2 +0,0 @@ -function #\hyperref[zmemBitsToCapBitsonetwoeight]{memBitsToCapBits128}#(tag, b) : (bool, #\hyperref[zbits]{bits}#(128)) -> CapReg= - (tag @ b) diff --git a/cheri/sail_latexcc/sailccfnmipssignextend.tex b/cheri/sail_latexcc/sailccfnmipssignextend.tex deleted file mode 100644 index 80945b61..00000000 --- a/cheri/sail_latexcc/sailccfnmipssignextend.tex +++ /dev/null @@ -1 +0,0 @@ -function mips_sign_extend v = #\hyperref[zsailzysignzyextend]{sail\_sign\_extend}#(v, sizeof('m)) diff --git a/cheri/sail_latexcc/sailccfnmipszzeroextend.tex b/cheri/sail_latexcc/sailccfnmipszzeroextend.tex deleted file mode 100644 index 6c9914d9..00000000 --- a/cheri/sail_latexcc/sailccfnmipszzeroextend.tex +++ /dev/null @@ -1 +0,0 @@ -function mips_zero_extend v = #\hyperref[zsailzyzzerozyextend]{sail\_zero\_extend}#(v, sizeof('m)) diff --git a/cheri/sail_latexcc/sailccfnneqanything.tex b/cheri/sail_latexcc/sailccfnneqanything.tex deleted file mode 100644 index 1605ed05..00000000 --- a/cheri/sail_latexcc/sailccfnneqanything.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zneqzyanything]{neq\_anything}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(x == y) diff --git a/cheri/sail_latexcc/sailccfnneqatom.tex b/cheri/sail_latexcc/sailccfnneqatom.tex deleted file mode 100644 index e9a9f93f..00000000 --- a/cheri/sail_latexcc/sailccfnneqatom.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zneqzyatom]{neq\_atom}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzyatom]{eq\_atom}#(x, y)) diff --git a/cheri/sail_latexcc/sailccfnneqbool.tex b/cheri/sail_latexcc/sailccfnneqbool.tex deleted file mode 100644 index 65007b8e..00000000 --- a/cheri/sail_latexcc/sailccfnneqbool.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zneqzybool]{neq\_bool}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzybool]{eq\_bool}#(x, y)) diff --git a/cheri/sail_latexcc/sailccfnneqint.tex b/cheri/sail_latexcc/sailccfnneqint.tex deleted file mode 100644 index 952a7735..00000000 --- a/cheri/sail_latexcc/sailccfnneqint.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zneqzyint]{neq\_int}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzyint]{eq\_int}#(x, y)) diff --git a/cheri/sail_latexcc/sailccfnneqrange.tex b/cheri/sail_latexcc/sailccfnneqrange.tex deleted file mode 100644 index 43f49e9e..00000000 --- a/cheri/sail_latexcc/sailccfnneqrange.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zneqzyrange]{neq\_range}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzyrange]{eq\_range}#(x, y)) diff --git a/cheri/sail_latexcc/sailccfnneqvec.tex b/cheri/sail_latexcc/sailccfnneqvec.tex deleted file mode 100644 index c446df08..00000000 --- a/cheri/sail_latexcc/sailccfnneqvec.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zneqzyvec]{neq\_vec}# (x, y) = #\hyperref[znotzybool]{not\_bool}#(#\hyperref[zeqzybits]{eq\_bits}#(x, y)) diff --git a/cheri/sail_latexcc/sailccfnnumofCPtrCmpOp.tex b/cheri/sail_latexcc/sailccfnnumofCPtrCmpOp.tex deleted file mode 100644 index 4d20546b..00000000 --- a/cheri/sail_latexcc/sailccfnnumofCPtrCmpOp.tex +++ /dev/null @@ -1,10 +0,0 @@ -function num_of_CPtrCmpOp arg# = match arg# { - CEQ => 0, - CNE => 1, - CLT => 2, - CLE => 3, - CLTU => 4, - CLEU => 5, - CEXEQ => 6, - CNEXEQ => 7 -} diff --git a/cheri/sail_latexcc/sailccfnnumofClearRegSet.tex b/cheri/sail_latexcc/sailccfnnumofClearRegSet.tex deleted file mode 100644 index 3dd58b89..00000000 --- a/cheri/sail_latexcc/sailccfnnumofClearRegSet.tex +++ /dev/null @@ -1,6 +0,0 @@ -function num_of_ClearRegSet arg# = match arg# { - GPLo => 0, - GPHi => 1, - CLo => 2, - CHi => 3 -} diff --git a/cheri/sail_latexcc/sailccfnones.tex b/cheri/sail_latexcc/sailccfnones.tex deleted file mode 100644 index e58040d7..00000000 --- a/cheri/sail_latexcc/sailccfnones.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zones]{ones}#() = #\hyperref[zreplicatezybits]{replicate\_bits}# (0b1,'n) diff --git a/cheri/sail_latexcc/sailccfnroundUp.tex b/cheri/sail_latexcc/sailccfnroundUp.tex deleted file mode 100644 index 1ed68a59..00000000 --- a/cheri/sail_latexcc/sailccfnroundUp.tex +++ /dev/null @@ -1,5 +0,0 @@ -function #\hyperref[zroundUp]{roundUp}#(e) : range(0, 45) -> range(0, 48) = - let 'r = e % 4 in - if (r == 0) - then e - else (e - r + 4) diff --git a/cheri/sail_latexcc/sailccfnsailmask.tex b/cheri/sail_latexcc/sailccfnsailmask.tex deleted file mode 100644 index 37ede658..00000000 --- a/cheri/sail_latexcc/sailccfnsailmask.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zsailzymask]{sail\_mask}#(len, v) = if len <= #\hyperref[zlength]{length}#(v) then #\hyperref[ztruncate]{truncate}#(v, len) else #\hyperref[zsailzyzzerozyextend]{sail\_zero\_extend}#(v, len) diff --git a/cheri/sail_latexcc/sailccfnsealCap.tex b/cheri/sail_latexcc/sailccfnsealCap.tex deleted file mode 100644 index 55c55014..00000000 --- a/cheri/sail_latexcc/sailccfnsealCap.tex +++ /dev/null @@ -1,5 +0,0 @@ -function #\hyperref[zsealCap]{sealCap}#(cap, otype) : (CapStruct, #\hyperref[zbits]{bits}#(24)) -> (bool, CapStruct) = - if (((cap.T)[11..0] == #\hyperref[zzzeros]{zeros}#()) & ((cap.B)[11..0] == #\hyperref[zzzeros]{zeros}#())) then - (true, {cap with sealed=true, otype=otype}) - else - (false, cap /* XXX should be undefined? */ ) diff --git a/cheri/sail_latexcc/sailccfnsetCapBounds.tex b/cheri/sail_latexcc/sailccfnsetCapBounds.tex deleted file mode 100644 index 44808068..00000000 --- a/cheri/sail_latexcc/sailccfnsetCapBounds.tex +++ /dev/null @@ -1,13 +0,0 @@ -function #\hyperref[zsetCapBounds]{setCapBounds}#(cap, base, top) : (CapStruct, #\hyperref[zbits]{bits}#(64), #\hyperref[zbits]{bits}#(65)) -> (bool, CapStruct) = - /* {cap with base=base; length=(#\hyperref[zbits]{bits}#(64)) length; offset=0} */ - let 'e = #\hyperref[zcomputeE]{computeE}#(top - (0b0 @ base)) in - let Bc : #\hyperref[zbits]{bits}#(20) = #\hyperref[zmask]{mask}#(base >> e) in - let T : #\hyperref[zbits]{bits}#(20) = #\hyperref[zmask]{mask}#(top >> e) in - let e_mask : #\hyperref[zbits]{bits}#(65) = #\hyperref[zzzerozyextend]{zero\_extend}#(#\hyperref[zreplicatezybits]{replicate\_bits}#(0b1, e)) in - let e_bits = top & e_mask in - let T2 : #\hyperref[zbits]{bits}#(20) = T + (if #\hyperref[zunsigned]{unsigned}#(e_bits) == 0 then 0x00000 else 0x00001) in - let newCap = {cap with address=base, E=#\hyperref[ztozybits]{to\_bits}#(6, e), B=Bc, T=T2} in - let newBase = #\hyperref[zgetCapBase]{getCapBase}#(newCap) in - let newTop = #\hyperref[zgetCapTop]{getCapTop}#(newCap) in - let exact = (#\hyperref[zunsigned]{unsigned}#(base) == newBase) & (#\hyperref[zunsigned]{unsigned}#(top) == newTop) in - (exact, newCap) diff --git a/cheri/sail_latexcc/sailccfnsetCapOffset.tex b/cheri/sail_latexcc/sailccfnsetCapOffset.tex deleted file mode 100644 index f272f7d3..00000000 --- a/cheri/sail_latexcc/sailccfnsetCapOffset.tex +++ /dev/null @@ -1,6 +0,0 @@ -function #\hyperref[zsetCapOffset]{setCapOffset}#(c, offset) : (CapStruct, #\hyperref[zbits]{bits}#(64)) -> (bool, CapStruct) = - let base : #\hyperref[zbits]{bits}#(64) = #\hyperref[ztozybits]{to\_bits}#(64, #\hyperref[zgetCapBase]{getCapBase}#(c)) in - let newAddress : #\hyperref[zbits]{bits}#(64) = base + offset in - let newCap = { c with address = newAddress } in - let representable = #\hyperref[zfastRepCheck]{fastRepCheck}#(c, (newAddress - c.address)) in - (representable, newCap) diff --git a/cheri/sail_latexcc/sailccfnsetCapPerms.tex b/cheri/sail_latexcc/sailccfnsetCapPerms.tex deleted file mode 100644 index 5af9e7f6..00000000 --- a/cheri/sail_latexcc/sailccfnsetCapPerms.tex +++ /dev/null @@ -1,16 +0,0 @@ -function #\hyperref[zsetCapPerms]{setCapPerms}#(cap, perms) : (CapStruct, #\hyperref[zbits]{bits}#(31)) -> CapStruct = - { cap with - uperms = perms[18..15], - /* 14..11 reserved -- ignore */ - access_system_regs = perms[10], - permit_unseal = perms[9], - permit_ccall = perms[8], - permit_seal = perms[7], - permit_store_local_cap = perms[6], - permit_store_cap = perms[5], - permit_load_cap = perms[4], - permit_store = perms[3], - permit_load = perms[2], - permit_execute = perms[1], - global = perms[0] - } diff --git a/cheri/sail_latexcc/sailccfntobits.tex b/cheri/sail_latexcc/sailccfntobits.tex deleted file mode 100644 index d1df5e83..00000000 --- a/cheri/sail_latexcc/sailccfntobits.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[ztozybits]{to\_bits}# (l, n) = #\hyperref[zgetzyslicezyint]{get\_slice\_int}#(l, n, 0) diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIsznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIsznine.tex deleted file mode 100644 index 62e5a2e4..00000000 --- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIsznine.tex +++ /dev/null @@ -1 +0,0 @@ -function operator <#\hyperref[zzys]{\_s}# (x, y) = #\hyperref[zsigned]{signed}#(x) < #\hyperref[zsigned]{signed}#(y) diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIuznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIuznine.tex deleted file mode 100644 index 3f946820..00000000 --- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIuznine.tex +++ /dev/null @@ -1 +0,0 @@ -function operator <#\hyperref[zzyu]{\_u}# (x, y) = #\hyperref[zunsigned]{unsigned}#(x) < #\hyperref[zunsigned]{unsigned}#(y) diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJsznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJsznine.tex deleted file mode 100644 index 57ecf181..00000000 --- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJsznine.tex +++ /dev/null @@ -1 +0,0 @@ -function operator >=#\hyperref[zzys]{\_s}# (x, y) = #\hyperref[zsigned]{signed}#(x) >= #\hyperref[zsigned]{signed}#(y) diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJuznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJuznine.tex deleted file mode 100644 index 6df36c6f..00000000 --- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJuznine.tex +++ /dev/null @@ -1 +0,0 @@ -function operator >=#\hyperref[zzyu]{\_u}# (x, y) = #\hyperref[zunsigned]{unsigned}#(x) >= #\hyperref[zunsigned]{unsigned}#(y) diff --git a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozQzQznine.tex b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozQzQznine.tex deleted file mode 100644 index 2c372e1b..00000000 --- a/cheri/sail_latexcc/sailccfnzeightoperatorzzerozQzQznine.tex +++ /dev/null @@ -1 +0,0 @@ -function operator ^^ (bs, n) = #\hyperref[zreplicatezybits]{replicate\_bits}# (bs, n) diff --git a/cheri/sail_latexcc/sailccfnzzeros.tex b/cheri/sail_latexcc/sailccfnzzeros.tex deleted file mode 100644 index 38d463fb..00000000 --- a/cheri/sail_latexcc/sailccfnzzeros.tex +++ /dev/null @@ -1 +0,0 @@ -function #\hyperref[zzzeros]{zeros}#() = #\hyperref[zreplicatezybits]{replicate\_bits}# (0b0,'n) diff --git a/cheri/sail_latexcc/sailccgetCapBase.tex b/cheri/sail_latexcc/sailccgetCapBase.tex deleted file mode 100644 index c7044d1d..00000000 --- a/cheri/sail_latexcc/sailccgetCapBase.tex +++ /dev/null @@ -1 +0,0 @@ -val getCapBase : CapStruct -> uint64 diff --git a/cheri/sail_latexcc/sailccgetCapCursor.tex b/cheri/sail_latexcc/sailccgetCapCursor.tex deleted file mode 100644 index fd5d72d8..00000000 --- a/cheri/sail_latexcc/sailccgetCapCursor.tex +++ /dev/null @@ -1 +0,0 @@ -val getCapCursor : CapStruct -> uint64 diff --git a/cheri/sail_latexcc/sailccgetCapHardPerms.tex b/cheri/sail_latexcc/sailccgetCapHardPerms.tex deleted file mode 100644 index 3b65a7c0..00000000 --- a/cheri/sail_latexcc/sailccgetCapHardPerms.tex +++ /dev/null @@ -1 +0,0 @@ -val getCapHardPerms : CapStruct -> bits(11) diff --git a/cheri/sail_latexcc/sailccgetCapLength.tex b/cheri/sail_latexcc/sailccgetCapLength.tex deleted file mode 100644 index be84bfb5..00000000 --- a/cheri/sail_latexcc/sailccgetCapLength.tex +++ /dev/null @@ -1 +0,0 @@ -val getCapLength : CapStruct -> CapLen effect {escape} diff --git a/cheri/sail_latexcc/sailccgetCapOffset.tex b/cheri/sail_latexcc/sailccgetCapOffset.tex deleted file mode 100644 index 668c3df1..00000000 --- a/cheri/sail_latexcc/sailccgetCapOffset.tex +++ /dev/null @@ -1 +0,0 @@ -val getCapOffset : CapStruct -> uint64 diff --git a/cheri/sail_latexcc/sailccgetCapPerms.tex b/cheri/sail_latexcc/sailccgetCapPerms.tex deleted file mode 100644 index b2dabf89..00000000 --- a/cheri/sail_latexcc/sailccgetCapPerms.tex +++ /dev/null @@ -1 +0,0 @@ -val getCapPerms : CapStruct -> bits(31) diff --git a/cheri/sail_latexcc/sailccgetCapTop.tex b/cheri/sail_latexcc/sailccgetCapTop.tex deleted file mode 100644 index ff0e5f95..00000000 --- a/cheri/sail_latexcc/sailccgetCapTop.tex +++ /dev/null @@ -1 +0,0 @@ -val getCapTop : CapStruct -> CapLen diff --git a/cheri/sail_latexcc/sailccgetsliceint.tex b/cheri/sail_latexcc/sailccgetsliceint.tex deleted file mode 100644 index 2b30d096..00000000 --- a/cheri/sail_latexcc/sailccgetsliceint.tex +++ /dev/null @@ -1 +0,0 @@ -val get_slice_int = "get_slice_int" : forall 'w. (atom('w), int, int) -> #\hyperref[zbits]{bits}#('w) diff --git a/cheri/sail_latexcc/sailccgettimens.tex b/cheri/sail_latexcc/sailccgettimens.tex deleted file mode 100644 index 74cfd526..00000000 --- a/cheri/sail_latexcc/sailccgettimens.tex +++ /dev/null @@ -1 +0,0 @@ -val "get_time_ns" : unit -> int diff --git a/cheri/sail_latexcc/sailccgtatom.tex b/cheri/sail_latexcc/sailccgtatom.tex deleted file mode 100644 index b2147a8f..00000000 --- a/cheri/sail_latexcc/sailccgtatom.tex +++ /dev/null @@ -1 +0,0 @@ -val gt_atom = {coq: "Z.gtb", _: "gt"} : forall 'n 'm. (atom('n), atom('m)) -> bool diff --git a/cheri/sail_latexcc/sailccgtatomrange.tex b/cheri/sail_latexcc/sailccgtatomrange.tex deleted file mode 100644 index 3c520181..00000000 --- a/cheri/sail_latexcc/sailccgtatomrange.tex +++ /dev/null @@ -1 +0,0 @@ -val gt_atom_range = {coq: "gtb_range_r", _: "gt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool diff --git a/cheri/sail_latexcc/sailccgteqatom.tex b/cheri/sail_latexcc/sailccgteqatom.tex deleted file mode 100644 index fb3b66b2..00000000 --- a/cheri/sail_latexcc/sailccgteqatom.tex +++ /dev/null @@ -1 +0,0 @@ -val gteq_atom = {coq: "Z.geb", _: "gteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool diff --git a/cheri/sail_latexcc/sailccgteqatomrange.tex b/cheri/sail_latexcc/sailccgteqatomrange.tex deleted file mode 100644 index 7aaf633f..00000000 --- a/cheri/sail_latexcc/sailccgteqatomrange.tex +++ /dev/null @@ -1 +0,0 @@ -val gteq_atom_range = {coq: "geb_range_r", _: "gteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool diff --git a/cheri/sail_latexcc/sailccgteqint.tex b/cheri/sail_latexcc/sailccgteqint.tex deleted file mode 100644 index 77271d1f..00000000 --- a/cheri/sail_latexcc/sailccgteqint.tex +++ /dev/null @@ -1 +0,0 @@ -val gteq_int = {coq: "Z.geb", _:"gteq"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailccgteqrangeatom.tex b/cheri/sail_latexcc/sailccgteqrangeatom.tex deleted file mode 100644 index fda25265..00000000 --- a/cheri/sail_latexcc/sailccgteqrangeatom.tex +++ /dev/null @@ -1 +0,0 @@ -val gteq_range_atom = {coq: "geb_range_l", _: "gteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool diff --git a/cheri/sail_latexcc/sailccgtint.tex b/cheri/sail_latexcc/sailccgtint.tex deleted file mode 100644 index 2d953eec..00000000 --- a/cheri/sail_latexcc/sailccgtint.tex +++ /dev/null @@ -1 +0,0 @@ -val gt_int = {coq: "Z.gtb", _:"gt"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailccgtrangeatom.tex b/cheri/sail_latexcc/sailccgtrangeatom.tex deleted file mode 100644 index b8635909..00000000 --- a/cheri/sail_latexcc/sailccgtrangeatom.tex +++ /dev/null @@ -1 +0,0 @@ -val gt_range_atom = {coq: "gtb_range_l", _: "gt"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool diff --git a/cheri/sail_latexcc/sailccincCapOffset.tex b/cheri/sail_latexcc/sailccincCapOffset.tex deleted file mode 100644 index 21c08cb5..00000000 --- a/cheri/sail_latexcc/sailccincCapOffset.tex +++ /dev/null @@ -1 +0,0 @@ -val incCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct) diff --git a/cheri/sail_latexcc/sailccintpower.tex b/cheri/sail_latexcc/sailccintpower.tex deleted file mode 100644 index 0aa13188..00000000 --- a/cheri/sail_latexcc/sailccintpower.tex +++ /dev/null @@ -1 +0,0 @@ -val int_power = {ocaml: "int_power", lem: "pow", coq: "Z.pow"} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccinttocap.tex b/cheri/sail_latexcc/sailccinttocap.tex deleted file mode 100644 index 0f4cd328..00000000 --- a/cheri/sail_latexcc/sailccinttocap.tex +++ /dev/null @@ -1 +0,0 @@ -val int_to_cap : bits(64) -> CapStruct diff --git a/cheri/sail_latexcc/sailccisnone.tex b/cheri/sail_latexcc/sailccisnone.tex deleted file mode 100644 index 76688d37..00000000 --- a/cheri/sail_latexcc/sailccisnone.tex +++ /dev/null @@ -1 +0,0 @@ -val is_none : forall ('a : Type). #\hyperref[zoption]{option}#('a) -> bool diff --git a/cheri/sail_latexcc/sailccissome.tex b/cheri/sail_latexcc/sailccissome.tex deleted file mode 100644 index 071ac6b6..00000000 --- a/cheri/sail_latexcc/sailccissome.tex +++ /dev/null @@ -1 +0,0 @@ -val is_some : forall ('a : Type). #\hyperref[zoption]{option}#('a) -> bool diff --git a/cheri/sail_latexcc/sailcclength.tex b/cheri/sail_latexcc/sailcclength.tex deleted file mode 100644 index 248c8507..00000000 --- a/cheri/sail_latexcc/sailcclength.tex +++ /dev/null @@ -1 +0,0 @@ -overload length = {bitvector_length, vector_length}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccltatom.tex b/cheri/sail_latexcc/sailccltatom.tex deleted file mode 100644 index 5cca54df..00000000 --- a/cheri/sail_latexcc/sailccltatom.tex +++ /dev/null @@ -1 +0,0 @@ -val lt_atom = {coq: "Z.ltb", _: "lt"} : forall 'n 'm. (atom('n), atom('m)) -> bool diff --git a/cheri/sail_latexcc/sailccltatomrange.tex b/cheri/sail_latexcc/sailccltatomrange.tex deleted file mode 100644 index 19d3375d..00000000 --- a/cheri/sail_latexcc/sailccltatomrange.tex +++ /dev/null @@ -1 +0,0 @@ -val lt_atom_range = {coq: "ltb_range_r", _: "lt"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool diff --git a/cheri/sail_latexcc/sailcclteqatom.tex b/cheri/sail_latexcc/sailcclteqatom.tex deleted file mode 100644 index 26e27e2d..00000000 --- a/cheri/sail_latexcc/sailcclteqatom.tex +++ /dev/null @@ -1 +0,0 @@ -val lteq_atom = {coq: "Z.leb", _: "lteq"} : forall 'n 'm. (atom('n), atom('m)) -> bool diff --git a/cheri/sail_latexcc/sailcclteqatomrange.tex b/cheri/sail_latexcc/sailcclteqatomrange.tex deleted file mode 100644 index 6e951cf7..00000000 --- a/cheri/sail_latexcc/sailcclteqatomrange.tex +++ /dev/null @@ -1 +0,0 @@ -val lteq_atom_range = {coq: "leb_range_r", _: "lteq"} : forall 'n 'm 'o. (atom('n), range('m, 'o)) -> bool diff --git a/cheri/sail_latexcc/sailcclteqint.tex b/cheri/sail_latexcc/sailcclteqint.tex deleted file mode 100644 index 555176be..00000000 --- a/cheri/sail_latexcc/sailcclteqint.tex +++ /dev/null @@ -1 +0,0 @@ -val lteq_int = {coq: "Z.leb", _:"lteq"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailcclteqrangeatom.tex b/cheri/sail_latexcc/sailcclteqrangeatom.tex deleted file mode 100644 index f8fcd32d..00000000 --- a/cheri/sail_latexcc/sailcclteqrangeatom.tex +++ /dev/null @@ -1 +0,0 @@ -val lteq_range_atom = {coq: "leb_range_l", _: "lteq"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool diff --git a/cheri/sail_latexcc/sailccltint.tex b/cheri/sail_latexcc/sailccltint.tex deleted file mode 100644 index 40bd4e85..00000000 --- a/cheri/sail_latexcc/sailccltint.tex +++ /dev/null @@ -1 +0,0 @@ -val lt_int = {coq: "Z.ltb", _:"lt"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailccltrangeatom.tex b/cheri/sail_latexcc/sailccltrangeatom.tex deleted file mode 100644 index d8495496..00000000 --- a/cheri/sail_latexcc/sailccltrangeatom.tex +++ /dev/null @@ -1 +0,0 @@ -val lt_range_atom = {coq: "ltb_range_l", _: "lt"} : forall 'n 'm 'o. (range('n, 'm), atom('o)) -> bool diff --git a/cheri/sail_latexcc/sailccmask.tex b/cheri/sail_latexcc/sailccmask.tex deleted file mode 100644 index 35d052db..00000000 --- a/cheri/sail_latexcc/sailccmask.tex +++ /dev/null @@ -1 +0,0 @@ -val mask : forall 'm 'n , 'm >= 'n > 0 . #\hyperref[zbits]{bits}#('m) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccmax.tex b/cheri/sail_latexcc/sailccmax.tex deleted file mode 100644 index 1ceed42c..00000000 --- a/cheri/sail_latexcc/sailccmax.tex +++ /dev/null @@ -1 +0,0 @@ -overload max = {max_atom, max_nat, max_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccmaxatom.tex b/cheri/sail_latexcc/sailccmaxatom.tex deleted file mode 100644 index 6cbdfa7f..00000000 --- a/cheri/sail_latexcc/sailccmaxatom.tex +++ /dev/null @@ -1 +0,0 @@ -val max_atom = {ocaml: "max_int", lem: "max", coq: "max_atom", c:"max_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c >= 'a & 'c >= 'b . atom('c)} diff --git a/cheri/sail_latexcc/sailccmaxint.tex b/cheri/sail_latexcc/sailccmaxint.tex deleted file mode 100644 index c537babb..00000000 --- a/cheri/sail_latexcc/sailccmaxint.tex +++ /dev/null @@ -1 +0,0 @@ -val max_int = {lem: "max", coq: "Z.max", _: "max_int"} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccmaxnat.tex b/cheri/sail_latexcc/sailccmaxnat.tex deleted file mode 100644 index 1b62334a..00000000 --- a/cheri/sail_latexcc/sailccmaxnat.tex +++ /dev/null @@ -1 +0,0 @@ -val max_nat = {lem: "max", coq: "Z.max", _: "max_int"} : (nat, nat) -> nat diff --git a/cheri/sail_latexcc/sailccmemBitsToCapBits.tex b/cheri/sail_latexcc/sailccmemBitsToCapBits.tex deleted file mode 100644 index a5c86272..00000000 --- a/cheri/sail_latexcc/sailccmemBitsToCapBits.tex +++ /dev/null @@ -1 +0,0 @@ -val memBitsToCapBits : (bool, bits(128)) -> bits(129) diff --git a/cheri/sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex b/cheri/sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex deleted file mode 100644 index 4eb94a3d..00000000 --- a/cheri/sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex +++ /dev/null @@ -1 +0,0 @@ -val memBitsToCapBits128 : (bool, bits(128)) -> CapReg diff --git a/cheri/sail_latexcc/sailccmin.tex b/cheri/sail_latexcc/sailccmin.tex deleted file mode 100644 index 94097198..00000000 --- a/cheri/sail_latexcc/sailccmin.tex +++ /dev/null @@ -1 +0,0 @@ -overload min = {min_atom, min_nat, min_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccminatom.tex b/cheri/sail_latexcc/sailccminatom.tex deleted file mode 100644 index acfea384..00000000 --- a/cheri/sail_latexcc/sailccminatom.tex +++ /dev/null @@ -1 +0,0 @@ -val min_atom = {ocaml: "min_int", lem: "min", coq: "min_atom", c:"min_int"} : forall 'a 'b . (atom('a), atom('b)) -> {'c, ('c = 'a | 'c = 'b) & 'c <= 'a & 'c <= 'b . atom('c)} diff --git a/cheri/sail_latexcc/sailccminint.tex b/cheri/sail_latexcc/sailccminint.tex deleted file mode 100644 index 3d633d08..00000000 --- a/cheri/sail_latexcc/sailccminint.tex +++ /dev/null @@ -1 +0,0 @@ -val min_int = {lem: "min", coq: "Z.min", _: "min_int"} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccminnat.tex b/cheri/sail_latexcc/sailccminnat.tex deleted file mode 100644 index 85409bd8..00000000 --- a/cheri/sail_latexcc/sailccminnat.tex +++ /dev/null @@ -1 +0,0 @@ -val min_nat = {lem: "min", coq: "Z.min", _: "min_int"} : (nat, nat) -> nat diff --git a/cheri/sail_latexcc/sailccmipssignextend.tex b/cheri/sail_latexcc/sailccmipssignextend.tex deleted file mode 100644 index e613567d..00000000 --- a/cheri/sail_latexcc/sailccmipssignextend.tex +++ /dev/null @@ -1 +0,0 @@ -val mips_sign_extend : forall 'n 'm , 'm >= 'n . #\hyperref[zbits]{bits}#('n) -> #\hyperref[zbits]{bits}#('m) diff --git a/cheri/sail_latexcc/sailccmipszzeroextend.tex b/cheri/sail_latexcc/sailccmipszzeroextend.tex deleted file mode 100644 index adbb4188..00000000 --- a/cheri/sail_latexcc/sailccmipszzeroextend.tex +++ /dev/null @@ -1 +0,0 @@ -val mips_zero_extend : forall 'n 'm , 'm >= 'n . #\hyperref[zbits]{bits}#('n) -> #\hyperref[zbits]{bits}#('m) diff --git a/cheri/sail_latexcc/sailccmod.tex b/cheri/sail_latexcc/sailccmod.tex deleted file mode 100644 index ab70dd7a..00000000 --- a/cheri/sail_latexcc/sailccmod.tex +++ /dev/null @@ -1,7 +0,0 @@ -val mod = { - smt: "mod", - ocaml: "modulus", - lem: "integerMod", - c: "tmod_int", - coq: "mod_with_eq" -} : forall 'n 'm. (atom('n), atom('m)) -> {'o, 'o = #\hyperref[zmod]{mod}#('n, 'm). atom('o)} diff --git a/cheri/sail_latexcc/sailccmodint.tex b/cheri/sail_latexcc/sailccmodint.tex deleted file mode 100644 index bd5677aa..00000000 --- a/cheri/sail_latexcc/sailccmodint.tex +++ /dev/null @@ -1,7 +0,0 @@ -val mod_int = { - smt: "mod", - ocaml: "modulus", - lem: "integerMod", - c: "tmod_int", - coq: "Z.rem" -} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccmodulus.tex b/cheri/sail_latexcc/sailccmodulus.tex deleted file mode 100644 index ca23a339..00000000 --- a/cheri/sail_latexcc/sailccmodulus.tex +++ /dev/null @@ -1 +0,0 @@ -val modulus = {ocaml: "modulus", lem: "hardware_mod", coq: "euclid_modulo", _ : "tmod_int"} : forall 'n, 'n > 0 . (int, atom('n)) -> range(0, 'n - 1) diff --git a/cheri/sail_latexcc/sailccmultatom.tex b/cheri/sail_latexcc/sailccmultatom.tex deleted file mode 100644 index bbac3e2f..00000000 --- a/cheri/sail_latexcc/sailccmultatom.tex +++ /dev/null @@ -1,2 +0,0 @@ -val mult_atom = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : forall 'n 'm. - (atom('n), atom('m)) -> atom('n * 'm) diff --git a/cheri/sail_latexcc/sailccmultint.tex b/cheri/sail_latexcc/sailccmultint.tex deleted file mode 100644 index 08698e6f..00000000 --- a/cheri/sail_latexcc/sailccmultint.tex +++ /dev/null @@ -1 +0,0 @@ -val mult_int = {ocaml: "mult", lem: "integerMult", c: "mult_int", coq: "Z.mul"} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccnegate.tex b/cheri/sail_latexcc/sailccnegate.tex deleted file mode 100644 index ce000062..00000000 --- a/cheri/sail_latexcc/sailccnegate.tex +++ /dev/null @@ -1 +0,0 @@ -overload negate = {negate_range, negate_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccnegateatom.tex b/cheri/sail_latexcc/sailccnegateatom.tex deleted file mode 100644 index d1361e63..00000000 --- a/cheri/sail_latexcc/sailccnegateatom.tex +++ /dev/null @@ -1 +0,0 @@ -val negate_atom = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : forall 'n. atom('n) -> atom(- 'n) diff --git a/cheri/sail_latexcc/sailccnegateint.tex b/cheri/sail_latexcc/sailccnegateint.tex deleted file mode 100644 index 52375787..00000000 --- a/cheri/sail_latexcc/sailccnegateint.tex +++ /dev/null @@ -1 +0,0 @@ -val negate_int = {ocaml: "negate", lem: "integerNegate", c: "neg_int", coq: "Z.opp"} : int -> int diff --git a/cheri/sail_latexcc/sailccnegaterange.tex b/cheri/sail_latexcc/sailccnegaterange.tex deleted file mode 100644 index 7a4ad386..00000000 --- a/cheri/sail_latexcc/sailccnegaterange.tex +++ /dev/null @@ -1 +0,0 @@ -val negate_range = {ocaml: "minus_big_int", lem: "integerNegate", coq: "negate_range"} : forall 'n 'm. range('n, 'm) -> range(- 'm, - 'n) diff --git a/cheri/sail_latexcc/sailccneqanything.tex b/cheri/sail_latexcc/sailccneqanything.tex deleted file mode 100644 index a898649e..00000000 --- a/cheri/sail_latexcc/sailccneqanything.tex +++ /dev/null @@ -1 +0,0 @@ -val neq_anything = {lem: "neq", coq: "generic_neq"} : forall ('a : Type). ('a, 'a) -> bool diff --git a/cheri/sail_latexcc/sailccneqatom.tex b/cheri/sail_latexcc/sailccneqatom.tex deleted file mode 100644 index be777013..00000000 --- a/cheri/sail_latexcc/sailccneqatom.tex +++ /dev/null @@ -1 +0,0 @@ -val neq_atom = {lem: "neq", coq: "neq_atom"} : forall 'n 'm. (atom('n), atom('m)) -> bool diff --git a/cheri/sail_latexcc/sailccneqbool.tex b/cheri/sail_latexcc/sailccneqbool.tex deleted file mode 100644 index 0d80dc17..00000000 --- a/cheri/sail_latexcc/sailccneqbool.tex +++ /dev/null @@ -1 +0,0 @@ -val neq_bool : (bool, bool) -> bool diff --git a/cheri/sail_latexcc/sailccneqint.tex b/cheri/sail_latexcc/sailccneqint.tex deleted file mode 100644 index b233ca6b..00000000 --- a/cheri/sail_latexcc/sailccneqint.tex +++ /dev/null @@ -1 +0,0 @@ -val neq_int = {lem: "neq"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailccneqrange.tex b/cheri/sail_latexcc/sailccneqrange.tex deleted file mode 100644 index d2d8fb0c..00000000 --- a/cheri/sail_latexcc/sailccneqrange.tex +++ /dev/null @@ -1 +0,0 @@ -val neq_range = {lem: "neq"} : forall 'n 'm 'o 'p. (range('n, 'm), range('o, 'p)) -> bool diff --git a/cheri/sail_latexcc/sailccneqvec.tex b/cheri/sail_latexcc/sailccneqvec.tex deleted file mode 100644 index f655b3d8..00000000 --- a/cheri/sail_latexcc/sailccneqvec.tex +++ /dev/null @@ -1 +0,0 @@ -val neq_vec = {lem: "neq"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool diff --git a/cheri/sail_latexcc/sailccnot.tex b/cheri/sail_latexcc/sailccnot.tex deleted file mode 100644 index 515b3ef9..00000000 --- a/cheri/sail_latexcc/sailccnot.tex +++ /dev/null @@ -1 +0,0 @@ -val not = {coq:"negb", _:"not"} : bool -> bool diff --git a/cheri/sail_latexcc/sailccnotbool.tex b/cheri/sail_latexcc/sailccnotbool.tex deleted file mode 100644 index 7630f6c2..00000000 --- a/cheri/sail_latexcc/sailccnotbool.tex +++ /dev/null @@ -1 +0,0 @@ -val not_bool = {coq: "negb", _: "not"} : bool -> bool diff --git a/cheri/sail_latexcc/sailccnotvec.tex b/cheri/sail_latexcc/sailccnotvec.tex deleted file mode 100644 index a560a544..00000000 --- a/cheri/sail_latexcc/sailccnotvec.tex +++ /dev/null @@ -1 +0,0 @@ -val not_vec = {c:"not_bits", _:"not_vec"} : forall 'n. #\hyperref[zbits]{bits}#('n) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccnumofCPtrCmpOp.tex b/cheri/sail_latexcc/sailccnumofCPtrCmpOp.tex deleted file mode 100644 index 40f1bfa9..00000000 --- a/cheri/sail_latexcc/sailccnumofCPtrCmpOp.tex +++ /dev/null @@ -1 +0,0 @@ -val num_of_CPtrCmpOp : CPtrCmpOp -> {'e, 0 <= 'e & 'e <= 7. atom('e)} diff --git a/cheri/sail_latexcc/sailccnumofClearRegSet.tex b/cheri/sail_latexcc/sailccnumofClearRegSet.tex deleted file mode 100644 index 14ea7bea..00000000 --- a/cheri/sail_latexcc/sailccnumofClearRegSet.tex +++ /dev/null @@ -1 +0,0 @@ -val num_of_ClearRegSet : ClearRegSet -> {'e, 0 <= 'e & 'e <= 3. atom('e)} diff --git a/cheri/sail_latexcc/sailccones.tex b/cheri/sail_latexcc/sailccones.tex deleted file mode 100644 index 94fd805f..00000000 --- a/cheri/sail_latexcc/sailccones.tex +++ /dev/null @@ -1 +0,0 @@ -val ones : forall 'n, 'n >= 0 . unit -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccorbits.tex b/cheri/sail_latexcc/sailccorbits.tex deleted file mode 100644 index 55db5ffa..00000000 --- a/cheri/sail_latexcc/sailccorbits.tex +++ /dev/null @@ -1 +0,0 @@ -val or_bits = {c: "or_bits", _: "or_vec"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccorbool.tex b/cheri/sail_latexcc/sailccorbool.tex deleted file mode 100644 index 4b6bfa15..00000000 --- a/cheri/sail_latexcc/sailccorbool.tex +++ /dev/null @@ -1 +0,0 @@ -val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool diff --git a/cheri/sail_latexcc/sailccplainvectoraccess.tex b/cheri/sail_latexcc/sailccplainvectoraccess.tex deleted file mode 100644 index 94824f77..00000000 --- a/cheri/sail_latexcc/sailccplainvectoraccess.tex +++ /dev/null @@ -1,6 +0,0 @@ -val plain_vector_access = { - ocaml: "access", - lem: "access_list_dec", - coq: "vec_access_dec", - c: "vector_access" -} : forall ('n : Int) ('m : Int) ('a : Type), 0 <= 'm < 'n. (vector('n, dec, 'a), atom('m)) -> 'a diff --git a/cheri/sail_latexcc/sailccplainvectorupdate.tex b/cheri/sail_latexcc/sailccplainvectorupdate.tex deleted file mode 100644 index 6880d9bd..00000000 --- a/cheri/sail_latexcc/sailccplainvectorupdate.tex +++ /dev/null @@ -1,6 +0,0 @@ -val plain_vector_update = { - ocaml: "update", - lem: "update_list_dec", - coq: "vec_update_dec", - c: "vector_update" -} : forall '#\hyperref[zn]{n}# ('a : Type). (vector('n, dec, 'a), int, 'a) -> vector('n, dec, 'a) diff --git a/cheri/sail_latexcc/sailccpowtwo.tex b/cheri/sail_latexcc/sailccpowtwo.tex deleted file mode 100644 index 41da946e..00000000 --- a/cheri/sail_latexcc/sailccpowtwo.tex +++ /dev/null @@ -1 +0,0 @@ -val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) diff --git a/cheri/sail_latexcc/sailccprerrbits.tex b/cheri/sail_latexcc/sailccprerrbits.tex deleted file mode 100644 index 7d926384..00000000 --- a/cheri/sail_latexcc/sailccprerrbits.tex +++ /dev/null @@ -1 +0,0 @@ -val "prerr_bits" : forall 'n. (string, #\hyperref[zbits]{bits}#('n)) -> unit diff --git a/cheri/sail_latexcc/sailccprerrendline.tex b/cheri/sail_latexcc/sailccprerrendline.tex deleted file mode 100644 index ad4a94a0..00000000 --- a/cheri/sail_latexcc/sailccprerrendline.tex +++ /dev/null @@ -1 +0,0 @@ -val "prerr_endline" : string -> unit diff --git a/cheri/sail_latexcc/sailccprerrint.tex b/cheri/sail_latexcc/sailccprerrint.tex deleted file mode 100644 index ce7a7d61..00000000 --- a/cheri/sail_latexcc/sailccprerrint.tex +++ /dev/null @@ -1 +0,0 @@ -val "prerr_int" : (string, int) -> unit diff --git a/cheri/sail_latexcc/sailccprerrstring.tex b/cheri/sail_latexcc/sailccprerrstring.tex deleted file mode 100644 index 7b849da2..00000000 --- a/cheri/sail_latexcc/sailccprerrstring.tex +++ /dev/null @@ -1 +0,0 @@ -val "prerr_string" : string -> unit diff --git a/cheri/sail_latexcc/sailccprint.tex b/cheri/sail_latexcc/sailccprint.tex deleted file mode 100644 index 50a64219..00000000 --- a/cheri/sail_latexcc/sailccprint.tex +++ /dev/null @@ -1 +0,0 @@ -val print = "print_endline" : string -> unit diff --git a/cheri/sail_latexcc/sailccprintbits.tex b/cheri/sail_latexcc/sailccprintbits.tex deleted file mode 100644 index 8783a59a..00000000 --- a/cheri/sail_latexcc/sailccprintbits.tex +++ /dev/null @@ -1 +0,0 @@ -val "print_bits" : forall 'n. (string, #\hyperref[zbits]{bits}#('n)) -> unit diff --git a/cheri/sail_latexcc/sailccprintint.tex b/cheri/sail_latexcc/sailccprintint.tex deleted file mode 100644 index ddf33afc..00000000 --- a/cheri/sail_latexcc/sailccprintint.tex +++ /dev/null @@ -1 +0,0 @@ -val "print_int" : (string, int) -> unit diff --git a/cheri/sail_latexcc/sailccputchar.tex b/cheri/sail_latexcc/sailccputchar.tex deleted file mode 100644 index a123c709..00000000 --- a/cheri/sail_latexcc/sailccputchar.tex +++ /dev/null @@ -1 +0,0 @@ -val putchar = {c:"sail_putchar", _:"putchar"} : int -> unit diff --git a/cheri/sail_latexcc/sailccquotient.tex b/cheri/sail_latexcc/sailccquotient.tex deleted file mode 100644 index 7dba5359..00000000 --- a/cheri/sail_latexcc/sailccquotient.tex +++ /dev/null @@ -1 +0,0 @@ -val quotient = {ocaml: "quotient", lem: "integerDiv", coq: "Z.mod"} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccquotientnat.tex b/cheri/sail_latexcc/sailccquotientnat.tex deleted file mode 100644 index 14db4ae0..00000000 --- a/cheri/sail_latexcc/sailccquotientnat.tex +++ /dev/null @@ -1 +0,0 @@ -val quotient_nat = {ocaml: "quotient", lem: "integerDiv", coq: "Z.div"} : (nat, nat) -> nat diff --git a/cheri/sail_latexcc/sailccquotroundzzero.tex b/cheri/sail_latexcc/sailccquotroundzzero.tex deleted file mode 100644 index 9523cfcc..00000000 --- a/cheri/sail_latexcc/sailccquotroundzzero.tex +++ /dev/null @@ -1 +0,0 @@ -val quot_round_zero = {ocaml: "quot_round_zero", lem: "hardware_quot", coq: "Z.quot", _ : "tdiv_int"} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccregderef.tex b/cheri/sail_latexcc/sailccregderef.tex deleted file mode 100644 index 7f1dc7e8..00000000 --- a/cheri/sail_latexcc/sailccregderef.tex +++ /dev/null @@ -1 +0,0 @@ -val _reg_deref = "reg_deref" : forall ('a : Type). #\hyperref[zregister]{register}#('a) -> 'a diff --git a/cheri/sail_latexcc/sailccremroundzzero.tex b/cheri/sail_latexcc/sailccremroundzzero.tex deleted file mode 100644 index 9d8113ba..00000000 --- a/cheri/sail_latexcc/sailccremroundzzero.tex +++ /dev/null @@ -1 +0,0 @@ -val rem_round_zero = {ocaml: "rem_round_zero", lem: "hardware_mod", coq: "Z.rem", _ : "tmod_int"} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccreplicatebits.tex b/cheri/sail_latexcc/sailccreplicatebits.tex deleted file mode 100644 index cd7a97d7..00000000 --- a/cheri/sail_latexcc/sailccreplicatebits.tex +++ /dev/null @@ -1 +0,0 @@ -val replicate_bits = "replicate_bits" : forall 'n 'm. (#\hyperref[zbits]{bits}#('n), atom('m)) -> #\hyperref[zbits]{bits}#('n * 'm) diff --git a/cheri/sail_latexcc/sailccroundUp.tex b/cheri/sail_latexcc/sailccroundUp.tex deleted file mode 100644 index b7e31074..00000000 --- a/cheri/sail_latexcc/sailccroundUp.tex +++ /dev/null @@ -1 +0,0 @@ -val roundUp : range(0, 45) -> range(0, 48) diff --git a/cheri/sail_latexcc/sailccsailccnegatev.tex b/cheri/sail_latexcc/sailccsailccnegatev.tex deleted file mode 100644 index 4f7aea58..00000000 --- a/cheri/sail_latexcc/sailccsailccnegatev.tex +++ /dev/null @@ -1 +0,0 @@ -overload negate = {negate_atom, negate_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailccregderefv.tex b/cheri/sail_latexcc/sailccsailccregderefv.tex deleted file mode 100644 index f5de92ca..00000000 --- a/cheri/sail_latexcc/sailccsailccregderefv.tex +++ /dev/null @@ -1 +0,0 @@ -val "reg_deref" : forall ('a : Type). #\hyperref[zregister]{register}#('a) -> 'a effect {rreg} diff --git a/cheri/sail_latexcc/sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv.tex b/cheri/sail_latexcc/sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv.tex deleted file mode 100644 index 0f72fdc9..00000000 --- a/cheri/sail_latexcc/sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator ==) = {eq_bit2}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex deleted file mode 100644 index eacd556c..00000000 --- a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator +) = {add_atom, add_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozFzninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozFzninevv.tex deleted file mode 100644 index 73c40722..00000000 --- a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozFzninevv.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator /) = {div}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex deleted file mode 100644 index 47b1d0f6..00000000 --- a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator ==) = {eq_atom, eq_range, eq_int, eq_bool}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozfivezninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozfivezninevv.tex deleted file mode 100644 index 552e0c24..00000000 --- a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozfivezninevv.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator %) = {mod}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex deleted file mode 100644 index afe7a721..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator *) = {mult_atom, mult_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozBzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozBzninev.tex deleted file mode 100644 index ddc56bfd..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozBzninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator +) = {add_bits, add_bits_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozDzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozDzninev.tex deleted file mode 100644 index 5d12fdf1..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozDzninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator -) = {sub_atom, sub_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozFzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozFzninev.tex deleted file mode 100644 index 38e9124b..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozFzninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator /) = {div_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex deleted file mode 100644 index 1314a962..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator ==) = {eq_bit, eq_bits}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozQzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozQzninev.tex deleted file mode 100644 index 05769645..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozQzninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator ^) = {sail_mask}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex deleted file mode 100644 index 1ebacbc4..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator |) = {or_bool}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex deleted file mode 100644 index 14fa73b8..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator %) = {mod_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex deleted file mode 100644 index 527cf596..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator !=) = {neq_atom, neq_range, neq_int, neq_bool}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozsixzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozsixzninev.tex deleted file mode 100644 index be6f29ef..00000000 --- a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozsixzninev.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator &) = {and_bool}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailmask.tex b/cheri/sail_latexcc/sailccsailmask.tex deleted file mode 100644 index 45862747..00000000 --- a/cheri/sail_latexcc/sailccsailmask.tex +++ /dev/null @@ -1 +0,0 @@ -val sail_mask : forall 'len 'v, 'len >= 0 & 'v >= 0. (atom('len), vector('v, dec, bit)) -> vector('len, dec, bit) diff --git a/cheri/sail_latexcc/sailccsailsignextend.tex b/cheri/sail_latexcc/sailccsailsignextend.tex deleted file mode 100644 index dfaa5c86..00000000 --- a/cheri/sail_latexcc/sailccsailsignextend.tex +++ /dev/null @@ -1 +0,0 @@ -val sail_sign_extend = "sign_extend" : forall 'n 'm, 'm >= 'n. (#\hyperref[zbits]{bits}#('n), atom('m)) -> #\hyperref[zbits]{bits}#('m) diff --git a/cheri/sail_latexcc/sailccsailzzeroextend.tex b/cheri/sail_latexcc/sailccsailzzeroextend.tex deleted file mode 100644 index 53f6fff9..00000000 --- a/cheri/sail_latexcc/sailccsailzzeroextend.tex +++ /dev/null @@ -1 +0,0 @@ -val sail_zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (#\hyperref[zbits]{bits}#('n), atom('m)) -> #\hyperref[zbits]{bits}#('m) diff --git a/cheri/sail_latexcc/sailccsailzzeros.tex b/cheri/sail_latexcc/sailccsailzzeros.tex deleted file mode 100644 index 9c60aa12..00000000 --- a/cheri/sail_latexcc/sailccsailzzeros.tex +++ /dev/null @@ -1 +0,0 @@ -val sail_zeros = "zeros" : forall 'n. atom('n) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccsealCap.tex b/cheri/sail_latexcc/sailccsealCap.tex deleted file mode 100644 index 891ae279..00000000 --- a/cheri/sail_latexcc/sailccsealCap.tex +++ /dev/null @@ -1 +0,0 @@ -val sealCap : (CapStruct, bits(24)) -> (bool, CapStruct) diff --git a/cheri/sail_latexcc/sailccsetCapBounds.tex b/cheri/sail_latexcc/sailccsetCapBounds.tex deleted file mode 100644 index 94fbecaf..00000000 --- a/cheri/sail_latexcc/sailccsetCapBounds.tex +++ /dev/null @@ -1 +0,0 @@ -val setCapBounds : (CapStruct, bits(64), bits(65)) -> (bool, CapStruct) effect {escape} diff --git a/cheri/sail_latexcc/sailccsetCapOffset.tex b/cheri/sail_latexcc/sailccsetCapOffset.tex deleted file mode 100644 index fef324f7..00000000 --- a/cheri/sail_latexcc/sailccsetCapOffset.tex +++ /dev/null @@ -1 +0,0 @@ -val setCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct) diff --git a/cheri/sail_latexcc/sailccsetCapPerms.tex b/cheri/sail_latexcc/sailccsetCapPerms.tex deleted file mode 100644 index 617f19fb..00000000 --- a/cheri/sail_latexcc/sailccsetCapPerms.tex +++ /dev/null @@ -1 +0,0 @@ -val setCapPerms : (CapStruct, bits(31)) -> CapStruct diff --git a/cheri/sail_latexcc/sailccsetslicebits.tex b/cheri/sail_latexcc/sailccsetslicebits.tex deleted file mode 100644 index 8a81bff5..00000000 --- a/cheri/sail_latexcc/sailccsetslicebits.tex +++ /dev/null @@ -1,2 +0,0 @@ -val set_slice_bits = "set_slice" : forall 'n 'm. - (atom('n), atom('m), #\hyperref[zbits]{bits}#('n), int, #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccsetsliceint.tex b/cheri/sail_latexcc/sailccsetsliceint.tex deleted file mode 100644 index 413bf721..00000000 --- a/cheri/sail_latexcc/sailccsetsliceint.tex +++ /dev/null @@ -1 +0,0 @@ -val set_slice_int = "set_slice_int" : forall 'w. (atom('w), int, int, #\hyperref[zbits]{bits}#('w)) -> int diff --git a/cheri/sail_latexcc/sailccshiftbitsleft.tex b/cheri/sail_latexcc/sailccshiftbitsleft.tex deleted file mode 100644 index cdb2eb6a..00000000 --- a/cheri/sail_latexcc/sailccshiftbitsleft.tex +++ /dev/null @@ -1 +0,0 @@ -val "shift_bits_left" : forall 'n 'm. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n) effect {undef} diff --git a/cheri/sail_latexcc/sailccshiftbitsright.tex b/cheri/sail_latexcc/sailccshiftbitsright.tex deleted file mode 100644 index dbc72b11..00000000 --- a/cheri/sail_latexcc/sailccshiftbitsright.tex +++ /dev/null @@ -1 +0,0 @@ -val "shift_bits_right" : forall 'n 'm. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n) effect {undef} diff --git a/cheri/sail_latexcc/sailccshiftl.tex b/cheri/sail_latexcc/sailccshiftl.tex deleted file mode 100644 index b2c54c27..00000000 --- a/cheri/sail_latexcc/sailccshiftl.tex +++ /dev/null @@ -1 +0,0 @@ -val "shiftl" : forall 'm 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('m), atom('n)) -> #\hyperref[zbits]{bits}#('m) diff --git a/cheri/sail_latexcc/sailccshiftr.tex b/cheri/sail_latexcc/sailccshiftr.tex deleted file mode 100644 index f282dcbe..00000000 --- a/cheri/sail_latexcc/sailccshiftr.tex +++ /dev/null @@ -1 +0,0 @@ -val "shiftr" : forall 'm 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('m), atom('n)) -> #\hyperref[zbits]{bits}#('m) diff --git a/cheri/sail_latexcc/sailccshlint.tex b/cheri/sail_latexcc/sailccshlint.tex deleted file mode 100644 index 8ffbcf6c..00000000 --- a/cheri/sail_latexcc/sailccshlint.tex +++ /dev/null @@ -1 +0,0 @@ -val shl_int = "shl_int" : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccshrint.tex b/cheri/sail_latexcc/sailccshrint.tex deleted file mode 100644 index 087c17bb..00000000 --- a/cheri/sail_latexcc/sailccshrint.tex +++ /dev/null @@ -1 +0,0 @@ -val shr_int = "shr_int" : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccsigned.tex b/cheri/sail_latexcc/sailccsigned.tex deleted file mode 100644 index dcdc3049..00000000 --- a/cheri/sail_latexcc/sailccsigned.tex +++ /dev/null @@ -1,4 +0,0 @@ -val signed = { - c: "sail_signed", - _: "sint" -} : forall 'n, 'n > 0. #\hyperref[zbits]{bits}#('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) diff --git a/cheri/sail_latexcc/sailccsignextend.tex b/cheri/sail_latexcc/sailccsignextend.tex deleted file mode 100644 index 03f56369..00000000 --- a/cheri/sail_latexcc/sailccsignextend.tex +++ /dev/null @@ -1 +0,0 @@ -overload sign_extend = {mips_sign_extend}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccslice.tex b/cheri/sail_latexcc/sailccslice.tex deleted file mode 100644 index b9bb5a70..00000000 --- a/cheri/sail_latexcc/sailccslice.tex +++ /dev/null @@ -1,2 +0,0 @@ -val slice = "slice" : forall 'n 'm 'o, 0 <= 'o < 'm & 'o + 'n <= 'm & 0 <= 'n. - (#\hyperref[zbits]{bits}#('m), atom('o), atom('n)) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccstringofint.tex b/cheri/sail_latexcc/sailccstringofint.tex deleted file mode 100644 index 05edaa20..00000000 --- a/cheri/sail_latexcc/sailccstringofint.tex +++ /dev/null @@ -1 +0,0 @@ -val string_of_int = "string_of_int" : int -> string diff --git a/cheri/sail_latexcc/sailccsubatom.tex b/cheri/sail_latexcc/sailccsubatom.tex deleted file mode 100644 index 437e2d4c..00000000 --- a/cheri/sail_latexcc/sailccsubatom.tex +++ /dev/null @@ -1,2 +0,0 @@ -val sub_atom = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : forall 'n 'm. - (atom('n), atom('m)) -> atom('n - 'm) diff --git a/cheri/sail_latexcc/sailccsubint.tex b/cheri/sail_latexcc/sailccsubint.tex deleted file mode 100644 index 11fdf922..00000000 --- a/cheri/sail_latexcc/sailccsubint.tex +++ /dev/null @@ -1 +0,0 @@ -val sub_int = {ocaml: "sub_int", lem: "integerMinus", c: "sub_int", coq: "Z.sub"} : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccsubrange.tex b/cheri/sail_latexcc/sailccsubrange.tex deleted file mode 100644 index 2aad56b6..00000000 --- a/cheri/sail_latexcc/sailccsubrange.tex +++ /dev/null @@ -1,2 +0,0 @@ -val sub_range = {ocaml: "sub_int", lem: "integerMinus", coq: "sub_range"} : forall 'n 'm 'o 'p. - (range('n, 'm), range('o, 'p)) -> range('n - 'p, 'm - 'o) diff --git a/cheri/sail_latexcc/sailccsubvec.tex b/cheri/sail_latexcc/sailccsubvec.tex deleted file mode 100644 index b92f07a4..00000000 --- a/cheri/sail_latexcc/sailccsubvec.tex +++ /dev/null @@ -1 +0,0 @@ -val sub_vec = {c : "sub_bits", _:"sub_vec"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccsubvecint.tex b/cheri/sail_latexcc/sailccsubvecint.tex deleted file mode 100644 index 70bf667e..00000000 --- a/cheri/sail_latexcc/sailccsubvecint.tex +++ /dev/null @@ -1 +0,0 @@ -val sub_vec_int = {c:"sub_bits_int", _: "sub_vec_int"} : forall 'n. (#\hyperref[zbits]{bits}#('n), int) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailcctobits.tex b/cheri/sail_latexcc/sailcctobits.tex deleted file mode 100644 index 9dd3c655..00000000 --- a/cheri/sail_latexcc/sailcctobits.tex +++ /dev/null @@ -1 +0,0 @@ -val to_bits : forall 'l, 'l >= 0 .(atom('l), int) -> #\hyperref[zbits]{bits}#('l) diff --git a/cheri/sail_latexcc/sailcctruncate.tex b/cheri/sail_latexcc/sailcctruncate.tex deleted file mode 100644 index 5f7760f3..00000000 --- a/cheri/sail_latexcc/sailcctruncate.tex +++ /dev/null @@ -1,6 +0,0 @@ -val truncate = { - ocaml: "vector_truncate", - lem: "vector_truncate", - coq: "vector_truncate", - c: "sail_truncate" -} : forall 'm 'n, 'm >= 0 & 'm <= 'n. (vector('n, dec, bit), atom('m)) -> vector('m, dec, bit) diff --git a/cheri/sail_latexcc/sailccuintsixfour.tex b/cheri/sail_latexcc/sailccuintsixfour.tex deleted file mode 100644 index a0d52c8f..00000000 --- a/cheri/sail_latexcc/sailccuintsixfour.tex +++ /dev/null @@ -1 +0,0 @@ -type uint64 = range(0, (2 ^ 64) - 1) diff --git a/cheri/sail_latexcc/sailccunsigned.tex b/cheri/sail_latexcc/sailccunsigned.tex deleted file mode 100644 index 47867039..00000000 --- a/cheri/sail_latexcc/sailccunsigned.tex +++ /dev/null @@ -1,7 +0,0 @@ -val unsigned = { - ocaml: "uint", - lem: "uint", - interpreter: "uint", - c: "sail_unsigned", - coq: "uint" -} : forall 'n. #\hyperref[zbits]{bits}#('n) -> range(0, 2 ^ 'n - 1) diff --git a/cheri/sail_latexcc/sailccvectoraccess.tex b/cheri/sail_latexcc/sailccvectoraccess.tex deleted file mode 100644 index a8e8074f..00000000 --- a/cheri/sail_latexcc/sailccvectoraccess.tex +++ /dev/null @@ -1 +0,0 @@ -overload vector_access = {bitvector_access, plain_vector_access}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccvectorlength.tex b/cheri/sail_latexcc/sailccvectorlength.tex deleted file mode 100644 index f41d5bfa..00000000 --- a/cheri/sail_latexcc/sailccvectorlength.tex +++ /dev/null @@ -1,6 +0,0 @@ -val vector_length = { - ocaml: "length", - lem: "length_list", - c: "length", - coq: "vec_length" -} : forall '#\hyperref[zn]{n}# ('a : Type). vector('n, dec, 'a) -> atom('n) diff --git a/cheri/sail_latexcc/sailccvectorsubrange.tex b/cheri/sail_latexcc/sailccvectorsubrange.tex deleted file mode 100644 index c069c7b6..00000000 --- a/cheri/sail_latexcc/sailccvectorsubrange.tex +++ /dev/null @@ -1,7 +0,0 @@ -val vector_subrange = { - ocaml: "subrange", - lem: "subrange_vec_dec", - c: "vector_subrange", - coq: "subrange_vec_dec" -} : forall ('n : Int) ('m : Int) ('o : Int), 0 <= 'o <= 'm < 'n. - (#\hyperref[zbits]{bits}#('n), atom('m), atom('o)) -> #\hyperref[zbits]{bits}#('m - 'o + 1) diff --git a/cheri/sail_latexcc/sailccvectorupdate.tex b/cheri/sail_latexcc/sailccvectorupdate.tex deleted file mode 100644 index 1ec4aaef..00000000 --- a/cheri/sail_latexcc/sailccvectorupdate.tex +++ /dev/null @@ -1 +0,0 @@ -overload vector_update = {bitvector_update, plain_vector_update}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccvectorupdatesubrange.tex b/cheri/sail_latexcc/sailccvectorupdatesubrange.tex deleted file mode 100644 index 6ff4f9f6..00000000 --- a/cheri/sail_latexcc/sailccvectorupdatesubrange.tex +++ /dev/null @@ -1,6 +0,0 @@ -val vector_update_subrange = { - ocaml: "update_subrange", - lem: "update_subrange_vec_dec", - c: "vector_update_subrange", - coq: "update_subrange_vec_dec" -} : forall 'n 'm 'o. (#\hyperref[zbits]{bits}#('n), atom('m), atom('o), #\hyperref[zbits]{bits}#('m - ('o - 1))) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailccxorvec.tex b/cheri/sail_latexcc/sailccxorvec.tex deleted file mode 100644 index b3aa7372..00000000 --- a/cheri/sail_latexcc/sailccxorvec.tex +++ /dev/null @@ -1 +0,0 @@ -val xor_vec = {c: "xor_bits" , _: "xor_vec"} : forall 'n. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#('n) diff --git a/cheri/sail_latexcc/sailcczW.tex b/cheri/sail_latexcc/sailcczW.tex deleted file mode 100644 index a29ec93f..00000000 --- a/cheri/sail_latexcc/sailcczW.tex +++ /dev/null @@ -1 +0,0 @@ -overload ~ = {not_bool, not_vec}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozAsznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozAsznine.tex deleted file mode 100644 index 0b0a46e2..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozAsznine.tex +++ /dev/null @@ -1 +0,0 @@ -val operator *_s = "mults_vec" : forall 'n . (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#(2 * 'n) diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozAuznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozAuznine.tex deleted file mode 100644 index 5b762ba7..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozAuznine.tex +++ /dev/null @@ -1 +0,0 @@ -val operator *_u = "mult_vec" : forall 'n . (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> #\hyperref[zbits]{bits}#(2 * 'n) diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozAznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozAznine.tex deleted file mode 100644 index 2d188f63..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozAznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator *) = {mult_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozBznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozBznine.tex deleted file mode 100644 index 432e85e5..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozBznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator +) = {add_range, add_int, add_vec, add_vec_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozDznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozDznine.tex deleted file mode 100644 index d671e6b0..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozDznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator -) = {sub_range, sub_int, sub_vec, sub_vec_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozFznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozFznine.tex deleted file mode 100644 index 3c2e441c..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozFznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator /) = {quotient_nat, quotient}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIsznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIsznine.tex deleted file mode 100644 index 9b4ebe19..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIsznine.tex +++ /dev/null @@ -1 +0,0 @@ -val operator <_s : forall 'n, 'n > 0. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIuznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIuznine.tex deleted file mode 100644 index 5b54235e..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIuznine.tex +++ /dev/null @@ -1 +0,0 @@ -val operator <_u : forall 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIzIznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIzIznine.tex deleted file mode 100644 index 51ff2b6c..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIzIznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator <<) = {shift_bits_left, shiftl}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIzJznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIzJznine.tex deleted file mode 100644 index d23f28dd..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIzJznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator <=) = {lteq_atom, lteq_range_atom, lteq_atom_range, lteq_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozIznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozIznine.tex deleted file mode 100644 index 8e5e3fe9..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozIznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator <) = {lt_atom, lt_range_atom, lt_atom_range, lt_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozJzJznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozJzJznine.tex deleted file mode 100644 index 57ea823c..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozJzJznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator ==) = {eq_anything}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex deleted file mode 100644 index 032e8600..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex +++ /dev/null @@ -1 +0,0 @@ -val operator >=_s : forall 'n, 'n > 0. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJuznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJuznine.tex deleted file mode 100644 index eaa72e60..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJuznine.tex +++ /dev/null @@ -1 +0,0 @@ -val operator >=_u : forall 'n, 'n >= 0. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('n)) -> bool diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJznine.tex deleted file mode 100644 index 5733b740..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator >=) = {gteq_atom, gteq_range_atom, gteq_atom_range, gteq_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKsznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKsznine.tex deleted file mode 100644 index 0f0793a6..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKsznine.tex +++ /dev/null @@ -1 +0,0 @@ -val operator >>_s = "shift_bits_right_arith" : forall 'n 'm. (#\hyperref[zbits]{bits}#('n), #\hyperref[zbits]{bits}#('m)) -> #\hyperref[zbits]{bits}#('n) effect {undef} diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKznine.tex deleted file mode 100644 index b129e9d2..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator >>) = {shift_bits_right, shiftr}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKznine.tex deleted file mode 100644 index a8da7e48..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozKznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator >) = {gt_atom, gt_range_atom, gt_atom_range, gt_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozQzQznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozQzQznine.tex deleted file mode 100644 index 185f501e..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozQzQznine.tex +++ /dev/null @@ -1 +0,0 @@ -val operator ^^ = {lem: "replicate_bits"} : forall 'n 'm, 'm >= 0 . (#\hyperref[zbits]{bits}#('n), atom('m)) -> #\hyperref[zbits]{bits}#('n * 'm) diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozQznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozQznine.tex deleted file mode 100644 index 106b6064..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozQznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator ^) = {xor_vec, int_power}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozUznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozUznine.tex deleted file mode 100644 index 4de737e0..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozUznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator |) = {or_bool, or_bits}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozfiveznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozfiveznine.tex deleted file mode 100644 index 8d6b54c3..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozfiveznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator %) = {modulus}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex deleted file mode 100644 index 22052668..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator !=) = {neq_atom, neq_int, neq_vec, neq_anything}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozsixznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozsixznine.tex deleted file mode 100644 index 248fb15e..00000000 --- a/cheri/sail_latexcc/sailcczeightoperatorzzerozsixznine.tex +++ /dev/null @@ -1 +0,0 @@ -overload (operator &) = {and_bool, and_bits}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczzeroextend.tex b/cheri/sail_latexcc/sailcczzeroextend.tex deleted file mode 100644 index 0f754d44..00000000 --- a/cheri/sail_latexcc/sailcczzeroextend.tex +++ /dev/null @@ -1 +0,0 @@ -overload zero_extend = {mips_zero_extend}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczzeros.tex b/cheri/sail_latexcc/sailcczzeros.tex deleted file mode 100644 index 1c251eda..00000000 --- a/cheri/sail_latexcc/sailcczzeros.tex +++ /dev/null @@ -1 +0,0 @@ -val zeros : forall 'n, 'n >= 0 . unit -> #\hyperref[zbits]{bits}#('n) |