documentation update

.gitignore

@@ -38,3 +38,6 @@ CoqMakefile.conf
 *.vo
 *.vos
 *.css
+Makefile
+*.pdf
+doc

coqdoc.css

@@ -63,8 +63,9 @@ div:empty{ display: none;}
 #main .doc {
     margin: 0;
     text-align: left;
-    background-color: rgba(0,0,0,0.08);
-    max-width: 40em;
+    background-color: #d3d3d3; //rgba(0,0,0,0.08);
+    padding: 1em;
+    max-width: 50em;
 }
 
 .inlinecode, .code, #main pre {
@@ -196,4 +197,8 @@ ul.doclist {
     display: inline;
 }
 
-
+ul,li {
+    /*margin:20pt;*/
+   margin-left: 0.5em;
+   padding-left:0.5em;
+}

docseq

@@ -1,41 +1,46 @@
+doc/EraVM.Introduction.html
 doc/EraVM.Glossary.html
-doc/EraVM.Common.html
 doc/EraVM.Core.html
 doc/EraVM.PrimitiveValue.html
+
 doc/EraVM.State.html
-doc/EraVM.CallStack.html
-doc/EraVM.KernelMode.html
+doc/EraVM.GPR.html
+doc/EraVM.Flags.html
 doc/EraVM.Predication.html
-doc/EraVM.Addressing.html
-doc/EraVM.Resolution.html
-doc/EraVM.Bootloader.html
-doc/EraVM.Coder.html
-doc/EraVM.Decommitter.html
-doc/EraVM.Ergs.html
+doc/EraVM.Memory.html
+doc/EraVM.Pointer.html
+doc/EraVM.Slice.html
+doc/EraVM.CallStack.html
+doc/EraVM.MemoryContext.html
+
 doc/EraVM.History.html
 doc/EraVM.Event.html
-doc/EraVM.Flags.html
-doc/EraVM.GPR.html
-doc/EraVM.Memory.html
+
 doc/EraVM.MemoryBase.html
 doc/EraVM.MemoryOps.html
-doc/EraVM.MemoryContext.html
 doc/EraVM.MemoryManagement.html
-doc/EraVM.Slice.html
-doc/EraVM.Pointer.html
-doc/EraVM.StaticMode.html
-doc/EraVM.VersionedHash.html
 
+
+doc/EraVM.Addressing.html
+doc/EraVM.Resolution.html
 doc/EraVM.isa.Instructions.html
+doc/EraVM.isa.Modifiers.html
 doc/EraVM.isa.Assembly.html
 doc/EraVM.isa.CoreSet.html
+doc/EraVM.isa.GeneratedMachISA.html
 doc/EraVM.isa.AssemblyToCore.html
-doc/EraVM.isa.Modifiers.html
+doc/EraVM.isa.AssemblyToMach.html
 
+doc/EraVM.Ergs.html
+doc/EraVM.KernelMode.html
+doc/EraVM.StaticMode.html
+doc/EraVM.Steps.html
 doc/EraVM.Semantics.html
 doc/EraVM.VMPanic.html
 doc/EraVM.sem.SemanticCommon.html
-doc/EraVM.sem.StepPanic.html
+
+
+doc/EraVM.sem.Nop.html
 doc/EraVM.sem.SpAdd.html
 doc/EraVM.sem.SpSub.html
 doc/EraVM.sem.Jump.html
@@ -54,14 +59,15 @@ doc/EraVM.sem.Ror.html
 
 doc/EraVM.sem.NearCall.html
 doc/EraVM.sem.NearRet.html
-doc/EraVM.sem.NearRetTo.html
 doc/EraVM.sem.NearRevert.html
+doc/EraVM.sem.NearRetTo.html
 doc/EraVM.sem.NearRevertTo.html
+doc/EraVM.sem.StepPanic.html
 doc/EraVM.sem.Panic.html
 doc/EraVM.sem.NearPanicTo.html
+doc/EraVM.sem.Farcall.html
 doc/EraVM.sem.FarRet.html
 doc/EraVM.sem.FarRevert.html
-doc/EraVM.sem.Farcall.html
 
 doc/EraVM.sem.LoadPtr.html
 doc/EraVM.sem.LoadPtrInc.html
@@ -80,19 +86,29 @@ doc/EraVM.sem.SLoad.html
 
 doc/EraVM.sem.OpEvent.html
 doc/EraVM.sem.ToL1.html
-doc/EraVM.sem.Context.html
 doc/EraVM.sem.PrecompileCall.html
 
+doc/EraVM.sem.Context.html
 
-doc/EraVM.Steps.html
+
+doc/EraVM.Coder.html
 doc/EraVM.ABI.html
+doc/EraVM.ABI.NearCallABI.html
 doc/EraVM.ABI.FatPointerABI.html
 doc/EraVM.ABI.ForwardPageTypesABI.html
