diff options
| author | Peter Sewell | 2018-07-27 18:52:40 +0100 |
|---|---|---|
| committer | Peter Sewell | 2018-07-27 18:52:40 +0100 |
| commit | 34c745ff78a409daeddf4b5a78e28c85c62eb6fd (patch) | |
| tree | e9f391cab299f83953a489992de590cbb220c983 | |
| parent | 4c84c70eafbbf9bea475e3264f21eedc3555021f (diff) | |
Revert "wib" (mistaken delete of sail_latexcc)
This reverts commit 4c84c70eafbbf9bea475e3264f21eedc3555021f.
273 files changed, 1165 insertions, 9 deletions
diff --git a/cheri/Makefile b/cheri/Makefile index 3074cd96..0d207391 100644 --- a/cheri/Makefile +++ b/cheri/Makefile @@ -61,15 +61,6 @@ latex_256: $(CHERI_SAILS) latex: latex_128 latex_256 -# to install latex in the right place - specific to PS checkouts -CHERI_ARCH_PATH=/home/pes20/ctsrd/ctsrd/reports/cheri-architecture -install_latex: - rm -rf $(CHERI_ARCH_PATH)/sail_latex/*.tex - cp sail_latex/*.tex $(CHERI_ARCH_PATH)/sail_latex - -#rm -rf $(CHERI_ARCH_PATH)/sail_latexcc/*.tex -#cp sail_latexcc/*.tex $(CHERI_ARCH_PATH)/sail_latexcc - cheri128: $(CHERI128_SAILS) $(CHERI_MAIN) $(SAIL) -ocaml -o $@ $^ diff --git a/cheri/sail_latexcc/commands.tex b/cheri/sail_latexcc/commands.tex new file mode 100644 index 00000000..8b9678a1 --- /dev/null +++ b/cheri/sail_latexcc/commands.tex @@ -0,0 +1,544 @@ +\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 new file mode 100644 index 00000000..a0d408ab --- /dev/null +++ b/cheri/sail_latexcc/sailccBitStr.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..cb0a73ae --- /dev/null +++ b/cheri/sail_latexcc/sailccCPtrCmpOp.tex @@ -0,0 +1,10 @@ +enum CPtrCmpOp = { + CEQ, + CNE, + CLT, + CLE, + CLTU, + CLEU, + CEXEQ, + CNEXEQ +} diff --git a/cheri/sail_latexcc/sailccCPtrCmpOpofnum.tex b/cheri/sail_latexcc/sailccCPtrCmpOpofnum.tex new file mode 100644 index 00000000..bd6ca31c --- /dev/null +++ b/cheri/sail_latexcc/sailccCPtrCmpOpofnum.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..812f45ff --- /dev/null +++ b/cheri/sail_latexcc/sailccCapLen.tex @@ -0,0 +1 @@ +type CapLen = range(0, 2 ^ 65) diff --git a/cheri/sail_latexcc/sailccCapReg.tex b/cheri/sail_latexcc/sailccCapReg.tex new file mode 100644 index 00000000..702141d9 --- /dev/null +++ b/cheri/sail_latexcc/sailccCapReg.tex @@ -0,0 +1 @@ +type CapReg = #\hyperref[zbits]{bits}#(129) diff --git a/cheri/sail_latexcc/sailccCapStruct.tex b/cheri/sail_latexcc/sailccCapStruct.tex new file mode 100644 index 00000000..b1df7ec5 --- /dev/null +++ b/cheri/sail_latexcc/sailccCapStruct.tex @@ -0,0 +1,22 @@ +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 new file mode 100644 index 00000000..c04ea7d4 --- /dev/null +++ b/cheri/sail_latexcc/sailccClearRegSet.tex @@ -0,0 +1,6 @@ +enum ClearRegSet = { +GPLo, +GPHi, +CLo, +CHi +} diff --git a/cheri/sail_latexcc/sailccClearRegSetofnum.tex b/cheri/sail_latexcc/sailccClearRegSetofnum.tex new file mode 100644 index 00000000..c73d36d9 --- /dev/null +++ b/cheri/sail_latexcc/sailccClearRegSetofnum.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..eb8a5e36 --- /dev/null +++ b/cheri/sail_latexcc/sailccHighestSetBit.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..92ca59cc --- /dev/null +++ b/cheri/sail_latexcc/sailccMIPSread.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..cc67fa20 --- /dev/null +++ b/cheri/sail_latexcc/sailccMIPSwrite.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..68d629a6 --- /dev/null +++ b/cheri/sail_latexcc/sailccReadRAM.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..2ed4aca2 --- /dev/null +++ b/cheri/sail_latexcc/sailccWriteRAM.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..5164ef32 --- /dev/null +++ b/cheri/sail_latexcc/sailccabsatom.tex @@ -0,0 +1,7 @@ +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 new file mode 100644 index 00000000..d3b67cfb --- /dev/null +++ b/cheri/sail_latexcc/sailccabsint.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..8b6ac810 --- /dev/null +++ b/cheri/sail_latexcc/sailccaddatom.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..95f653d1 --- /dev/null +++ b/cheri/sail_latexcc/sailccaddbits.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..ee9a8aa2 --- /dev/null +++ b/cheri/sail_latexcc/sailccaddbitsint.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..9fe5b078 --- /dev/null +++ b/cheri/sail_latexcc/sailccaddint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..fbf498b1 --- /dev/null +++ b/cheri/sail_latexcc/sailccaddrange.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..bb625afe --- /dev/null +++ b/cheri/sail_latexcc/sailccaddvec.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..189ad4aa --- /dev/null +++ b/cheri/sail_latexcc/sailccaddvecint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..8e35bd5b --- /dev/null +++ b/cheri/sail_latexcc/sailccandbits.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..926dce9f --- /dev/null +++ b/cheri/sail_latexcc/sailccandbool.tex @@ -0,0 +1 @@ +val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool diff --git a/cheri/sail_latexcc/sailccappend.tex b/cheri/sail_latexcc/sailccappend.tex new file mode 100644 index 00000000..56c12116 --- /dev/null +++ b/cheri/sail_latexcc/sailccappend.tex @@ -0,0 +1 @@ +overload append = {bitvector_concat}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccappendsixfour.tex b/cheri/sail_latexcc/sailccappendsixfour.tex new file mode 100644 index 00000000..633593b3 --- /dev/null +++ b/cheri/sail_latexcc/sailccappendsixfour.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..13bbaf7b --- /dev/null +++ b/cheri/sail_latexcc/sailccatopcorrection.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..88255b5a --- /dev/null +++ b/cheri/sail_latexcc/sailccbits.tex @@ -0,0 +1 @@ +type #\hyperref[zbits]{bits}# ('n : Int) = vector('n, dec, bit) diff --git a/cheri/sail_latexcc/sailccbitstobool.tex b/cheri/sail_latexcc/sailccbitstobool.tex new file mode 100644 index 00000000..17cb3483 --- /dev/null +++ b/cheri/sail_latexcc/sailccbitstobool.tex @@ -0,0 +1 @@ +val cast bits_to_bool : #\hyperref[zbits]{bits}#(1) -> bool diff --git a/cheri/sail_latexcc/sailccbittobool.tex b/cheri/sail_latexcc/sailccbittobool.tex new file mode 100644 index 00000000..13a2dfb8 --- /dev/null +++ b/cheri/sail_latexcc/sailccbittobool.tex @@ -0,0 +1 @@ +val cast bit_to_bool : bit -> bool diff --git a/cheri/sail_latexcc/sailccbitvectoraccess.tex b/cheri/sail_latexcc/sailccbitvectoraccess.tex new file mode 100644 index 00000000..4bb98eb8 --- /dev/null +++ b/cheri/sail_latexcc/sailccbitvectoraccess.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..afc03901 --- /dev/null +++ b/cheri/sail_latexcc/sailccbitvectorconcat.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..ac601acd --- /dev/null +++ b/cheri/sail_latexcc/sailccbitvectorlength.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..6524146e --- /dev/null +++ b/cheri/sail_latexcc/sailccbitvectorupdate.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..711ab763 --- /dev/null +++ b/cheri/sail_latexcc/sailccbooltobits.tex @@ -0,0 +1 @@ +val cast bool_to_bits : bool -> #\hyperref[zbits]{bits}#(1) diff --git a/cheri/sail_latexcc/sailcccapRegToCapStruct.tex b/cheri/sail_latexcc/sailcccapRegToCapStruct.tex new file mode 100644 index 00000000..bd64d554 --- /dev/null +++ b/cheri/sail_latexcc/sailcccapRegToCapStruct.tex @@ -0,0 +1 @@ +val capRegToCapStruct : CapReg -> CapStruct diff --git a/cheri/sail_latexcc/sailcccapStructToCapReg.tex b/cheri/sail_latexcc/sailcccapStructToCapReg.tex new file mode 100644 index 00000000..b5409845 --- /dev/null +++ b/cheri/sail_latexcc/sailcccapStructToCapReg.tex @@ -0,0 +1 @@ +val capStructToCapReg : CapStruct -> CapReg diff --git a/cheri/sail_latexcc/sailcccapStructToMemBits.tex b/cheri/sail_latexcc/sailcccapStructToMemBits.tex new file mode 100644 index 00000000..4a49e9c0 --- /dev/null +++ b/cheri/sail_latexcc/sailcccapStructToMemBits.tex @@ -0,0 +1 @@ +val capStructToMemBits : CapStruct -> bits(128) diff --git a/cheri/sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex b/cheri/sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex new file mode 100644 index 00000000..8f3a8d0f --- /dev/null +++ b/cheri/sail_latexcc/sailcccapStructToMemBitsonetwoeight.tex @@ -0,0 +1 @@ +val capStructToMemBits128 : CapStruct -> bits(128) diff --git a/cheri/sail_latexcc/sailcccastunitvec.tex b/cheri/sail_latexcc/sailcccastunitvec.tex new file mode 100644 index 00000000..e0391ded --- /dev/null +++ b/cheri/sail_latexcc/sailcccastunitvec.tex @@ -0,0 +1 @@ +val cast cast_unit_vec : bit -> #\hyperref[zbits]{bits}#(1) diff --git a/cheri/sail_latexcc/sailcccomputeE.tex b/cheri/sail_latexcc/sailcccomputeE.tex new file mode 100644 index 00000000..893cea49 --- /dev/null +++ b/cheri/sail_latexcc/sailcccomputeE.tex @@ -0,0 +1 @@ +val computeE : bits(65) -> range(0, 48) effect {escape} diff --git a/cheri/sail_latexcc/sailccconcatstr.tex b/cheri/sail_latexcc/sailccconcatstr.tex new file mode 100644 index 00000000..07556728 --- /dev/null +++ b/cheri/sail_latexcc/sailccconcatstr.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..58318fe9 --- /dev/null +++ b/cheri/sail_latexcc/sailccdiv.tex @@ -0,0 +1,7 @@ +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 new file mode 100644 index 00000000..34ae6121 --- /dev/null +++ b/cheri/sail_latexcc/sailccdivint.tex @@ -0,0 +1,7 @@ +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 new file mode 100644 index 00000000..9b5d3c92 --- /dev/null +++ b/cheri/sail_latexcc/sailcceqanything.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..0325ab15 --- /dev/null +++ b/cheri/sail_latexcc/sailcceqatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..205d3436 --- /dev/null +++ b/cheri/sail_latexcc/sailcceqbit.tex @@ -0,0 +1 @@ +val eq_bit = { lem : "eq", _ : "eq_bit" } : (bit, bit) -> bool diff --git a/cheri/sail_latexcc/sailcceqbits.tex b/cheri/sail_latexcc/sailcceqbits.tex new file mode 100644 index 00000000..e78ed19a --- /dev/null +++ b/cheri/sail_latexcc/sailcceqbits.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..59353940 --- /dev/null +++ b/cheri/sail_latexcc/sailcceqbittwo.tex @@ -0,0 +1 @@ +val eq_bit2 = "eq_bit" : (bit, bit) -> bool diff --git a/cheri/sail_latexcc/sailcceqbool.tex b/cheri/sail_latexcc/sailcceqbool.tex new file mode 100644 index 00000000..4d2c346b --- /dev/null +++ b/cheri/sail_latexcc/sailcceqbool.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..4c0462c1 --- /dev/null +++ b/cheri/sail_latexcc/sailcceqint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..7f1cd5f2 --- /dev/null +++ b/cheri/sail_latexcc/sailcceqrange.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..2dd665fb --- /dev/null +++ b/cheri/sail_latexcc/sailccfastRepCheck.tex @@ -0,0 +1 @@ +val fastRepCheck : (CapStruct, bits(64)) -> bool diff --git a/cheri/sail_latexcc/sailccfnCPtrCmpOpofnum.tex b/cheri/sail_latexcc/sailccfnCPtrCmpOpofnum.tex new file mode 100644 index 00000000..6ab563f3 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnCPtrCmpOpofnum.tex @@ -0,0 +1,10 @@ +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 new file mode 100644 index 00000000..edfe64e3 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnClearRegSetofnum.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..dbbc5b49 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnHighestSetBit.tex @@ -0,0 +1,5 @@ +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 new file mode 100644 index 00000000..ee937856 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnMIPSread.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..5e81f335 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnMIPSwrite.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..3a6be173 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnatopcorrection.tex @@ -0,0 +1,7 @@ +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 new file mode 100644 index 00000000..1cb33076 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnbitstobool.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..a5eea578 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnbittobool.tex @@ -0,0 +1,4 @@ +function bit_to_bool b = match b { + bitone => true, + _ => false +} diff --git a/cheri/sail_latexcc/sailccfnbooltobits.tex b/cheri/sail_latexcc/sailccfnbooltobits.tex new file mode 100644 index 00000000..99075369 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnbooltobits.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..4af338b9 --- /dev/null +++ b/cheri/sail_latexcc/sailccfncapRegToCapStruct.tex @@ -0,0 +1,27 @@ +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 new file mode 100644 index 00000000..f6b02365 --- /dev/null +++ b/cheri/sail_latexcc/sailccfncapStructToCapReg.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..ea19467f --- /dev/null +++ b/cheri/sail_latexcc/sailccfncapStructToMemBits.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..08da637f --- /dev/null +++ b/cheri/sail_latexcc/sailccfncapStructToMemBitsonetwoeight.tex @@ -0,0 +1,12 @@ +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 new file mode 100644 index 00000000..1bb7a9e0 --- /dev/null +++ b/cheri/sail_latexcc/sailccfncastunitvec.tex @@ -0,0 +1,4 @@ +function cast_unit_vec b = match b { + bitzero => 0b0, + _ => 0b1 +} diff --git a/cheri/sail_latexcc/sailccfncomputeE.tex b/cheri/sail_latexcc/sailccfncomputeE.tex new file mode 100644 index 00000000..ef4cb71b --- /dev/null +++ b/cheri/sail_latexcc/sailccfncomputeE.tex @@ -0,0 +1,7 @@ +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 new file mode 100644 index 00000000..3e4d2111 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnfastRepCheck.tex @@ -0,0 +1,23 @@ +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 new file mode 100644 index 00000000..51677965 --- /dev/null +++ b/cheri/sail_latexcc/sailccfngetCapBase.tex @@ -0,0 +1,10 @@ +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 new file mode 100644 index 00000000..9f5d5757 --- /dev/null +++ b/cheri/sail_latexcc/sailccfngetCapCursor.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..0b86b980 --- /dev/null +++ b/cheri/sail_latexcc/sailccfngetCapHardPerms.tex @@ -0,0 +1,12 @@ +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 new file mode 100644 index 00000000..e9ce6566 --- /dev/null +++ b/cheri/sail_latexcc/sailccfngetCapLength.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..8bf83916 --- /dev/null +++ b/cheri/sail_latexcc/sailccfngetCapOffset.tex @@ -0,0 +1,3 @@ +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 new file mode 100644 index 00000000..9701e163 --- /dev/null +++ b/cheri/sail_latexcc/sailccfngetCapPerms.tex @@ -0,0 +1,5 @@ +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 new file mode 100644 index 00000000..1be5af24 --- /dev/null +++ b/cheri/sail_latexcc/sailccfngetCapTop.tex @@ -0,0 +1,11 @@ +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 new file mode 100644 index 00000000..59d3237e --- /dev/null +++ b/cheri/sail_latexcc/sailccfnincCapOffset.tex @@ -0,0 +1,5 @@ +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 new file mode 100644 index 00000000..31bb2bec --- /dev/null +++ b/cheri/sail_latexcc/sailccfninttocap.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..877cc2a0 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnisnone.tex @@ -0,0 +1,4 @@ +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 new file mode 100644 index 00000000..f1f5f655 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnissome.tex @@ -0,0 +1,4 @@ +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 new file mode 100644 index 00000000..e62ea529 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnmask.tex @@ -0,0 +1 @@ +function mask bs = bs['n - 1 .. 0] diff --git a/cheri/sail_latexcc/sailccfnmemBitsToCapBits.tex b/cheri/sail_latexcc/sailccfnmemBitsToCapBits.tex new file mode 100644 index 00000000..198cf984 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnmemBitsToCapBits.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..723571e9 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnmemBitsToCapBitsonetwoeight.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..80945b61 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnmipssignextend.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..6c9914d9 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnmipszzeroextend.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..1605ed05 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnneqanything.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..e9a9f93f --- /dev/null +++ b/cheri/sail_latexcc/sailccfnneqatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..65007b8e --- /dev/null +++ b/cheri/sail_latexcc/sailccfnneqbool.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..952a7735 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnneqint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..43f49e9e --- /dev/null +++ b/cheri/sail_latexcc/sailccfnneqrange.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..c446df08 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnneqvec.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..4d20546b --- /dev/null +++ b/cheri/sail_latexcc/sailccfnnumofCPtrCmpOp.tex @@ -0,0 +1,10 @@ +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 new file mode 100644 index 00000000..3dd58b89 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnnumofClearRegSet.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..e58040d7 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnones.tex @@ -0,0 +1 @@ +function #\hyperref[zones]{ones}#() = #\hyperref[zreplicatezybits]{replicate\_bits}# (0b1,'n) diff --git a/cheri/sail_latexcc/sailccfnroundUp.tex b/cheri/sail_latexcc/sailccfnroundUp.tex new file mode 100644 index 00000000..1ed68a59 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnroundUp.tex @@ -0,0 +1,5 @@ +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 new file mode 100644 index 00000000..37ede658 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnsailmask.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..55c55014 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnsealCap.tex @@ -0,0 +1,5 @@ +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 new file mode 100644 index 00000000..44808068 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnsetCapBounds.tex @@ -0,0 +1,13 @@ +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 new file mode 100644 index 00000000..f272f7d3 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnsetCapOffset.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..5af9e7f6 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnsetCapPerms.tex @@ -0,0 +1,16 @@ +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 new file mode 100644 index 00000000..d1df5e83 --- /dev/null +++ b/cheri/sail_latexcc/sailccfntobits.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..62e5a2e4 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIsznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..3f946820 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozIuznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..57ecf181 --- /dev/null +++ b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJsznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..6df36c6f --- /dev/null +++ b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozKzJuznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..2c372e1b --- /dev/null +++ b/cheri/sail_latexcc/sailccfnzeightoperatorzzerozQzQznine.tex @@ -0,0 +1 @@ +function operator ^^ (bs, n) = #\hyperref[zreplicatezybits]{replicate\_bits}# (bs, n) diff --git a/cheri/sail_latexcc/sailccfnzzeros.tex b/cheri/sail_latexcc/sailccfnzzeros.tex new file mode 100644 index 00000000..38d463fb --- /dev/null +++ b/cheri/sail_latexcc/sailccfnzzeros.tex @@ -0,0 +1 @@ +function #\hyperref[zzzeros]{zeros}#() = #\hyperref[zreplicatezybits]{replicate\_bits}# (0b0,'n) diff --git a/cheri/sail_latexcc/sailccgetCapBase.tex b/cheri/sail_latexcc/sailccgetCapBase.tex new file mode 100644 index 00000000..c7044d1d --- /dev/null +++ b/cheri/sail_latexcc/sailccgetCapBase.tex @@ -0,0 +1 @@ +val getCapBase : CapStruct -> uint64 diff --git a/cheri/sail_latexcc/sailccgetCapCursor.tex b/cheri/sail_latexcc/sailccgetCapCursor.tex new file mode 100644 index 00000000..fd5d72d8 --- /dev/null +++ b/cheri/sail_latexcc/sailccgetCapCursor.tex @@ -0,0 +1 @@ +val getCapCursor : CapStruct -> uint64 diff --git a/cheri/sail_latexcc/sailccgetCapHardPerms.tex b/cheri/sail_latexcc/sailccgetCapHardPerms.tex new file mode 100644 index 00000000..3b65a7c0 --- /dev/null +++ b/cheri/sail_latexcc/sailccgetCapHardPerms.tex @@ -0,0 +1 @@ +val getCapHardPerms : CapStruct -> bits(11) diff --git a/cheri/sail_latexcc/sailccgetCapLength.tex b/cheri/sail_latexcc/sailccgetCapLength.tex new file mode 100644 index 00000000..be84bfb5 --- /dev/null +++ b/cheri/sail_latexcc/sailccgetCapLength.tex @@ -0,0 +1 @@ +val getCapLength : CapStruct -> CapLen effect {escape} diff --git a/cheri/sail_latexcc/sailccgetCapOffset.tex b/cheri/sail_latexcc/sailccgetCapOffset.tex new file mode 100644 index 00000000..668c3df1 --- /dev/null +++ b/cheri/sail_latexcc/sailccgetCapOffset.tex @@ -0,0 +1 @@ +val getCapOffset : CapStruct -> uint64 diff --git a/cheri/sail_latexcc/sailccgetCapPerms.tex b/cheri/sail_latexcc/sailccgetCapPerms.tex new file mode 100644 index 00000000..b2dabf89 --- /dev/null +++ b/cheri/sail_latexcc/sailccgetCapPerms.tex @@ -0,0 +1 @@ +val getCapPerms : CapStruct -> bits(31) diff --git a/cheri/sail_latexcc/sailccgetCapTop.tex b/cheri/sail_latexcc/sailccgetCapTop.tex new file mode 100644 index 00000000..ff0e5f95 --- /dev/null +++ b/cheri/sail_latexcc/sailccgetCapTop.tex @@ -0,0 +1 @@ +val getCapTop : CapStruct -> CapLen diff --git a/cheri/sail_latexcc/sailccgetsliceint.tex b/cheri/sail_latexcc/sailccgetsliceint.tex new file mode 100644 index 00000000..2b30d096 --- /dev/null +++ b/cheri/sail_latexcc/sailccgetsliceint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..74cfd526 --- /dev/null +++ b/cheri/sail_latexcc/sailccgettimens.tex @@ -0,0 +1 @@ +val "get_time_ns" : unit -> int diff --git a/cheri/sail_latexcc/sailccgtatom.tex b/cheri/sail_latexcc/sailccgtatom.tex new file mode 100644 index 00000000..b2147a8f --- /dev/null +++ b/cheri/sail_latexcc/sailccgtatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..3c520181 --- /dev/null +++ b/cheri/sail_latexcc/sailccgtatomrange.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..fb3b66b2 --- /dev/null +++ b/cheri/sail_latexcc/sailccgteqatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..7aaf633f --- /dev/null +++ b/cheri/sail_latexcc/sailccgteqatomrange.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..77271d1f --- /dev/null +++ b/cheri/sail_latexcc/sailccgteqint.tex @@ -0,0 +1 @@ +val gteq_int = {coq: "Z.geb", _:"gteq"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailccgteqrangeatom.tex b/cheri/sail_latexcc/sailccgteqrangeatom.tex new file mode 100644 index 00000000..fda25265 --- /dev/null +++ b/cheri/sail_latexcc/sailccgteqrangeatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..2d953eec --- /dev/null +++ b/cheri/sail_latexcc/sailccgtint.tex @@ -0,0 +1 @@ +val gt_int = {coq: "Z.gtb", _:"gt"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailccgtrangeatom.tex b/cheri/sail_latexcc/sailccgtrangeatom.tex new file mode 100644 index 00000000..b8635909 --- /dev/null +++ b/cheri/sail_latexcc/sailccgtrangeatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..21c08cb5 --- /dev/null +++ b/cheri/sail_latexcc/sailccincCapOffset.tex @@ -0,0 +1 @@ +val incCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct) diff --git a/cheri/sail_latexcc/sailccintpower.tex b/cheri/sail_latexcc/sailccintpower.tex new file mode 100644 index 00000000..0aa13188 --- /dev/null +++ b/cheri/sail_latexcc/sailccintpower.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..0f4cd328 --- /dev/null +++ b/cheri/sail_latexcc/sailccinttocap.tex @@ -0,0 +1 @@ +val int_to_cap : bits(64) -> CapStruct diff --git a/cheri/sail_latexcc/sailccisnone.tex b/cheri/sail_latexcc/sailccisnone.tex new file mode 100644 index 00000000..76688d37 --- /dev/null +++ b/cheri/sail_latexcc/sailccisnone.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..071ac6b6 --- /dev/null +++ b/cheri/sail_latexcc/sailccissome.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..248c8507 --- /dev/null +++ b/cheri/sail_latexcc/sailcclength.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..5cca54df --- /dev/null +++ b/cheri/sail_latexcc/sailccltatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..19d3375d --- /dev/null +++ b/cheri/sail_latexcc/sailccltatomrange.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..26e27e2d --- /dev/null +++ b/cheri/sail_latexcc/sailcclteqatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..6e951cf7 --- /dev/null +++ b/cheri/sail_latexcc/sailcclteqatomrange.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..555176be --- /dev/null +++ b/cheri/sail_latexcc/sailcclteqint.tex @@ -0,0 +1 @@ +val lteq_int = {coq: "Z.leb", _:"lteq"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailcclteqrangeatom.tex b/cheri/sail_latexcc/sailcclteqrangeatom.tex new file mode 100644 index 00000000..f8fcd32d --- /dev/null +++ b/cheri/sail_latexcc/sailcclteqrangeatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..40bd4e85 --- /dev/null +++ b/cheri/sail_latexcc/sailccltint.tex @@ -0,0 +1 @@ +val lt_int = {coq: "Z.ltb", _:"lt"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailccltrangeatom.tex b/cheri/sail_latexcc/sailccltrangeatom.tex new file mode 100644 index 00000000..d8495496 --- /dev/null +++ b/cheri/sail_latexcc/sailccltrangeatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..35d052db --- /dev/null +++ b/cheri/sail_latexcc/sailccmask.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..1ceed42c --- /dev/null +++ b/cheri/sail_latexcc/sailccmax.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..6cbdfa7f --- /dev/null +++ b/cheri/sail_latexcc/sailccmaxatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..c537babb --- /dev/null +++ b/cheri/sail_latexcc/sailccmaxint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..1b62334a --- /dev/null +++ b/cheri/sail_latexcc/sailccmaxnat.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..a5c86272 --- /dev/null +++ b/cheri/sail_latexcc/sailccmemBitsToCapBits.tex @@ -0,0 +1 @@ +val memBitsToCapBits : (bool, bits(128)) -> bits(129) diff --git a/cheri/sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex b/cheri/sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex new file mode 100644 index 00000000..4eb94a3d --- /dev/null +++ b/cheri/sail_latexcc/sailccmemBitsToCapBitsonetwoeight.tex @@ -0,0 +1 @@ +val memBitsToCapBits128 : (bool, bits(128)) -> CapReg diff --git a/cheri/sail_latexcc/sailccmin.tex b/cheri/sail_latexcc/sailccmin.tex new file mode 100644 index 00000000..94097198 --- /dev/null +++ b/cheri/sail_latexcc/sailccmin.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..acfea384 --- /dev/null +++ b/cheri/sail_latexcc/sailccminatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..3d633d08 --- /dev/null +++ b/cheri/sail_latexcc/sailccminint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..85409bd8 --- /dev/null +++ b/cheri/sail_latexcc/sailccminnat.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..e613567d --- /dev/null +++ b/cheri/sail_latexcc/sailccmipssignextend.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..adbb4188 --- /dev/null +++ b/cheri/sail_latexcc/sailccmipszzeroextend.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..ab70dd7a --- /dev/null +++ b/cheri/sail_latexcc/sailccmod.tex @@ -0,0 +1,7 @@ +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 new file mode 100644 index 00000000..bd5677aa --- /dev/null +++ b/cheri/sail_latexcc/sailccmodint.tex @@ -0,0 +1,7 @@ +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 new file mode 100644 index 00000000..ca23a339 --- /dev/null +++ b/cheri/sail_latexcc/sailccmodulus.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..bbac3e2f --- /dev/null +++ b/cheri/sail_latexcc/sailccmultatom.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..08698e6f --- /dev/null +++ b/cheri/sail_latexcc/sailccmultint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..ce000062 --- /dev/null +++ b/cheri/sail_latexcc/sailccnegate.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..d1361e63 --- /dev/null +++ b/cheri/sail_latexcc/sailccnegateatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..52375787 --- /dev/null +++ b/cheri/sail_latexcc/sailccnegateint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..7a4ad386 --- /dev/null +++ b/cheri/sail_latexcc/sailccnegaterange.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..a898649e --- /dev/null +++ b/cheri/sail_latexcc/sailccneqanything.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..be777013 --- /dev/null +++ b/cheri/sail_latexcc/sailccneqatom.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..0d80dc17 --- /dev/null +++ b/cheri/sail_latexcc/sailccneqbool.tex @@ -0,0 +1 @@ +val neq_bool : (bool, bool) -> bool diff --git a/cheri/sail_latexcc/sailccneqint.tex b/cheri/sail_latexcc/sailccneqint.tex new file mode 100644 index 00000000..b233ca6b --- /dev/null +++ b/cheri/sail_latexcc/sailccneqint.tex @@ -0,0 +1 @@ +val neq_int = {lem: "neq"} : (int, int) -> bool diff --git a/cheri/sail_latexcc/sailccneqrange.tex b/cheri/sail_latexcc/sailccneqrange.tex new file mode 100644 index 00000000..d2d8fb0c --- /dev/null +++ b/cheri/sail_latexcc/sailccneqrange.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..f655b3d8 --- /dev/null +++ b/cheri/sail_latexcc/sailccneqvec.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..515b3ef9 --- /dev/null +++ b/cheri/sail_latexcc/sailccnot.tex @@ -0,0 +1 @@ +val not = {coq:"negb", _:"not"} : bool -> bool diff --git a/cheri/sail_latexcc/sailccnotbool.tex b/cheri/sail_latexcc/sailccnotbool.tex new file mode 100644 index 00000000..7630f6c2 --- /dev/null +++ b/cheri/sail_latexcc/sailccnotbool.tex @@ -0,0 +1 @@ +val not_bool = {coq: "negb", _: "not"} : bool -> bool diff --git a/cheri/sail_latexcc/sailccnotvec.tex b/cheri/sail_latexcc/sailccnotvec.tex new file mode 100644 index 00000000..a560a544 --- /dev/null +++ b/cheri/sail_latexcc/sailccnotvec.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..40f1bfa9 --- /dev/null +++ b/cheri/sail_latexcc/sailccnumofCPtrCmpOp.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..14ea7bea --- /dev/null +++ b/cheri/sail_latexcc/sailccnumofClearRegSet.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..94fd805f --- /dev/null +++ b/cheri/sail_latexcc/sailccones.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..55db5ffa --- /dev/null +++ b/cheri/sail_latexcc/sailccorbits.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..4b6bfa15 --- /dev/null +++ b/cheri/sail_latexcc/sailccorbool.tex @@ -0,0 +1 @@ +val or_bool = {coq: "orb", _: "or_bool"} : (bool, bool) -> bool diff --git a/cheri/sail_latexcc/sailccplainvectoraccess.tex b/cheri/sail_latexcc/sailccplainvectoraccess.tex new file mode 100644 index 00000000..94824f77 --- /dev/null +++ b/cheri/sail_latexcc/sailccplainvectoraccess.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..6880d9bd --- /dev/null +++ b/cheri/sail_latexcc/sailccplainvectorupdate.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..41da946e --- /dev/null +++ b/cheri/sail_latexcc/sailccpowtwo.tex @@ -0,0 +1 @@ +val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) diff --git a/cheri/sail_latexcc/sailccprerrbits.tex b/cheri/sail_latexcc/sailccprerrbits.tex new file mode 100644 index 00000000..7d926384 --- /dev/null +++ b/cheri/sail_latexcc/sailccprerrbits.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..ad4a94a0 --- /dev/null +++ b/cheri/sail_latexcc/sailccprerrendline.tex @@ -0,0 +1 @@ +val "prerr_endline" : string -> unit diff --git a/cheri/sail_latexcc/sailccprerrint.tex b/cheri/sail_latexcc/sailccprerrint.tex new file mode 100644 index 00000000..ce7a7d61 --- /dev/null +++ b/cheri/sail_latexcc/sailccprerrint.tex @@ -0,0 +1 @@ +val "prerr_int" : (string, int) -> unit diff --git a/cheri/sail_latexcc/sailccprerrstring.tex b/cheri/sail_latexcc/sailccprerrstring.tex new file mode 100644 index 00000000..7b849da2 --- /dev/null +++ b/cheri/sail_latexcc/sailccprerrstring.tex @@ -0,0 +1 @@ +val "prerr_string" : string -> unit diff --git a/cheri/sail_latexcc/sailccprint.tex b/cheri/sail_latexcc/sailccprint.tex new file mode 100644 index 00000000..50a64219 --- /dev/null +++ b/cheri/sail_latexcc/sailccprint.tex @@ -0,0 +1 @@ +val print = "print_endline" : string -> unit diff --git a/cheri/sail_latexcc/sailccprintbits.tex b/cheri/sail_latexcc/sailccprintbits.tex new file mode 100644 index 00000000..8783a59a --- /dev/null +++ b/cheri/sail_latexcc/sailccprintbits.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..ddf33afc --- /dev/null +++ b/cheri/sail_latexcc/sailccprintint.tex @@ -0,0 +1 @@ +val "print_int" : (string, int) -> unit diff --git a/cheri/sail_latexcc/sailccputchar.tex b/cheri/sail_latexcc/sailccputchar.tex new file mode 100644 index 00000000..a123c709 --- /dev/null +++ b/cheri/sail_latexcc/sailccputchar.tex @@ -0,0 +1 @@ +val putchar = {c:"sail_putchar", _:"putchar"} : int -> unit diff --git a/cheri/sail_latexcc/sailccquotient.tex b/cheri/sail_latexcc/sailccquotient.tex new file mode 100644 index 00000000..7dba5359 --- /dev/null +++ b/cheri/sail_latexcc/sailccquotient.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..14db4ae0 --- /dev/null +++ b/cheri/sail_latexcc/sailccquotientnat.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..9523cfcc --- /dev/null +++ b/cheri/sail_latexcc/sailccquotroundzzero.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..7f1dc7e8 --- /dev/null +++ b/cheri/sail_latexcc/sailccregderef.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..9d8113ba --- /dev/null +++ b/cheri/sail_latexcc/sailccremroundzzero.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..cd7a97d7 --- /dev/null +++ b/cheri/sail_latexcc/sailccreplicatebits.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..b7e31074 --- /dev/null +++ b/cheri/sail_latexcc/sailccroundUp.tex @@ -0,0 +1 @@ +val roundUp : range(0, 45) -> range(0, 48) diff --git a/cheri/sail_latexcc/sailccsailccnegatev.tex b/cheri/sail_latexcc/sailccsailccnegatev.tex new file mode 100644 index 00000000..4f7aea58 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailccnegatev.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..f5de92ca --- /dev/null +++ b/cheri/sail_latexcc/sailccsailccregderefv.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..0f72fdc9 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailccsailccsailcczeightoperatorzzerozJzJzninevvv.tex @@ -0,0 +1 @@ +overload (operator ==) = {eq_bit2}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex new file mode 100644 index 00000000..eacd556c --- /dev/null +++ b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozBzninevv.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..73c40722 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozFzninevv.tex @@ -0,0 +1 @@ +overload (operator /) = {div}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex new file mode 100644 index 00000000..47b1d0f6 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozJzJzninevv.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..552e0c24 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailccsailcczeightoperatorzzerozfivezninevv.tex @@ -0,0 +1 @@ +overload (operator %) = {mod}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex new file mode 100644 index 00000000..afe7a721 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozAzninev.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..ddc56bfd --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozBzninev.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..5d12fdf1 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozDzninev.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..38e9124b --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozFzninev.tex @@ -0,0 +1 @@ +overload (operator /) = {div_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex new file mode 100644 index 00000000..1314a962 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozJzJzninev.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..05769645 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozQzninev.tex @@ -0,0 +1 @@ +overload (operator ^) = {sail_mask}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex new file mode 100644 index 00000000..1ebacbc4 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozUzninev.tex @@ -0,0 +1 @@ +overload (operator |) = {or_bool}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex new file mode 100644 index 00000000..14fa73b8 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozfivezninev.tex @@ -0,0 +1 @@ +overload (operator %) = {mod_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex new file mode 100644 index 00000000..527cf596 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozonezJzninev.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..be6f29ef --- /dev/null +++ b/cheri/sail_latexcc/sailccsailcczeightoperatorzzerozsixzninev.tex @@ -0,0 +1 @@ +overload (operator &) = {and_bool}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailccsailmask.tex b/cheri/sail_latexcc/sailccsailmask.tex new file mode 100644 index 00000000..45862747 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailmask.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..dfaa5c86 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailsignextend.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..53f6fff9 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailzzeroextend.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..9c60aa12 --- /dev/null +++ b/cheri/sail_latexcc/sailccsailzzeros.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..891ae279 --- /dev/null +++ b/cheri/sail_latexcc/sailccsealCap.tex @@ -0,0 +1 @@ +val sealCap : (CapStruct, bits(24)) -> (bool, CapStruct) diff --git a/cheri/sail_latexcc/sailccsetCapBounds.tex b/cheri/sail_latexcc/sailccsetCapBounds.tex new file mode 100644 index 00000000..94fbecaf --- /dev/null +++ b/cheri/sail_latexcc/sailccsetCapBounds.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..fef324f7 --- /dev/null +++ b/cheri/sail_latexcc/sailccsetCapOffset.tex @@ -0,0 +1 @@ +val setCapOffset : (CapStruct, bits(64)) -> (bool, CapStruct) diff --git a/cheri/sail_latexcc/sailccsetCapPerms.tex b/cheri/sail_latexcc/sailccsetCapPerms.tex new file mode 100644 index 00000000..617f19fb --- /dev/null +++ b/cheri/sail_latexcc/sailccsetCapPerms.tex @@ -0,0 +1 @@ +val setCapPerms : (CapStruct, bits(31)) -> CapStruct diff --git a/cheri/sail_latexcc/sailccsetslicebits.tex b/cheri/sail_latexcc/sailccsetslicebits.tex new file mode 100644 index 00000000..8a81bff5 --- /dev/null +++ b/cheri/sail_latexcc/sailccsetslicebits.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..413bf721 --- /dev/null +++ b/cheri/sail_latexcc/sailccsetsliceint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..cdb2eb6a --- /dev/null +++ b/cheri/sail_latexcc/sailccshiftbitsleft.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..dbc72b11 --- /dev/null +++ b/cheri/sail_latexcc/sailccshiftbitsright.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..b2c54c27 --- /dev/null +++ b/cheri/sail_latexcc/sailccshiftl.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..f282dcbe --- /dev/null +++ b/cheri/sail_latexcc/sailccshiftr.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..8ffbcf6c --- /dev/null +++ b/cheri/sail_latexcc/sailccshlint.tex @@ -0,0 +1 @@ +val shl_int = "shl_int" : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccshrint.tex b/cheri/sail_latexcc/sailccshrint.tex new file mode 100644 index 00000000..087c17bb --- /dev/null +++ b/cheri/sail_latexcc/sailccshrint.tex @@ -0,0 +1 @@ +val shr_int = "shr_int" : (int, int) -> int diff --git a/cheri/sail_latexcc/sailccsigned.tex b/cheri/sail_latexcc/sailccsigned.tex new file mode 100644 index 00000000..dcdc3049 --- /dev/null +++ b/cheri/sail_latexcc/sailccsigned.tex @@ -0,0 +1,4 @@ +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 new file mode 100644 index 00000000..03f56369 --- /dev/null +++ b/cheri/sail_latexcc/sailccsignextend.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..b9bb5a70 --- /dev/null +++ b/cheri/sail_latexcc/sailccslice.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..05edaa20 --- /dev/null +++ b/cheri/sail_latexcc/sailccstringofint.tex @@ -0,0 +1 @@ +val string_of_int = "string_of_int" : int -> string diff --git a/cheri/sail_latexcc/sailccsubatom.tex b/cheri/sail_latexcc/sailccsubatom.tex new file mode 100644 index 00000000..437e2d4c --- /dev/null +++ b/cheri/sail_latexcc/sailccsubatom.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..11fdf922 --- /dev/null +++ b/cheri/sail_latexcc/sailccsubint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..2aad56b6 --- /dev/null +++ b/cheri/sail_latexcc/sailccsubrange.tex @@ -0,0 +1,2 @@ +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 new file mode 100644 index 00000000..b92f07a4 --- /dev/null +++ b/cheri/sail_latexcc/sailccsubvec.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..70bf667e --- /dev/null +++ b/cheri/sail_latexcc/sailccsubvecint.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..9dd3c655 --- /dev/null +++ b/cheri/sail_latexcc/sailcctobits.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..5f7760f3 --- /dev/null +++ b/cheri/sail_latexcc/sailcctruncate.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..a0d52c8f --- /dev/null +++ b/cheri/sail_latexcc/sailccuintsixfour.tex @@ -0,0 +1 @@ +type uint64 = range(0, (2 ^ 64) - 1) diff --git a/cheri/sail_latexcc/sailccunsigned.tex b/cheri/sail_latexcc/sailccunsigned.tex new file mode 100644 index 00000000..47867039 --- /dev/null +++ b/cheri/sail_latexcc/sailccunsigned.tex @@ -0,0 +1,7 @@ +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 new file mode 100644 index 00000000..a8e8074f --- /dev/null +++ b/cheri/sail_latexcc/sailccvectoraccess.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..f41d5bfa --- /dev/null +++ b/cheri/sail_latexcc/sailccvectorlength.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..c069c7b6 --- /dev/null +++ b/cheri/sail_latexcc/sailccvectorsubrange.tex @@ -0,0 +1,7 @@ +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 new file mode 100644 index 00000000..1ec4aaef --- /dev/null +++ b/cheri/sail_latexcc/sailccvectorupdate.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..6ff4f9f6 --- /dev/null +++ b/cheri/sail_latexcc/sailccvectorupdatesubrange.tex @@ -0,0 +1,6 @@ +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 new file mode 100644 index 00000000..b3aa7372 --- /dev/null +++ b/cheri/sail_latexcc/sailccxorvec.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..a29ec93f --- /dev/null +++ b/cheri/sail_latexcc/sailcczW.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..0b0a46e2 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozAsznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..5b762ba7 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozAuznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..2d188f63 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozAznine.tex @@ -0,0 +1 @@ +overload (operator *) = {mult_int}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozBznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozBznine.tex new file mode 100644 index 00000000..432e85e5 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozBznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..d671e6b0 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozDznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..3c2e441c --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozFznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..9b4ebe19 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozIsznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..5b54235e --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozIuznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..51ff2b6c --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozIzIznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..d23f28dd --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozIzJznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..8e5e3fe9 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozIznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..57ea823c --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozJzJznine.tex @@ -0,0 +1 @@ +overload (operator ==) = {eq_anything}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex new file mode 100644 index 00000000..032e8600 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJsznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..eaa72e60 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJuznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..5733b740 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzJznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..0f0793a6 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKsznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..b129e9d2 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozKzKznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..a8da7e48 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozKznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..185f501e --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozQzQznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..106b6064 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozQznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..4de737e0 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozUznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..8d6b54c3 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozfiveznine.tex @@ -0,0 +1 @@ +overload (operator %) = {modulus}
\ No newline at end of file diff --git a/cheri/sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex b/cheri/sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex new file mode 100644 index 00000000..22052668 --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozonezJznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..248fb15e --- /dev/null +++ b/cheri/sail_latexcc/sailcczeightoperatorzzerozsixznine.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..0f754d44 --- /dev/null +++ b/cheri/sail_latexcc/sailcczzeroextend.tex @@ -0,0 +1 @@ +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 new file mode 100644 index 00000000..1c251eda --- /dev/null +++ b/cheri/sail_latexcc/sailcczzeros.tex @@ -0,0 +1 @@ +val zeros : forall 'n, 'n >= 0 . unit -> #\hyperref[zbits]{bits}#('n) |