Function simplicity_analyseBounds

src/simplicity/eval.c:588–745

:TODO: Document extraFrameBound in the Tech Report (and implement it in Haskell) */ Given a well-typed dag representing a Simplicity expression, compute the memory and CPU requirements for evaluation. * * If 'malloc' fails, then returns SIMPLICITY_ERR_MALLOC. * When maxCells < UBOUNDED_MAX, if the bounds on the number of cells needed for evaluation of 'dag' on an idealized Bit Machine exceeds m

 *                 and if maxCells < UBOUNDED_MAX then '*frameBound' bounds the number of stack frames needed during execution of 'dag'.
 */
simplicity_err simplicity_analyseBounds( ubounded *cellsBound, ubounded *UWORDBound, ubounded *frameBound, ubounded *costBound
                                       , ubounded maxCells, ubounded minCost, ubounded maxCost, const dag_node* dag, const type* type_dag, const size_t len) {
  static_assert(DAG_LEN_MAX <= SIZE_MAX / sizeof(boundsAnalysis), "bound array too large.");
  static_assert(1 <= DAG_LEN_MAX, "DAG_LEN_MAX is zero.");
  static_assert(DAG_LEN_MAX - 1 <= UINT32_MAX, "bound array index does not fit in uint32_t.");
  simplicity_assert(1 <= len);
  simplicity_assert(len <= DAG_LEN_MAX);
  boundsAnalysis* bound = simplicity_malloc(len * sizeof(boundsAnalysis));
  if (!bound) return SIMPLICITY_ERR_MALLOC;

  /* Sum up the total costs.
   * The computations for extraCells and cost are clipped at UBOUNDED_MAX,
   * so a result of UBOUNDED_MAX means "UBOUNDED_MAX or larger".
   *
   * The extraUWORD computation may produce unsigned overflow.
   * However the extraUWORD true value is less than the true value of extraCells.
   * As long as extraCells is strictly less than UBOUNDED_MAX, extraUWORD will be too.
   *
   * The extraFrame computation is bounded by DAG_LEN, and cannot overflow.
   */
  for (size_t i = 0; i < len; ++i) {
    switch (dag[i].tag) {
     case ASSERTL:
     case ASSERTR:
     case CASE:
      bound[i].extraCellsBound[0] = bounded_max( bound[dag[i].child[0]].extraCellsBound[0]
                                       , bound[dag[i].child[1]].extraCellsBound[0] );
      bound[i].extraCellsBound[1] = bounded_max( bound[dag[i].child[0]].extraCellsBound[1]
                                       , bound[dag[i].child[1]].extraCellsBound[1] );

      bound[i].extraUWORDBound[0] = bounded_max( bound[dag[i].child[0]].extraUWORDBound[0]
                                       , bound[dag[i].child[1]].extraUWORDBound[0] );
      bound[i].extraUWORDBound[1] = bounded_max( bound[dag[i].child[0]].extraUWORDBound[1]
                                       , bound[dag[i].child[1]].extraUWORDBound[1] );

      bound[i].extraFrameBound[0] = bounded_max( bound[dag[i].child[0]].extraFrameBound[0]
                                       , bound[dag[i].child[1]].extraFrameBound[0] );
      bound[i].extraFrameBound[1] = bounded_max( bound[dag[i].child[0]].extraFrameBound[1]
                                       , bound[dag[i].child[1]].extraFrameBound[1] );
      bound[i].cost = bounded_add(overhead, bounded_max( bound[dag[i].child[0]].cost
                                               , bound[dag[i].child[1]].cost ));
      break;
     case DISCONNECT:
      bound[i].extraCellsBound[1] = type_dag[DISCONNECT_W256A(dag, type_dag, i)].bitSize;
      bound[i].extraCellsBound[0] = bounded_max(
        bounded_add( type_dag[DISCONNECT_BC(dag, type_dag, i)].bitSize
                   , bounded_max( bounded_add(bound[i].extraCellsBound[1], bound[dag[i].child[0]].extraCellsBound[1])
                                , bounded_max(bound[dag[i].child[0]].extraCellsBound[0], bound[dag[i].child[1]].extraCellsBound[1]))),
        bound[dag[i].child[1]].extraCellsBound[0]);
      bound[i].extraUWORDBound[1] = (ubounded)ROUND_UWORD(type_dag[DISCONNECT_W256A(dag, type_dag, i)].bitSize);
      bound[i].extraUWORDBound[0] = bounded_max(
          (ubounded)ROUND_UWORD(type_dag[DISCONNECT_BC(dag, type_dag, i)].bitSize) +
          bounded_max( bound[i].extraUWORDBound[1] + bound[dag[i].child[0]].extraUWORDBound[1]
             , bounded_max(bound[dag[i].child[0]].extraUWORDBound[0], bound[dag[i].child[1]].extraUWORDBound[1])),
        bound[dag[i].child[1]].extraUWORDBound[0]);

      bound[i].extraFrameBound[1] = bounded_max( bound[dag[i].child[0]].extraFrameBound[1] + 1
                                       , bound[dag[i].child[1]].extraFrameBound[1]);