Initial commit

Co-authored-by: François Bojarski <[email protected]>
Co-authored-by: Lorenzo Gentile <[email protected]>
Co-authored-by: David Pearce <[email protected]>
Co-authored-by: ewile <[email protected]>
Co-authored-by: Franklin Delehelle <[email protected]>
Co-authored-by: bkolad <[email protected]>

.exrc

@@ -0,0 +1,198 @@
+let s:cpo_save=&cpo
+set cpo&vim
+cnoremap <silent> <C-R> <Cmd>lua require("which-key").show("\18", {mode = "c", auto = true})
+inoremap <silent> <C-G>Þ <Nop>
+inoremap <silent> <C-G> <Cmd>lua require("which-key").show("\7", {mode = "i", auto = true})
+inoremap <silent> <C-R> <Cmd>lua require("which-key").show("\18", {mode = "i", auto = true})
+inoremap <C-G>S <Plug>(nvim-surround-insert-line)
+inoremap <C-G>s <Plug>(nvim-surround-insert)
+inoremap <C-J> <Down>
+inoremap <C-H> <Left>
+inoremap <C-B> ^i
+inoremap <C-K> <Up>
+inoremap <C-L> <Right>
+inoremap <C-W> u
+inoremap <C-U> u
+nnoremap  <Cmd> %y+ 
+nnoremap  h
+nnoremap <NL> j
+nnoremap  k
+nnoremap  l
+nnoremap  <Cmd> NvimTreeToggle 
+nnoremap  <Cmd> w 
+nnoremap <silent> Þ <Nop>
+nnoremap <silent>  <Cmd>lua require("which-key").show("\23", {mode = "n", auto = true})
+tnoremap  
+nnoremap  :noh 
+nnoremap <silent>  Þ <Nop>
+nnoremap <silent>   <Cmd>lua require("which-key").show(" ", {mode = "n", auto = true})
+xnoremap <silent>  Þ <Nop>
+xnoremap <silent>   <Cmd>lua require("which-key").show(" ", {mode = "v", auto = true})
+nnoremap <silent>  pÞ <Nop>
+nnoremap <silent>  mÞ <Nop>
+nnoremap <silent>  rÞ <Nop>
+nnoremap <silent>  wÞ <Nop>
+nnoremap <silent>  gÞ <Nop>
+nnoremap <silent>  cÞ <Nop>
+nnoremap <silent>  fÞ <Nop>
+nnoremap <silent>  tÞ <Nop>
+vnoremap  / <Cmd>lua require('Comment.api').toggle.linewise(vim.fn.visualmode())
+nnoremap  fz <Cmd> Telescope current_buffer_fuzzy_find 
+nnoremap  th <Cmd> Telescope themes 
+nnoremap  fb <Cmd> Telescope buffers 
+nnoremap  fo <Cmd> Telescope oldfiles 
+nnoremap  fw <Cmd> Telescope live_grep 
+nnoremap  cm <Cmd> Telescope git_commits 
+nnoremap  fa <Cmd> Telescope find_files follow=true no_ignore=true hidden=true 
+nnoremap  gt <Cmd> Telescope git_status 
+nnoremap  ff <Cmd> Telescope find_files 
+nnoremap  ma <Cmd> Telescope marks 
+nnoremap  pt <Cmd> Telescope terms 
+nnoremap  fh <Cmd> Telescope help_tags 
+nnoremap  e <Cmd> NvimTreeFocus 
+nnoremap  b <Cmd> enew 
+nnoremap  n <Cmd> set nu! 
+nnoremap  ch <Cmd> NvCheatsheet 
+nnoremap  rn <Cmd> set rnu! 
+nnoremap <silent> !aÞ <Nop>
+nnoremap <silent> !iÞ <Nop>
+nnoremap <silent> !Þ <Nop>
+nnoremap <silent> ! <Cmd>lua require("which-key").show("!", {mode = "n", auto = true})
+xnoremap <silent> " <Cmd>lua require("which-key").show("\"", {mode = "v", auto = true})
+nnoremap <silent> " <Cmd>lua require("which-key").show("\"", {mode = "n", auto = true})
+xnoremap # y?\V"
+nnoremap & :&&
+nnoremap <silent> ' <Cmd>lua require("which-key").show("'", {mode = "n", auto = true})
+xnoremap * y/\V"
+nnoremap <silent> <aÞ <Nop>
+nnoremap <silent> <iÞ <Nop>
+nnoremap <silent> <Þ <Nop>
+nnoremap <silent> < <Cmd>lua require("which-key").show("<", {mode = "n", auto = true})
+nnoremap <silent> >aÞ <Nop>
+nnoremap <silent> >iÞ <Nop>
+nnoremap <silent> >Þ <Nop>
+nnoremap <silent> > <Cmd>lua require("which-key").show(">", {mode = "n", auto = true})
+nnoremap <silent> @Þ <Nop>
+nnoremap <silent> @ <Cmd>lua require("which-key").show("@", {mode = "n", auto = true})
+xnoremap S <Plug>(nvim-surround-visual)
+nnoremap Y y$
+nnoremap <silent> [Þ <Nop>
+nnoremap <silent> [ <Cmd>lua require("which-key").show("[", {mode = "n", auto = true})
+nnoremap <silent> ]Þ <Nop>
+nnoremap <silent> ] <Cmd>lua require("which-key").show("]", {mode = "n", auto = true})
+nnoremap <silent> ` <Cmd>lua require("which-key").show("`", {mode = "n", auto = true})
+nnoremap <silent> ciÞ <Nop>
+nnoremap <silent> ci <Cmd>lua require("which-key").show("ci", {mode = "n", auto = true})
+nnoremap <silent> cÞ <Nop>
+nnoremap <silent> c <Cmd>lua require("which-key").show("c", {mode = "n", auto = true})
+nnoremap <silent> caÞ <Nop>
+nnoremap cS <Plug>(nvim-surround-change-line)
+nnoremap cs <Plug>(nvim-surround-change)
+nnoremap <silent> dÞ <Nop>
+nnoremap <silent> d <Cmd>lua require("which-key").show("d", {mode = "n", auto = true})
+nnoremap <silent> daÞ <Nop>
+nnoremap <silent> diÞ <Nop>
+nnoremap ds <Plug>(nvim-surround-delete)
+xnoremap <silent> gÞ <Nop>
+xnoremap <silent> g <Cmd>lua require("which-key").show("g", {mode = "v", auto = true})
+nnoremap <silent> gUaÞ <Nop>
+nnoremap <silent> gUiÞ <Nop>
+nnoremap <silent> gUÞ <Nop>
+nnoremap <silent> gbÞ <Nop>
+nnoremap <silent> gcÞ <Nop>
+nnoremap <silent> g~aÞ <Nop>
+nnoremap <silent> g~iÞ <Nop>
+nnoremap <silent> g~Þ <Nop>
+nnoremap <silent> guaÞ <Nop>
+nnoremap <silent> guiÞ <Nop>
+nnoremap <silent> guÞ <Nop>
+nnoremap <silent> gÞ <Nop>
+nnoremap <silent> g <Cmd>lua require("which-key").show("g", {mode = "n", auto = true})
+xnoremap gS <Plug>(nvim-surround-visual-line)
+nnoremap <expr> j v:count || mode(1)[0:1] == "no" ? "j" : "gj"
+xnoremap <expr> j v:count || mode(1)[0:1] == "no" ? "j" : "gj"
+nnoremap <expr> k v:count || mode(1)[0:1] == "no" ? "k" : "gk"
+xnoremap <expr> k v:count || mode(1)[0:1] == "no" ? "k" : "gk"
+xnoremap <silent> p p:let @+=@0:let @"=@0
+nnoremap <silent> viÞ <Nop>
+nnoremap <silent> vi <Cmd>lua require("which-key").show("vi", {mode = "n", auto = true})
+nnoremap <silent> vÞ <Nop>
+nnoremap <silent> v <Cmd>lua require("which-key").show("v", {mode = "n", auto = true})
+nnoremap <silent> vaÞ <Nop>
+nnoremap <silent> yÞ <Nop>
+nnoremap <silent> y <Cmd>lua require("which-key").show("y", {mode = "n", auto = true})
+nnoremap <silent> yiÞ <Nop>
+nnoremap <silent> yi <Cmd>lua require("which-key").show("yi", {mode = "n", auto = true})
+nnoremap <silent> yaÞ <Nop>
+nnoremap ySS <Plug>(nvim-surround-normal-cur-line)
+nnoremap yS <Plug>(nvim-surround-normal-line)
+nnoremap yss <Plug>(nvim-surround-normal-cur)
+nnoremap ys <Plug>(nvim-surround-normal)
+nnoremap <silent> zfaÞ <Nop>
+nnoremap <silent> zfiÞ <Nop>
+nnoremap <silent> zfÞ <Nop>
+nnoremap <silent> zÞ <Nop>
+nnoremap <silent> z <Cmd>lua require("which-key").show("z", {mode = "n", auto = true})
+nnoremap <silent> <C-W>Þ <Nop>
+nnoremap <silent> <C-W> <Cmd>lua require("which-key").show("\23", {mode = "n", auto = true})
+xnoremap <silent> <Plug>(nvim-surround-visual-line) <Cmd>lua require'nvim-surround'.visual_surround({ line_mode = true })
+xnoremap <silent> <Plug>(nvim-surround-visual) <Cmd>lua require'nvim-surround'.visual_surround({ line_mode = false })
+nnoremap <C-N> <Cmd> NvimTreeToggle 
+tnoremap <C-X> 
+vnoremap <expr> <Up> v:count || mode(1)[0:1] == "no" ? "k" : "gk"
+vnoremap <expr> <Down> v:count || mode(1)[0:1] == "no" ? "j" : "gj"
+nnoremap <C-C> <Cmd> %y+ 
+nnoremap <C-S> <Cmd> w 
+nnoremap <C-K> k
+nnoremap <C-J> j
+nnoremap <expr> <Down> v:count || mode(1)[0:1] == "no" ? "j" : "gj"
+nnoremap <C-H> h
+nnoremap <expr> <Up> v:count || mode(1)[0:1] == "no" ? "k" : "gk"
+nnoremap <C-L> l
+inoremap  ^i
+inoremap <silent> Þ <Nop>
+inoremap <silent>  <Cmd>lua require("which-key").show("\7", {mode = "i", auto = true})
+inoremap S <Plug>(nvim-surround-insert-line)
+inoremap s <Plug>(nvim-surround-insert)
+inoremap  <Left>
+inoremap <NL> <Down>
+inoremap  <Up>
+inoremap  <Right>
+cnoremap <silent>  <Cmd>lua require("which-key").show("\18", {mode = "c", auto = true})
+inoremap <silent>  <Cmd>lua require("which-key").show("\18", {mode = "i", auto = true})
+inoremap  u
+inoremap  u
+inoremap kj 
+let &cpo=s:cpo_save
+unlet s:cpo_save
+set clipboard=unnamedplus
+set expandtab
+set fillchars=eob:\ 
+set helplang=en
+set ignorecase
+set indentkeys=0{,0},0),0],:,0#,!^F,o,O,e,[,(,{,),},],&,=^s*\\bibitem,=\\item
+set laststatus=3
+set noloadplugins
+set mouse=a
+set packpath=/usr/share/nvim/runtime
+set noruler
+set runtimepath=~/.config/nvim,~/.local/share/nvim/lazy/lazy.nvim,~/.local/share/nvim/lazy/base46,~/.local/share/nvim/lazy/nvterm,~/.local/share/nvim/lazy/which-key.nvim,~/.local/share/nvim/lazy/cmp-path,~/.local/share/nvim/lazy/cmp-buffer,~/.local/share/nvim/lazy/cmp-nvim-lsp,~/.local/share/nvim/lazy/cmp-nvim-lua,~/.local/share/nvim/lazy/cmp_luasnip,~/.local/share/nvim/lazy/nvim-autopairs,~/.local/share/nvim/lazy/friendly-snippets,~/.local/share/nvim/lazy/LuaSnip,~/.local/share/nvim/lazy/nvim-cmp,~/.local/share/nvim/lazy/nvim-lspconfig,~/.local/share/nvim/lazy/gitsigns.nvim,~/.local/share/nvim/lazy/nvim-colorizer.lua,~/.local/share/nvim/lazy/indent-blankline.nvim,~/.local/share/nvim/lazy/nvim-treesitter,~/.local/share/nvim/lazy/nvim-web-devicons,~/.local/share/nvim/lazy/nvim-tree.lua,~/.local/share/nvim/lazy/nvim-surround,~/.local/share/nvim/lazy/ui,/usr/share/nvim/runtime,~/.local/state/nvim/lazy/readme,~/.local/share/nvim/lazy/cmp-path/after,~/.local/share/nvim/lazy/cmp-buffer/after,~/.local/share/nvim/lazy/cmp-nvim-lsp/after,~/.local/share/nvim/lazy/cmp-nvim-lua/after,~/.local/share/nvim/lazy/cmp_luasnip/after
+set shiftwidth=2
+set shortmess=ifnITFstOolx
+set noshowmode
+set showtabline=2
+set smartcase
+set smartindent
+set softtabstop=2
+set splitbelow
+set splitright
+set statusline=%!v:lua.require('nvchad_ui.statusline.default').run()
+set tabline=%!v:lua.require('nvchad_ui.tabufline.modules').run()
+set tabstop=2
+set termguicolors
+set timeoutlen=400
+set undofile
+set updatetime=250
+set whichwrap=<>[]hl,b,s
+set window=37
+" vim: set ft=vim :

