Merge pull request #58 from 0xPolygonHermez/feature/climb-key-const-tool

add tool to verify climb_key constants, add verification doc
0xPolygonHermez · Dec 21, 2023 · a307afd · a307afd
2 parents 29307cb + 0596850
commit a307afd
Show file tree

Hide file tree

Showing 2 changed files with 290 additions and 0 deletions.
diff --git a/tools/climb_key/climb_key_constants.md b/tools/climb_key/climb_key_constants.md
@@ -0,0 +1,175 @@
+# ClimbKey (constants)
+
+Goldilocks = **0xFFFFFFFF00000001**
+Chunks = 18 bits, 18 bits, 18 bits, 10 bits (LSB => MSB)  
+GoldilocksChunks[4] = [0x00001, 0x3C000, 0x3FFFF, 0x3FF]  
+0xFFFFFFFF00000001 == 0x00001 + 2**18 * 0x3C000 + 2 **36 * 0x3FFFF + 2 ** 54 * 0x3FF
+
+*carry* and *lt* are after apply shift and set climb bit  
+*lt* is done only with bits of chunk  
+*carryLt* = *carry* + 2 * *lt*
+
+*cols* = CLKSEL, CARRY_LT_IN, CARRY_LT_OUT, CHUNK_RANGE, LEVELS  
+*climb* = (CHUNK_RANGE * 2 + bit) & CHUNK_MASK  
+*glc* = goldilocks chunk
+
+CLKSEL = CLK + 4 * selKey0 + 8 * selKey1 + 16 * selKey2 + 32 * selKey3  
+[a1,a2..+..an] arithmetic serie with values = a1, a2, a2 + (a2-a1), a2 + 2*(a2-a1),..,an
+
+values of *cols* generated with *tools/climb_key/cpp_helpers.js* parsing output of *buildConstants*.
+
+## CLK0 GL_CHUNK = 0x00001
+
+#### clock = 0, bit = 0 (carryLtIn = 0)
+valid chunk values (all) = 0x0, 0x1-0x1ffff, 0x20000, 0x20001-0x3ffff
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|0,0,**2**,0x0,0|0x0|0x00001|ltOut = 1 (only for chunk = 0) ⇒ carryLtOut = 2|
+|0,0,**0**,0x1-0x1ffff,0|0x2-0x3fffe|0x00001|ltOut = 0, carryOut = 0 ⇒ carryLtOut = 0|
+|0,0,**3**,0x20000,0|0x00000|0x00001|ltOut = 1, carryOut = 1 ⇒ carryLtOut = 3 (1)|
+|0,0,**1**,0x20001-0x3ffff,0|0x00001-0x3fffe|0x00001|ltOut = 0, carryOut = 1 ⇒ carryLtOut = 2|
+
+(1) lt is active because ((0x20000 << 1) & 0x3FFFF) = 0
+
+#### clock = 0, bit = 1 (carryLtIn = 1)
+valid chunk values (all) = 0x0-0x1ffff, 0x20000-0x3ffff
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|0,1,0,0x0-0x1ffff,0|0x1-0x3ffff|0x00001|ltOut = 0, carryOut = 0 ⇒ carryLtOut = 0|
+|0,1,1,0x20000-0x3ffff,0|0x1-0x3ffff|0x00001|ltOut = 0, carryOut = 1 ⇒ carryLtOut = 1|
+
+## CLK1 GL_CHUNK = 0x3C000
+
+#### clock = 1, carryIn = 0, ltIn = 0 (carryLtIn = 0)
+valid chunk values (all) = 0x0-0x1dfff, 0x1e000-0x1ffff, 0x20000-0x3dfff, 0x3e000-0x3ffff
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|1,0,2,0x0-0x1dfff,0|0x0-0x3bffe(1)|0x3c00|carryOut = 0 ltOut  = 1 ⇒ carryLtOut = 2 |
+|1,0,0,0x1e000-0x1ffff,0|0x3c000-0x3fffe|0x3c00|carryOut = 0 ltOut = 0 ⇒ carryLtOut = 0|
+|1,0,3,0x20000-0x3dfff,0|0x0-0x3bffe|0x3c00|carryOut = 1 ltOut = 1 ⇒ carryLtOut = 3|
+|1,0,1,0x3e000-0x3ffff,0|0x3c000-0x3fffe|0x3c00|carryOut = 1 ltOut = 0 ⇒ carryLtOut = 1|
+
+(1) 0x3bfff not included because after shift LSB is zero
+
+#### clock = 1, carryIn = 1, ltIn = 0 (carryLtIn = 1)
+valid chunk values (all) = 0x0-0x1dfff, 0x1e000-0x1ffff, 0x20000-0x3dfff, 0x3e000-0x3ffff
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|1,1,2,0x0-0x1dfff,0|0x1-0x3bfff|0x3c000|carryOut = 0 ltOut = 1 ⇒ carryLtOut = 2|
+|1,1,0,0x1e000-0x1ffff,0|0x3c001-0x3ffff|0x3c000|carryOut = 0 ltOut = 0 ⇒ carryLtOut = 0|
+|1,1,3,0x20000-0x3dfff,0|0x1-0x3dfff|0x3c000|carryOut = 1 ltOut = 1 ⇒ carryLtOut = 3|
+|1,1,1,0x3e000-0x3ffff,0|0x3c001-0x3ffff|0x3c000|carryOut = 1 ltOut = 0 ⇒ carryLtOut = 2|
+
+#### clock = 1, carryIn = 0, ltIn = 1 (carryLtIn = 2)
+valid chunk values (all) = 0x0-0x1e000, 0x1e001-0x1ffff, 0x20000-0x3e000, 0x3e001-0x3ffff
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|1,2,2,0x0,0|0x0|0x3c000|carryOut = 0 ltOut = 1 ⇒ carryLtOut = 2 (1)|
+|1,2,2,0x0-0x1e000,0|0x0-0x3c000|0x3c000|carryOut = 0 ltOut = 1 ⇒ carryLtOut = 2|
+|1,2,0,0x1e001-0x1ffff,0|0x3c002-3fffe|0x3c000|carryOut = 0 ltOut = 0 ⇒ carryLtOut = 0|
+|1,2,3,0x20000-0x3e000,0|0x0-3c000|0x3c000|carryOut = 1 ltOut = 1 ⇒ carryLtOut = 3|
+|1,2,1,0x3e001-0x3ffff,0|0x3c002-0x3fffe|0x3c000|carryOut = 1 ltOut = 0 ⇒ carryLtOut = 1|
+
+(1) specific case at begining of table for empty rows
+
+#### clock = 1, carryIn = 1, ltIn = 1 (carryLtIn = 3)
+valid chunk values (all) = 0x0-0x1dfff, 0x1e000-0x1ffff, 0x20000-0x3dfff, 0x3e000-0x3ffff
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|1,3,2,0x0-0x1dfff,0|0x1-0x3bfff|0x3c000|carryOut = 0 ltOut = 1 ⇒ carryLtOut = 2|
+|1,3,0,0x1e000-0x1ffff,0|0x3c001-0x3ffff|0x3c000|carryOut = 0 ltOut = 0 ⇒ carryLtOut = 0|
+|1,3,3,0x20000-0x3dfff,0|0x1-0x3bfff|0x3c000|carryOut = 1 ltOut = 1 ⇒ carryLtOut = 3|
+|1,3,1,0x3e000-0x3ffff,0|0x3c001-0x3ffff|0x3c000|carryOut = 1 ltOut = 0 ⇒ carryLtOut = 1|
+
+## CLK2 GL_CHUNK = 0x3FFFF
+
+#### clock = 2, carryIn = 0, ltIn = 0 (carryLtIn = 0)
+valid chunk values (all) = 0x0-0x1ffff, 0x20000-0x3ffff
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|2,0,2,0x0-0x1ffff,0|0x0-0x3fffe|0x3ffff|carryOut = 0 ltOut = 1 ⇒ carryLtOut = 2|
+|2,0,3,0x20000-0x3ffff,0|0x0-0x3fffe|0x3ffff|carryOut = 1 ltOut = 1 ⇒ carryLtOut = 3|
+
+#### clock = 2, carryIn = 1, ltIn = 0 (carryLtIn = 1) 
+valid chunk values (all) = 0x0-0x1fffe, 0x1ffff, 0x20000-0x3fffe, 0x3ffff
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|2,1,2,0x0-0x1fffe,0|0x1-0x3fffd|0x3ffff|carryOut = 0 ltOut = 1 ⇒ carryLtOut = 2|
+|2,1,0,0x1ffff,0|0x3ffff|0x3ffff|carryOut = 0 ltOut = 0 ⇒ carryLtOut = 0|
+|2,1,3,0x20000-0x3fffe,0|0x1-0x3fffd|0x3ffff|carryOut = 1 ltOut = 1 ⇒ carryLtOut = 3|
+|2,1,1,0x3ffff,0|0x3ffff|0x3ffff|carryOut = 1 ltOut = 0 ⇒ carryLtOut = 1|
+
+#### clock = 2, carryIn = 0, ltIn = 1 (carryLtIn = 2)
+valid chunk values (all) = 0x0-0x1ffff, 0x20000-0x3ffff
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|2,2,2,0x0|0x0|0x3ffff|carryOut = 0 ltOut = 1 ⇒ carryLtOut = 2|
+|2,2,2,0x0-0x1ffff,0|0x0-0x3fffe|0x3ffff|carryOut = 0 ltOut = 1 ⇒ carryLtOut = 2|
+|2,2,3,0x20000-0x3ffff,0|0x0-0x3fffe|0x3ffff|carryOut = 1 ltOut = 1 ⇒ carryLtOut = 3|
+
+#### clock = 2, carryIn = 1, ltIn = 1 (carryLtIn = 3)
+valid chunk values (all) = 0x0-0x1ffff, 0x20000-0x3ffff
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|2,3,2,0x0-0x1ffff,0|0x0-0x3ffff|0x3ffff|carryOut = 0 ltOut = 1 ⇒ carryLtOut = 2|
+|2,3,3,0x20000-0x3ffff,0|0x1-0x3ffff|0x3ffff|carryOut = 1 ltOut = 0 ⇒ carryLtOut = 3|
+
+## CLK3 GL_CHUNK = 0x3FF
+In this clock all carryOut = 0 and ltOut = 1 otherwise key is greater o equal goldilocks, and it means invalid key (not include in lockup table)
+
+#### clock = 3 carryIn = 0, ltIn = 0 (carryLtIn = 0)  
+valid chunk values (all) = 0x0-0x1ff  
+0x1ff * 2 + 0 = 0x3fe < 0x3ff ⇒ OK !!
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|7,0,0,0x0-0x1ff,[0,4..+..252]|0x0-0x3fe|0x3ff|level % 4 == 0 ⇒ selKey0 = 1|
+|11,0,0,0x0-0x1ff,[1,5..+..253]|0x0-0x3fe|0x3ff|level % 4 == 1 ⇒ selKey1 = 1|
+|19,0,0,0x0-0x1ff,[2,6..+..254]|0x0-0x3fe|0x3ff|level % 4 == 2 ⇒ selKey2 = 1|
+|35,0,0,0x0-0x1ff,[3,7..+..255]|0x0-0x3fe|0x3ff|level % 4 == 3 ⇒ selKey3 = 1|
+
+#### clock = 3 carryIn = 1, ltIn = 0 (carryLtIn = 1)
+valid chunk values (all) = 0x0-0x1fe  
+0x1fe * 2 + 1 = 0x3fd < 0x3ff ⇒ OK !!  
+0x1ff * 2 + 1 = 0x3ff == 0x3ff && ltIn = 0 ⇒ FAILS !!
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|7,1,0,0x0-0x1fe,[0,4..+..252]|0x1-0x3fd|0x3ff|level % 4 = 0 ⇒ selKey0 = 1|
+|11,1,0,0x0-0x1fe,[1,5..+..253]|0x1-0x3fd|0x3ff|level % 4 = 1 ⇒ selKey1 = 1|
+|19,1,0,0x0-0x1fe,[2,6..+..254]|0x1-0x3fd|0x3ff|level % 4 = 2 ⇒ selKey2 = 1|
+|35,1,0,0x0-0x1fe,[3,7..+..255]|0x1-0x3fd|0x3ff|level % 4 = 3 ⇒ selKey3 = 1|
+
+#### clock = 3 carryIn = 0, ltIn = 1 (carryLtIn = 2)
+valid chunk values (all) = 0x0-0x1ff  
+0x1ff * 2 + 0 = 0x3fe < 0x3ff ⇒ OK !!  
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|7,2,0,0x0-0x0,0|0x0-0x3fe|0x3ff|level = 0 ⇒ selKey0 = 1|
+|7,2,0,0x0-0x1ff,[0,4..+..252]|0x0-0x3fe|0x3ff|level % 4 = 0 ⇒ selKey0 = 1|
+|11,2,0,0x0-0x1ff,[1,5..+..253]|0x0-0x3fe|0x3ff|level % 4 = 1 ⇒ selKey1 = 1|
+|19,2,0,0x0-0x1ff,[2,6..+..254]|0x0-0x3fe|0x3ff|level % 4 = 2 ⇒ selKey2 = 1|
+|35,2,0,0x0-0x1ff,[3,7..+..255]|0x0-0x3fe|0x3ff|level % 4 = 3 ⇒ selKey3 = 1|
+
+
+#### clock = 3 carryIn = 1, ltIn = 1 (carryLtIn = 3)
+valid chunk values (all) = 0x0-0x1ff  
+0x1fe * 2 + 1 = 0x3fd < 0x3ff ⇒ OK !!  
+0x1ff * 2 + 1 = 0x3ff == 0x3ff && ltIn = 1 ⇒ OK !!
+
+|cols(*) |climb|glc|notes|
+|------|-------|---|----|
+|7,3,0,0x0-0x1ff,[0,4..+..252]|0x1-0x3ff|0x3ff|level % 4 = 0 => selKey0 = 1|
+|11,3,0,0x0-0x1ff,[1,5..+..253]|0x1-0x3ff|0x3ff|level % 4 = 1 => selKey1 = 1|
+|19,3,0,0x0-0x1ff,[2,6..+..254]|0x1-0x3ff|0x3ff|level % 4 = 2 => selKey2 = 1|
+|35,3,0,0x0-0x1ff,[3,7..+..255]|0x1-0x3ff|0x3ff|level % 4 = 3 => selKey3 = 1|
diff --git a/tools/climb_key/cpp_helpers.js b/tools/climb_key/cpp_helpers.js
@@ -0,0 +1,115 @@
+const fs = require("fs");
+const path = require("path");
+const tty = require('tty');
+const version = require("../../package").version;
+
+const chai = require("chai");
+const assert = chai.assert;
+const expect = chai.expect;
+const F1Field = require("ffjavascript").F1Field;
+const util = require('util');
+
+const { newConstantPolsArray, newCommitPolsArray, compile, verifyPil } = require("pilcom");
+const smClimbKey = require("../../src/sm/sm_climb_key.js");
+
+const argv = require("yargs")
+    .version(version)
+    .usage("main_buildconstants -r <rom.json> -o <constant.bin|json> [-p <main.pil>] [-P <pilconfig.json>] [-v]")
+    .alias("r", "rom")
+    .alias("o", "output")
+    .alias("t", "text")
+    .alias("p", "pil")
+    .alias("P", "pilconfig")
+    .alias("v", "verbose")
+    .argv;
+
+const DEBUG = false;
+
+async function run() {
+    const F = new F1Field("0xFFFFFFFF00000001");
+    const pilCode = `
+    include "pil/global.pil";
+    include "pil/climb_key.pil";
+    `;
+
+    const pil = await compile(F, pilCode, null, { compileFromString: true, defines: {N: 2 ** 22}});
+    const constPols = newConstantPolsArray(pil);
+    const pols = constPols.ClimbKey;
+
+    await smClimbKey.buildConstants(pols);
+
+    // T_CLKEYSEL, T_LEVEL, T_CHUNK_VALUE, T_CARRYLT_IN, T_CARRYLT_OUT => "T_CLKEYSEL,T_LEVEL,T_CARRYLT_IN, T_CARRYLT_OUT", FROM_T_CHUNK_VALUE, TO_T_CHUNK_VALUE
+
+    const N = pols.T_CLKEYSEL.length;
+    let _cols = false;
+    let _colvalues = [];
+    let _fromChunkValue = false;
+    let _toChunkValue = false;
+    let _row = false;
+    let groups = [];
+    let _level = false;
+    let cols ;
+
+    for (let row = 0; row <= N; ++row) {
+        if (DEBUG && row < N) {
+            console.log('ROW#'+row+' '+[pols.T_CLKEYSEL[row], pols.T_CARRYLT_IN[row], pols.T_CARRYLT_OUT[row], pols.T_LEVEL[row], pols.T_CHUNK_VALUE[row].toString(16)].join(','));
+        }
+        const colvalues = (row < N) ? [pols.T_CLKEYSEL[row], pols.T_CARRYLT_IN[row], pols.T_CARRYLT_OUT[row], pols.T_LEVEL[row]] : false;
+        const cols = colvalues === false ? false : colvalues.join(',');
+        if (_cols === false) {
+            _cols = cols;
+            _colvalues = [...colvalues];
+            _row = row;
+        } else if (_cols !== cols) {
+            groups.push({cols: _cols, chunk: _fromChunkValue == _toChunkValue ? [_fromChunkValue] : [_fromChunkValue, _toChunkValue], colvalues: [..._colvalues], label: `[${_row}..${row-1}] ${cols} ${Math.round((_row*10000)/N)/100}%`});
+            _fromChunkValue = false;
+            _toChunkValue = false;
+            _cols = cols;
+            _colvalues = [...colvalues];
+            _row = row;
+        }
+        // Check end of loop, after that repeat sequence.
+        if (_level > 0 && pols.T_LEVEL[row] === 0n) {
+            break;
+        }
+        _level = Number(pols.T_LEVEL[row]);
+        if (_fromChunkValue === false || _fromChunkValue > pols.T_CHUNK_VALUE[row]) {
+            _fromChunkValue = pols.T_CHUNK_VALUE[row];
+        }
+        if (_toChunkValue === false || _toChunkValue < pols.T_CHUNK_VALUE[row]) {
+            _toChunkValue = pols.T_CHUNK_VALUE[row];
+        }
+    }
+    if (DEBUG) console.log("{\n" + groups.map(x => `\t\t{"${x.cols}", ${x.chunk.map(x => '0x'+x.toString(16)).join('-')}, ${x.colvalues.slice(0, 3).join(',')}}, // ${x.label}`).join("\n") + '\n};');
+    let common3 = {};
+    groups.map(x => {
+        let ckey = [...x.colvalues.slice(0, 3),x.chunk.map(x => '0x'+x.toString(16)).join('-')].join();
+        if (!common3[ckey]) {
+            common3[ckey] = []; 
+        }
+        common3[ckey].push(x.colvalues[3]);
+        return x.colvalues.join(',');
+    });
+    for (const key in common3) {
+        const levels = common3[key];
+        if (levels.length == 1 || (levels.length == 2 && levels[0] == levels[1])) {
+            common3[key] = levels[0].toString();
+            continue;
+        }
+        let clevel = levels[0];
+        if (levels.every(level => {const _clevel = clevel; clevel += 4n; return level === _clevel;})) {
+            common3[key] = levels[0] + ',' + levels[1] + '..+..' + levels.slice(-1)[0];
+        }
+    }
+    for (const key in common3) {
+        console.log(key+','+common3[key]);
+    }
+}
+
+run().then(()=> {
+    process.exit(0);
+}, (err) => {
+    console.log(err.message);
+    console.log(err.stack);
+    process.exit(1);
+});