doc: add Coq documentation

formal-land · Nov 25, 2024 · 17a06b9 · 17a06b9
1 parent 0f1af39
commit 17a06b9
Show file tree

Hide file tree

Showing 18 changed files with 3,180 additions and 14 deletions.
diff --git a/.github/workflows/coq-docs.yml b/.github/workflows/coq-docs.yml
@@ -0,0 +1,40 @@
+name: Coq docs
+on:
+  push:
+    branches:
+      - main
+
+jobs:
+  deploy:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write  # To push a branch 
+      pages: write  # To push to a GitHub Pages site
+      id-token: write # To update the deployment status
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - name: Install latest mdbook
+        run: |
+          tag=$(curl 'https://api.github.com/repos/rust-lang/mdbook/releases/latest' | jq -r '.tag_name')
+          url="https://github.com/rust-lang/mdbook/releases/download/${tag}/mdbook-${tag}-x86_64-unknown-linux-gnu.tar.gz"
+          mkdir mdbook
+          curl -sSL $url | tar -xz --directory=./mdbook
+          echo `pwd`/mdbook >> $GITHUB_PATH
+      - name: Build Book
+        run: |
+          # This assumes your book is in the root of your repository.
+          # Just add a `cd` here if you need to change to another directory.
+          cd coq/docs
+          mdbook build
+      - name: Setup Pages
+        uses: actions/configure-pages@v4
+      - name: Upload artifact
+        uses: actions/upload-pages-artifact@v3
+        with:
+          # Upload entire repository
+          path: 'book'
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4
diff --git a/coq/CoqOfSolidity/contracts/erc20/contract.json b/coq/CoqOfSolidity/contracts/erc20/contract.json
@@ -1480,7 +1480,7 @@
                                   "value": {
                                     "arguments": [],
                                     "functionName": {
-                                      "name": "abi_decode_address_2305",
+                                      "name": "abi_decode_t_address",
                                       "nodeType": "YulIdentifier"
                                     },
                                     "nodeType": "YulFunctionCall"
@@ -3545,7 +3545,7 @@
                                   "value": {
                                     "arguments": [],
                                     "functionName": {
-                                      "name": "abi_decode_address_2305",
+                                      "name": "abi_decode_t_address",
                                       "nodeType": "YulIdentifier"
                                     },
                                     "nodeType": "YulFunctionCall"
@@ -4244,7 +4244,7 @@
                   }
                 ]
               },