.github/workflows/compile.yml

@@ -0,0 +1,31 @@
+name: Build & Upload the Specification
+on:
+  push:
+    branches: [ main ]
+
+jobs:
+  archive-build-spec:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+      - name: Install JetBrainsMono # https://www.guyrutenberg.com/2020/01/29/install-jetbrains-mono-in-debian-ubuntu/
+        run: mkdir JetBrainsMono
+             && cd JetBrainsMono
+             && wget https://github.com/ryanoasis/nerd-fonts/releases/download/v3.2.1/JetBrainsMono.zip
+             && unzip JetBrainsMono.zip
+             && sudo mv JetBrainsMono*.ttf /usr/share/fonts/
+             && cd -
+      - name: Install fontawesome
+        run: sudo apt-get install fonts-font-awesome
+      - name: Install tectonic
+        run: curl --proto '=https' --tlsv1.2 -fsSL https://drop-sh.fullyjustified.net |sh
+      - name: Install lualatex
+        # run: sudo apt-get install texlive-latex-base && sudo apt install texlive-luatex && sudo apt-get install texlive-latex-extra
+        run: sudo apt install texlive-full
+      - name: Compile Specification
+        run: make ospec
+      - name: Upload the Specification
+        uses: actions/upload-artifact@v3
+        with:
+          name: specification.pdf
+          path: spec/_all_spec.pdf

