Picus/NOTES.md

Notes

This keeps track of some development notes.

Installing cvc5-ff

If you are installing it for Docker, checkout Dockerfile@base in resources/ folder.

If you use Mac, make sure that you have brew installed.

1. Clone https://github.com/cvc5/cvc5. (Known to work with version de62429.)
2. Install libgmp. E.g., on Ubuntu, run apt install libgmp-dev. On Mac, run brew install gmp.
3. Run pip3 install tomli scikit-build Cython. If you use Mac, make sure that your Python is not the one installed by default with Mac. (Use brew install python -- known to work with Python 3.12.)
4. Run ./configure.sh --cocoa --auto-download --python-bindings.
5. Go to the build subdirectory and run make -j4 install.

The Circom DSL

Transcribed from ast.rs.

terminal: uint | int | string | bool | list<T> | symbol | null
setype: 'empty | 'binary | 'fieldelem
stype: 'output | 'input | 'intermediate
signal: (stype, setype)
vtype: 'var | 'comp | signal
version: (uint, uint, uint)
access: string | expression
assignop: 'var | 'sig | 'csig
infixop: 'mul | 'div | 'add | 'sub | 'pow | 'intdiv | 'mod | 'shl | 'shr
       | 'leq | 'geq | 'lt | 'gt | 'eq | 'neq | 'or | 'and | 'bor | 'band | 'bxor
prefixop: 'neg | 'not | 'comp
treduction: 'var | 'comp | 'sig

fileloc
  |- "start": uint
  |- "end": uint

number
  |- "meta": meta
  |- "v": int

tknowledge
  |- "rto": treduction | null

mknowledge
  |- "cdims": list<uint> | null
  |- "len": uint | null
  |- "absmaddr": uint | null

meta
  |- "elemid": uint
  |- "start": uint
  |- "end": uint
  |- "loc": fileloc
  |- "fileid": uint | null
  |- "compinf": string | null
  |- "tk": tknowledge
  |- "mk": mknowledge

circom
  |- "meta": meta
  |- "ver": version | null
  |- "incs": list<string>
  |- "defs": list<definition>
  |- "main": component | null
  
component: (list<string>, expression)

definition: template | function

template
  |- "meta": meta
  |- "name": string
  |- "args": list<string>
  |- "argloc": fileloc
  |- "body": statement
  |- "parallel": bool

function
  |- "meta": meta
  |- "name": string
  |- "args": list<string>
  |- "argloc": fileloc
  |- "body": statement

statement: itestmt | whilestmt | retstmt | declstmt | substmt | ceqstmt
         | logcallstmt | assertstmt | initblock | block

itestmt
  |- "meta": meta
  |- "cond": expression
  |- "if": statement
  |- "else": statement | null
  
whilestme
  |- "meta": meta
  |- "cond": expression
  |- "stmt": statement

retstmt
  |- "meta": meta
  |- "val": expression

declstmt
  |- "meta": meta
  |- "xtype": vtype
  |- "name": string
  |- "dims": list<expression>
  |- "constant": bool

substmt
  |- "meta": meta
  |- "var": string
  |- "access": list<access>
  |- "op": assignop
  |- "rhe": expression
;
ceqstmt
  |- "meta": meta
  |- "lhe": expression
  |- "rhe": expression

logcallstmt
  |- "meta": meta
  |- "arg": expression

assertstmt
  |- "meta": meta
  |- "arg": expressions

initblock
  |- "meta": meta
  |- "xtype": vtype
  |- "inits": list<statement>

block
  |- "meta": meta
  |- "stmts": list<statement>

expression: infix | prefix | inlineswitch | variable | number | call | arrayinline

infix
  |- "meta": meta
  |- "lhe": expression
  |- "op": infixop
  |- "rhe": expression

prefix
  |- "meta": meta
  |- "op": prefixop
  |- "rhe": expression

inlineswitch
  |- "meta": meta
  |- "cond": expression
  |- "true": expression
  |- "false": expression

variable
  |- "meta": meta
  |- "name": string
  |- "access": list<access>

call
  |- "meta": meta
  |- "id": string
  |- "args": list<expression>

arrayinline
  |- "meta": meta
  |- "vals": list<expression>

The Tokamak Symbolic Programming Pattern (Draft)

Current Version Badge:

The tokamak pattern is used to restrict the scope of symbolic variables in a project, so as to make developing and debugging a project written using racket/rosette easier.

Overall Principle

• T0: Whoever processes lifts.
  • for/all
  • Symbolic variables should ONLY be lifted by those functions that process/interact with them.
  • This prevents performance drop by wrapping too many nested for/all's from upper level calls.
• T1: Whoever defines checks.
  • tokamak:typed
  • A variable type should be checked/expected whenever it's defined, especially those defined by for/all construct.
  • This prevents unexpected/uncontrolled type flow.
  • If the type of a defined variable is known for sure or ensured by the function called (e.g., builtin racket/rosette function), the type checking can be skipped.
• T2: Whoever tags overrides.
  • If a function processes an argument and specifically tags it as concrete only, then it's the caller's responsibility to make sure of it (by lifting or whatever). In this case, this overrides T0.

Terms Used

• Symbolic Scope: A scope that may deal with symbolic variables.
• Symbolic Status: A symbolic status is tagged with each argument of the function that introduces a symbolic scope, indicating whether the argument is expected to be symbolic or not.

Naming Conventions

• A local variable in a for/all scope is usually named <var><lvl>, where <var> is the original name and <lvl> is the number of nested levels.
  • Example: name0, rhe1.

Tagging & Checking Symbolic Statuss

• A function that introduces a symbolic scope should explicitly tag and check the expected symbolic status of each of its arguments.

  • Usually the arguments tagged with concrete are then checked.

  • The arguments tagged with symbolic can be either symbolic or concrete.

  • Example

    ; (concrete:top) arg-node
    ; (symbolic:top) arg-scopes
    ; (symbolic:top) arg-prefix
    (define (do-interpret arg-node arg-scopes arg-prefix)
      (tokamak:typed arg-node circom:lang?)
    )
    

Decomposability

(pending)

Approaching Indecomposable Variables

(pending)

Connecting Symbolic Variables

(pending)