-doc/EraVM.ABI.FarRetABI.html
 doc/EraVM.ABI.FarCallABI.html
+doc/EraVM.ABI.FarRetABI.html
 doc/EraVM.ABI.MetaParametersABI.html
-doc/EraVM.ABI.NearCallABI.html
 doc/EraVM.ABI.PrecompileParametersABI.html
+
+doc/EraVM.encoding.EncodingUtils.html
+doc/EraVM.encoding.GeneratedEncodeOpcode.html
+doc/EraVM.encoding.Encoder.html
+
+doc/EraVM.Bootloader.html
 doc/EraVM.Precompiles.html
+doc/EraVM.VersionedHash.html
+doc/EraVM.Decommitter.html
+
 doc/EraVM.Arith.html
 doc/index.html

src/ABI.v

@@ -9,13 +9,10 @@ Import Core Common Coder Bool GPR Ergs Memory MemoryManagement Pointer.
 This section details the serialization and deserialization formats for compound
 instruction arguments.
 
-
-Currently, they are not described in details, but introduced axiomatically.
-
 The description from Rust VM implementation is described here:
 https://github.com/matter-labs/zkevm_opcode_defs/blob/v1.4.1/src/definitions/abi
 
-## Fat pointers *)
+*)
 Require Export
   ABI.FatPointerABI
   ABI.MetaParametersABI

src/ABI/FarCallABI.v

@@ -3,6 +3,7 @@ Require Coder Ergs MemoryManagement Pointer lib.BitsExt ABI.FatPointerABI ABI.Fo
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
 Import Arith Core Common Coder Ergs Memory MemoryManagement Pointer lib.BitsExt FatPointerABI ForwardPageTypesABI.
 