-              "name": "abi_decode_address_2305",
+              "name": "abi_decode_t_address",
               "nodeType": "YulFunctionDefinition",
               "returnVariables": [
                 {
@@ -6237,7 +6237,7 @@
       "subObjects": [
         {
           "nodeType": "YulData",
-          "value": "a26469706673582212201a1fe65a5b6e9a889cfa2e0e3e08138191bebe93076641e37824cf6a4c5c784264736f6c634300081b0033"
+          "value": "a2646970667358221220d281a516cd90dd74be97397d2ed1953fb71afa6324f6cfa5aa3855fe59e15c9364736f6c634300081d0033"
         }
       ]
     }

diff --git a/coq/CoqOfSolidity/contracts/erc20/contract.v b/coq/CoqOfSolidity/contracts/erc20/contract.v
@@ -505,7 +505,7 @@ Module Erc20.
             )
           );
           Code.Function.make (
-            "abi_decode_address_2305",
+            "abi_decode_t_address",
             [],
             ["value"],
             M.scope (
@@ -1885,7 +1885,7 @@ Module Erc20.
                                 M.declare (|
                                   ["value1"],
                                   Some (M.call_function (|
-                                    "abi_decode_address_2305",
+                                    "abi_decode_t_address",
                                     []
                                   |))
                                 |)
@@ -2924,7 +2924,7 @@ Module Erc20.
                                 M.declare (|
                                   ["value1_1"],
                                   Some (M.call_function (|
-                                    "abi_decode_address_2305",
+                                    "abi_decode_t_address",
                                     []
                                   |))
                                 |)

diff --git a/coq/CoqOfSolidity/contracts/erc20/contract.yul b/coq/CoqOfSolidity/contracts/erc20/contract.yul
@@ -83,7 +83,7 @@ object "Erc20_403" {
                         if callvalue() { revert(0, 0) }
                         if slt(add(calldatasize(), not(3)), 96) { revert(0, 0) }
                         let value0_1 := abi_decode_address()
-                        let value1 := abi_decode_address_2305()
+                        let value1 := abi_decode_t_address()
                         let value := calldataload(68)
                         /// @src 0:1219:1224  "value"
                         fun_transfer(value0_1, value1, value)
@@ -171,7 +171,7 @@ object "Erc20_403" {
                         if callvalue() { revert(0, 0) }
                         if slt(add(calldatasize(), not(3)), 64) { revert(0, 0) }
                         let value0_5 := abi_decode_address()
-                        let value1_1 := abi_decode_address_2305()
+                        let value1_1 := abi_decode_t_address()
                         mstore(0, and(value0_5, sub(shl(160, 1), 1)))
                         mstore(32, /** @src 0:770:781  "_allowances" */ 0x01)
                         /// @src 0:65:3516  "contract Erc20 {..."
@@ -197,7 +197,7 @@ object "Erc20_403" {
                 value := calldataload(4)
                 if iszero(eq(value, and(value, sub(shl(160, 1), 1)))) { revert(0, 0) }
             }
-            function abi_decode_address_2305() -> value
+            function abi_decode_t_address() -> value
             {
                 value := calldataload(36)
                 if iszero(eq(value, and(value, sub(shl(160, 1), 1)))) { revert(0, 0) }
@@ -307,7 +307,7 @@ object "Erc20_403" {
                 log3(_5, /** @src 0:65:3516  "contract Erc20 {..." */ 0x20, /** @src 0:2251:2276  "Transfer(from, to, value)" */ 0xddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef, _2, _1)
             }
         }
-        data ".metadata" hex"a26469706673582212201a1fe65a5b6e9a889cfa2e0e3e08138191bebe93076641e37824cf6a4c5c784264736f6c634300081b0033"
+        data ".metadata" hex"a2646970667358221220d281a516cd90dd74be97397d2ed1953fb71afa6324f6cfa5aa3855fe59e15c9364736f6c634300081d0033"
     }
 }
 
diff --git a/coq/CoqOfSolidity/contracts/erc20/shallow.v b/coq/CoqOfSolidity/contracts/erc20/shallow.v
@@ -84,7 +84,7 @@ Module Erc20_403.
       in
       M.pure value.
 
-    Definition abi_decode_address_2305 : M.t U256.t :=
+    Definition abi_decode_t_address : M.t U256.t :=
       let~ '(_, value) :=
         let value := 0 in
         let~ value := [[ calldataload ~(| 36 |) ]] in
@@ -293,7 +293,7 @@ Module Erc20_403.
                     |)
                   ]] default~ tt in
                   let~ value0_1 := [[ abi_decode_address ~(||) ]] in
-                  let~ value1 := [[ abi_decode_address_2305 ~(||) ]] in
+                  let~ value1 := [[ abi_decode_t_address ~(||) ]] in
                   let~ value := [[ calldataload ~(| 68 |) ]] in
                   do~ [[ fun_transfer ~(| value0_1, value1, value |) ]] in
                   do~ [[ mstore ~(| 0, and ~(| value0_1, sub ~(| shl ~(| 160, 1 |), 1 |) |) |) ]] in
@@ -433,7 +433,7 @@ Module Erc20_403.
                     |)
                   ]] default~ tt in
                   let~ value0_5 := [[ abi_decode_address ~(||) ]] in
-                  let~ value1_1 := [[ abi_decode_address_2305 ~(||) ]] in
+                  let~ value1_1 := [[ abi_decode_t_address ~(||) ]] in
                   do~ [[ mstore ~(| 0, and ~(| value0_5, sub ~(| shl ~(| 160, 1 |), 1 |) |) |) ]] in
                   do~ [[ mstore ~(| 32, 0x01 |) ]] in
                   let~ dataSlot_6 := [[ keccak256 ~(| 0, 64 |) ]] in