# New SMT-LIB Code Generation

How should the different types of identifiers look in the smt code we generate?

What would natural encodings be?

There are a million options.

We tried to have package data structures only once *per package* rather than *per instance*.
Similarly for games. In these cases, game / package type params need to be included.

(declare-const const-proof-{proofname}-{name} {type})
(declare-const const-game-{proofname}-{gameinstname}-{name} {type})
(assert (=
  const-proof-{proofname}-{name}
  const-game-{proofname}-{gameinstname}-{name}))

This works for consts, but not for state. We can just keep that in a state datatype, bind that to easy names at the start of a function, and then create and return a new state datatype value containing the values of our bound variables. We can even include the available constants in the initial binding:

; we have talked about this before:
; the package state should not be identified by the package instance,
; but just the package type and the package's type parameters.
; this way we can reuse them better.
; for now, let's ignore the type params in the implementation,
; but keep a notice there to remind us
(define-datatype
  PackageState-{packagename}-{type-params}
  (mk-PackageState-{pkgname}-{type-params}
    (PackageState-{pkgname}-{type-params}-T (Array Int Bits_n))))

; Similar with the game state.
; however, it of course references all the package states by package instance name.
(define-datatype
  GameState-{gamename}-{game-type-params}
  (mk-GameState-{gamename}-{game-type-params}
    (GameState-{gamename}-{game-type-params}-{pkginst} PackageState-{pkgname}-{pkg-type-params})
    (GameState-{gamename}-{game-type-params}-{mi-pkginst} (Array Integer PackageState-{pkgname}-{pkg-type-params}))))

; the const params of a package. can be shared between different package isntances that use the same type params.
(define-datatype
  PackageConstParams-{pkg-name}-{type-params}
  (mk-PackageConstParams-{pkgname}-{type-params}
    ((PackageConstParams-{pkgname}-{type-params}-n Int))))

; the same for games.
(define-datatype
  GameConstParams-{game-name}-{game-type-params}
  (mk-GameConstParams-{game-name}-{game-type-params}
    ((GameConstParams-{game-name}-{game-type-params}-n Int))))

; this maps the game's parameters to the parameters of a package instance in the game.
; basically it is the smt represenation of the params block in a package instantiation.
; this should also contain the type params of the game and the package in the function name, but i was too lazy to include it.
; the function can be called in 
(define-function game-pkg-const-param-mapping-{game-name}-{pkg-inst-name} (params GameConstParams-{game-name}) PackageConstParams-{pkg-name} 
  ...
)

; while this is pretty, it doesn't work for function parameters (at least as long as we
; try to be SMT-LIB 2.6-compatible). So what we do here instead is
; - for game-level function params, just declare free functions
; - for package-level function params, define functions that call the game's function
;   that is assigned to it in the package instantiation.

; the return type is basically like before
(define-datatype
  OracleReturn-{game-name}-{game-type-params}-{pkg-name}-{pkg-type-params}-{oracle-name}
  (ok-OracleReturn-{game-name}-{game-type-params}-{pkg-name}-{pkg-type-params}-{oracle-name}
     (OracleReturn-{game-name}-{game-type-params}-{pkg-name}-{pkg-type-params}-{oracle-name}-gamestate GameState-{game-name}-{game-type-params})
     (OracleReturn-{game-name}-{game-type-params}-{pkg-name}-{pkg-type-params}-{oracle-name}-return    {type})
  abort-OracleReturn-{game-name}-{game-type-params}-{pkg-name}-{pkg-type-params}-{oracle-name})


; the oracles need to be specific to the the package instance, because the called oracles
; depend on the wires the oracle is connected to.
; Whether it is specific to the game inst depends on how we handle const params.
; If const params are just a bunch of loose globals, we need to be specific because we
;   must know which of the loose global to use, and these are specific to the game instances.
; However, if we have a consts struct specific to the game, then we can pass that in and
;   extract the values from there. The proof can then pass different values in there
; We can then compute the package const params from the game const params, using the mapping function.
(define-fun
  oracle-{proofname}-{gameinstname}-{pkginstname}-{oracle-name}
  ((<state> GameState-{game-name}-{game-type-params}))
  ((<game-consts> GameConstParams-{game-name}-{game-type-params}))
  OracleReturn-{game-name}-{game-type-params}-{pkg-inst-name}-{pkg-type-params}-{oracle-name}
  (let* ( ; I am not sure if SMT-LIB has 'let*' --- the idea is that we can reference values bound within the let header
      (<pkg-consts> (game-pkg-const-param-mapping-{game-name}-{pkg-inst-name} <game-consts>))
      (T (PackageState-{pkgname}-{type-params} (GameState-{gameinstname}-T state)))
      (n (PackageConstParams-{pkgname}-{type-params}-n <pkg-consts>)))
    (...
      (let ((x ...))
        (...
          (ok-OracleReturn-{pkgname}-{typeconst}
            (mk-GameState-{gameinstname}
              (mk-PackageState-{pkgname}-{typeparams} T))
            x))))))



; This explores multi instance indices. This code hasn't been ported to use the game const params struct, it still uses the globals.
; Hence, it is still specific to the game instance.
(define-fun
  mi-oracle-{proofname}-{game-inst-name}-{mi-pkg-inst-name}-{oracle-name}
  (
    (<state> GameState-{game-inst-name})
    (<mi-idx> Integer))
  OracleReturn-{game-inst-name}-{mi-pkg-inst-name}-{oracle-name}
  (let (
      (T (PackageState-{pkg-name}-{type-params}-T (select (GameState-{game-inst-name}-{mi-pkg-inst-name} <state>))) <mi-idx>)
      (n game-{proof-name}-{game-inst-name}-const-n))
    (...
      (let ((x ...))
        (...
          (ok-OracleReturn-{pkgname}-{typeconst}
            (mk-GameState-{gameinstname}
              (store GameState-{game-inst-name}-{mi-pkg-inst-name} <mi-idx> (mk-PackageState-{pkg-name}-{type-params} T)))
            x))))))

Where we use `<name>` for system variables, so they can't collide with user variables

## Action Items

- [ ] Implement generating Package Const instantiation functions
- [ ] Bind Package Consts at oracle start
- [ ] Use plain variable names for consts in oracle code
- [ ] Implement proof -> game inst const instantiation code