.gitignore

@@ -0,0 +1,11 @@
+*.pdf
+*.fls
+*.aux
+*.log
+*.out
+*.toc
+*.synctex.gz
+*.bib
+*.xml
+*.fdb_latexmk
+*.blg

Makefile

@@ -0,0 +1,106 @@
+.PHONY: alu bin exp gas oob
+
+view-%: lua_build
+	cd $* && tectonic -X compile _all_$*.tex && evince _all_$*.pdf
+
+recompile-%: lua_build
+	cd $* && tectonic -X compile _all_$*.tex
+
+buildOnGithub-%: lua_build
+	cd $* && ../tectonic -X compile _all_$*.tex
+
+alu:          view-alu
+blake:        view-blake_data
+block_data:   view-block_data
+block_hash:   view-block_hash
+btc:          view-btc_data
+bin:          view-bin
+exp:          view-exp
+euc:          view-euc
+formal:       view-formal
+gas:          view-gas
+hash_data:    view-hash_data
+hash_info:    view-hash_info
+hub:          view-hub
+lex:          view-lex
+logd_data:    view-log_data
+logi_info:    view-log_info
+mmio:         view-mmio
+modexp:       view-modexp_data
+mmu:          view-mmu
+mxp:          view-mxp
+oob:          view-oob
+prc:   	      view-prc
+rlp_addr:     view-rlp_addr
+rlp_txn:      view-rlp_txn
+rlp_txnrcpt:  view-rlp_txnrcpt
+rom:          view-rom
+rom_lex:      view-rom_lex
+shf:          view-shf
+spec:         view-spec
+stp:          view-stp
+trm:          view-trm
+txn_data:     view-txn_data
+wcp:          view-wcp
+
+ralu:          recompile-alu
+rblake:        recompile-blake_data
+rblock_data:   recompile-block_data
+rblock_hash:   recompile-block_hash
+rbtc:          recompile-btc_data
+rbin:          recompile-bin
+rexp:          recompile-exp
+reuc:          recompile-euc
+rformal:       recompile-formal
+rgas:          recompile-gas
+rhashd:        recompile-hash_data
+rhashi:        recompile-hash_info
+rhub:          recompile-hub
+rlex:          recompile-lex
+rlogd:         recompile-log_data
+rlogi:         recompile-log_info
+rmmio:         recompile-mmio
+rmodexp:       recompile-modexp_data
+rmmu:          recompile-mmu
+rmxp:          recompile-mxp
+roob:          recompile-oob
+rprc:          recompile-prc
+rrlp_addr:     recompile-rlp_addr
+rrlp_txn:      recompile-rlp_txn
+rrlp_txnrcpt:  recompile-rlp_txnrcpt
+rrom:          recompile-rom
+rrom_lex:      recompile-rom_lex
+rshf:          recompile-shf
+rspec:         recompile-spec
+rstp:          recompile-stp
+rtrm:          recompile-trm
+rtxn_data:     recompile-txn_data
+rwcp:          recompile-wcp
+
+ospec:         buildOnGithub-spec
+
+# ==============================================================================
+# Lualatex Generation
+# ==============================================================================
+
+# Find all luatex files
+LUATEX_FILES=$(shell find * -name "*.lua.tex" -type f)
+# Determine target PDFS
+LUATEX_PDFS=$(LUATEX_FILES:%.lua.tex=%.pdf)
+
+lua_build: $(LUATEX_PDFS)
+
+%.pdf : %.lua.tex
+	$(eval DIR := $(shell dirname "$<"))
+	$(eval LUAPDF := $(shell echo "$@" | sed -e "s/\.pdf/\.lua\.pdf/"))
+	lualatex --output-directory=$(DIR) "$<"
+	mv "$(LUAPDF)" "$@"
+	rm $(DIR)/*.log $(DIR)/*.aux
+
+lua_clean:
+	rm $(LUATEX_PDFS)
+
+# adding e.g. 
+# alias pdf='make -C ~/Documents/latex/zk-evm-notes/'
+# (or whatever your path is to the zk-evm-notes folder) to ~/.bashrc
+# allows one to execute commands like 'pdf oob' to view the oob module pdf from anywhere.

README.md

@@ -0,0 +1,2 @@
+# zk-evm-notes
+Home of Linea's zk-evm specification.

alu/_all_alu.maf

@@ -0,0 +1,7 @@
+_all_alu.mtc
+_all_alu.mtc0
+_all_alu.mtc5
+_all_alu.mtc4
+_all_alu.mtc3
+_all_alu.mtc2
+_all_alu.mtc1

alu/_all_alu.mtc1

@@ -0,0 +1,10 @@
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {1.1}Introduction}{\reset@font\mtcSfont 5}{section.1.1}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {1.2}Notations}{\reset@font\mtcSfont 5}{section.1.2}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {1.3}\texttt {setAbsoluteValue}{} i.e. constraints for taking absolute values}{\reset@font\mtcSfont 6}{section.1.3}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {1.4}\texttt {setNegative}{} i.e. constraints for taking negatives}{\reset@font\mtcSfont 7}{section.1.4}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {1.5}\texttt {setAddition}{} and \texttt {setSubtraction}{} i.e. constraints for addition and subtraction}{\reset@font\mtcSfont 8}{section.1.5}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {1.6}\texttt {setMultiplication}{} i.e. constraints for multiplying \texttt {uint256}'s}{\reset@font\mtcSfont 9}{section.1.6}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {1.7}Verifying a euclidean division}{\reset@font\mtcSfont 9}{section.1.7}}
+{\reset@font\mtcPfont\mtc@string\contentsline{paragraph}{\noexpand \leavevmode Verifying ${0 \leq \mathsf {R} < \mathsf {B}}$.}{\reset@font\mtcPfont 10}{section*.3}}
+{\reset@font\mtcPfont\mtc@string\contentsline{paragraph}{\noexpand \leavevmode Verifying ${\mathsf {A}} = {\mathsf {Q} \cdot \mathsf {B}} + {\mathsf {R}}$ over the integers.}{\reset@font\mtcPfont 10}{section*.4}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {1.8}Verifying extended modular arithmetic}{\reset@font\mtcSfont 11}{section.1.8}}

alu/_all_alu.mtc2

@@ -0,0 +1,8 @@
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {2.1}Introduction}{\reset@font\mtcSfont 13}{section.2.1}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {2.2}Column descriptions}{\reset@font\mtcSfont 13}{section.2.2}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {2.3}Stamp constancies}{\reset@font\mtcSfont 14}{section.2.3}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {2.4}Heartbeat}{\reset@font\mtcSfont 14}{section.2.4}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {2.5}``Type'' constraints}{\reset@font\mtcSfont 14}{section.2.5}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {2.6}Byte decomposition constraints}{\reset@font\mtcSfont 15}{section.2.6}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {2.7}Target constraints}{\reset@font\mtcSfont 15}{section.2.7}}
+{\reset@font\mtcSfont\mtc@string\contentsline{section}{\noexpand \leavevmode \numberline {2.8}Graphical representation}{\reset@font\mtcSfont 15}{section.2.8}}