+Section FarCallABI.
 Record params :=
   mk_params {
       fwd_memory: fwd_memory;
@@ -177,3 +178,4 @@ fun params =>
 End LayoutCoder.
 
 Definition coder := coder_compose coder_binary coder_layout.
+End FarCallABI.

src/ABI/FarRetABI.v

@@ -3,7 +3,9 @@ Require Coder Ergs MemoryManagement Pointer lib.BitsExt ABI.FatPointerABI ABI.Fo
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
 Import Arith Core Common Coder Ergs Memory MemoryManagement Pointer lib.BitsExt FatPointerABI ForwardPageTypesABI.
 
-Record params :=
+
+Section FarRetABI.
+  Record params :=
   mk_params {
       fwd_memory: fwd_memory;
     }.
@@ -147,3 +149,4 @@ fun params =>
 End LayoutCoder.
 
 Definition coder := coder_compose coder_binary coder_layout.
+End FarRetABI.

src/ABI/FatPointerABI.v

@@ -3,6 +3,7 @@ Require Coder Pointer lib.BitsExt.
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
 Import Core Common Coder Pointer lib.BitsExt.
 
+Section FatPointerABI.
 (** Record [%fat_ptr_layout] displays the memory layout of a 128-bit fat pointer.*)
 Record fat_ptr_layout := mk_fat_ptr_layout {
                               length: u32;
@@ -11,7 +12,6 @@ Record fat_ptr_layout := mk_fat_ptr_layout {
                               offset: u32;
                             }.
 Definition null_fat_ptr_layout := mk_fat_ptr_layout zero32 zero32 zero32 zero32.
-
 Section LayoutCoder.
   (** Functions [%encode_layout] and [%decode_layout] formalize the encoding of
   a [%fat_ptr_nullable] to [%fat_ptr_layout]. *)
@@ -163,3 +163,4 @@ Section ComposedCoder.
     | _ => None
     end.
 End ComposedCoder.
+End FatPointerABI.

src/ABI/MetaParametersABI.v

@@ -3,6 +3,7 @@ Require Coder Ergs MemoryManagement Pointer lib.BitsExt.
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
 Import Arith Core Common Coder Ergs Memory MemoryManagement Pointer lib.BitsExt.
 
+Section MetaParametersABI.
 Record params :=
   mk_params {
       ergs_per_pubdata_byte: ergs;
@@ -134,3 +135,4 @@ Qed.
 End LayoutCoder.
 
 Definition coder := coder_compose binary_coder layout_coder.
+End MetaParametersABI.

src/ABI/NearCallABI.v

@@ -3,6 +3,7 @@ Require Coder Ergs Memory.
 Import ssreflect.
 Import Types Core Coder Ergs Memory.
 
+Section NearCallABI.
 Record params: Type :=
   mk_params {
       ergs_passed: u32;
@@ -22,3 +23,4 @@ refine (mk_coder decode encode _).
 unfold revertible, encode, decode.
 by move => []; inversion 1.
 Defined.
+End NearCallABI.

src/ABI/PrecompileParametersABI.v

@@ -3,7 +3,9 @@ Require Coder Memory lib.BitsExt.
 Import ssreflect ssreflect.ssrfun ssreflect.eqtype ssreflect.tuple.
 Import Core Common Coder Memory lib.BitsExt.
 
-Record params :=
+Section PrecompileParametersABI.
+
+  Record params :=
   mk_params
     {
       input_memory_offset: mem_address;
@@ -49,5 +51,5 @@ Canonical params_eqType := Eval hnf in EqType _ params_eqMixin.
 (* end details *)
 
 
-
 Axiom ABI: @coder word params.
+End PrecompileParametersABI.

src/Core.v

@@ -24,6 +24,7 @@ EraVM is a 256-bit register-based language machine with two stacks and dedicated
   (* end details *)
 End Parameters.
 
+Section ArchOverview.
 (**
 ![](img/arch-overview.png)
 
@@ -175,6 +176,6 @@ There are three types of behaviors triggered by execution failures.
 
 
 *)
-
+End ArchOverview.
 Definition timestamp := nat.
 Definition tx_num := u16.

src/Glossary.v

@@ -1,3 +1,4 @@
+Section Glossary.
 (** # Notations
 
 - Definitional equality is denoted with $A:=B$. Its meaning is: $A$ can be substituted with $B$.
@@ -26,7 +27,6 @@
 - **ABI** --  application binary interface. See [%ABI].
 - **Active external frame** --  the closest external frame to the top of call stack. For example, in a callstack [%(InternalCall _ (InternalCall _ (ExternalCall _ (InternalCall _ ...))))] the active external frame will be the third frame in stack. See [%active_extframe].
 - **Auxheap** --  one of two heap variants (heap and auxheap), mostly used by system contracts. Executing one of far call instructions creates a new external frame and allocates pages for code, constants, data stack, heap and aux heap.
-- **Batch** -- ??
 - **Burning ergs** --  setting ergs to zero in topmost call stack frame, external or internal. See [%Ergs].
 - **Callstack** --  a stack of context information. Executing one of near call instructions pushes a frame of type [%InternalCall] to the callstack, executing one of far call instructions pushes a frame of type [%ExternalCall]. See [%CallStack].
 - **Checkpoint** -- see [%state_checkpoint]. Not to confuse with EraVM snapshot.
@@ -64,11 +64,10 @@
 - **Memory forwarding** -- a mechanism of sharing a read-only fragment ofmemory between contracts. The memory fragment is created from [%span] and described by [%fat_ptr]. This fragment can be narrowed or shrunk as a result of far call or executing [%OpPtrShrink].
 - **Machine instruction** -- a low-level machine instruction with a fixed format. The high-level [%instruction_predicated] is encoded to machine instructions.
 - **Memory growth** -- a process, where an access to a heap variant beyond its bound leads to increasing the bound and payment.
-- **Message** --  TODO
 - **Narrowing a fat pointer** -- subtract a given number from its length and add it to its start; it is guaranteed to not overflow. See [%fat_ptr_narrow]. Used when passing a fat pointer to a far call, or returning it from a contract.
 - **Near call** -- calling a function that belongs to the same contract.
 - **Operand** --  data or the address that is operated upon by the instruction. It represents the input or output values used by the instruction to perform a specific operation or computation. See [%InstructionArguments].
-- **Page** -- see [%page].
+- **Page** -- see [%page_type].
 - **Pointer value** -- a [%primitive_value] with a set pointer tag. May contain a fat pointer. See [%PtrValue].
 - **Precompile call** -- an invokation of [%OpPrecompileCall]. Precompiles are
 extensions of EraVM bound to one of the system contracts. When this contract
@@ -83,33 +82,34 @@ algorithm specific to this contract. See [%Precompiles].
 - **System contracts** -- contracts with addresses from 0 to [%KERNEL_MODE_MAXADDR_LIMIT]. They are executed in [%KernelMode].
 - **Topmost callstack frame** -- the last frame pushed to call stack.
 - **Word** -- 256-bit unsigned untagged integer value.
-- **address resolution** -- a matching between instruction operands and locations using the supported address modes. See [%resolve].
-- **base cost** -- the fixed cost of executing instruction, in ergs. Some instructions imply additional costs, e.g. far calls may require paying for code decommitment.
-- **bootloader** -- a system contract written in YUL in charge of block construction.
-- **cell** -- alias to "word". Often used to distinguish between values themselves and the memory locations holding them.
-- **depot** -- all storages in all shards. See [%depot].
-- **ergs** -- resource spent on actions such as executing instructions. See [%Ergs].
-- **instruction predicate** -- see [%Predication].
-- **flag** -- see [%flag_state].
-- **fully qualified address** -- see [%fqa_key].
-- **instruction** -- low-level command or operation that is executed by a virtual machine to perform a specific task. Instructions supported by EraVm are described by the type [%instruction_predicated].
-- **kernel mode** -- a mode of execution for system contracts opening access to full instruction set, containing instructions potentially harmful to the global state e.g. [%OpContextIncrementTxNumber]. See [%KernelMode].
-- **key** -- a 256-bit address of a cell in storage.
-- **location** -- see [%loc].
-- **panic** -- irrecoverable error. Handled by formally executing [%OpPanic].
-- **revert** -- execution of [%OpRevert], usually as a consequence of recoverable error.
-- **malformed transaction** -- a transaction rejected by the bootloader. Handling it is the responsibility of the server that controls EraVM.
-- **predicate** -- see [%Predication].
-- **predication** -- see [%Predication].
-- **program counter** -- the [%code_address] of the next instruction to be executed. See [%cf_pc].
-- **rollback** -- restoration of the [%gs_revertable] portion of [%state] as a result of revert or panic. The state is saved at every near or far call. See also [%state_checkpoint].
-- **shard** -- a collection of [%storage]s. See [%shard].
-- **snapshot** -- a copy of the full state of EraVM. Server makes a snapshot of VM state every time a transaction is successfully completed. When the bootloader encounters a malformed transaction, it fails, and the server restarts EraVM from the most recent snapshot, skipping this transaction.
-- **server** -- a program that launches EraVM and controls it. Feeds the transactions to the bootloader, provides decommitter and other external modules, restarts EraVM from the latest snapshot in case of malformed transactions.
-- **stack pointer** -- the [%stack_address] where the next element will be pushed. It is the address of the (top of the stack + 1).
-- **static mode** -- see [%StaticMode].
-- **storage** -- see [%storage].
-- **total cost** -- a sum of [%base_cost] of an instruction and all its additional costs.
-- **versioned hash** -- a key used to retrieve the contract code from decommitter. See [%versioned_hash] and [%Decommitter].
+- **Address resolution** -- a matching between instruction operands and locations using the supported address modes. See [%resolve].
+- **Base cost** -- the fixed cost of executing instruction, in ergs. Some instructions imply additional costs, e.g. far calls may require paying for code decommitment.
+- **Bootloader** -- a system contract written in YUL in charge of block construction.
+- **Cell** -- alias to "word". Often used to distinguish between values themselves and the memory locations holding them.
+- **Depot** -- all storages in all shards. See [%depot].
+- **Ergs** -- resource spent on actions such as executing instructions. See [%Ergs].
+- **Instruction predicate** -- see [%Predication].
+- **Flag** -- see [%flag_state].
+- **Fully qualified address** -- see [%fqa_key].
+- **Instruction** -- low-level command or operation that is executed by a virtual machine to perform a specific task. Instructions supported by EraVm are described by the type [%instruction_predicated].
+- **Kernel mode** -- a mode of execution for system contracts opening access to full instruction set, containing instructions potentially harmful to the global state e.g. [%OpContextIncrementTxNumber]. See [%KernelMode].
+- **Key** -- a 256-bit address of a cell in storage.
+- **Location** -- see [%loc].
+- **Panic** -- irrecoverable error. Handled by formally executing [%OpPanic].
+- **Revert** -- execution of [%OpRevert], usually as a consequence of recoverable error.
+- **Malformed transaction** -- a transaction rejected by the bootloader. Handling it is the responsibility of the server that controls EraVM.
+- **Predicate** -- see [%Predication].
+- **Predication** -- see [%Predication].
+- **Program counter** -- the [%code_address] of the next instruction to be executed. See [%cf_pc].
+- **Rollback** -- restoration of the [%gs_revertable] portion of [%state] as a result of revert or panic. The state is saved at every near or far call. See also [%state_checkpoint].
+- **Shard** -- a collection of [%storage]s. See [%shard].
+- **Snapshot** -- a copy of the full state of EraVM. Server makes a snapshot of VM state every time a transaction is successfully completed. When the bootloader encounters a malformed transaction, it fails, and the server restarts EraVM from the most recent snapshot, skipping this transaction.
+- **Server** -- a program that launches EraVM and controls it. Feeds the transactions to the bootloader, provides decommitter and other external modules, restarts EraVM from the latest snapshot in case of malformed transactions.
+- **Stack pointer** -- the [%stack_address] where the next element will be pushed. It is the address of the (top of the stack + 1).
+- **Static mode** -- see [%StaticMode].
+- **Storage** -- see [%storage].
+- **Total cost** -- a sum of [%base_cost] of an instruction and all its additional costs.
+- **Versioned hash** -- a key used to retrieve the contract code from decommitter. See [%versioned_hash] and [%Decommitter].
 - **VM** -- the same as EraVM, the abstract virtual machine that this document specifies.
  *)
+End Glossary.