feat: scope for functions

[lorenzogentile404]

In some module, we may have shorthands (defined through functions) appearing with the same name in the spec (the scope is defined informally through the section) but defined differently based on the scope. The way we manage this is the following for now:

(defun (scope1___bla)
  [DATA 1])

(defun (scope2___bla)
  [DATA 7])

The proposed feature is the following:

(defun (bla :scope scope1)
  [DATA 1])

(defun (bla :scope scope2)
  [DATA 7])

(defconstraint c1 (:scope scope1)
  (eq! (bla) 1))

(defconstraint c2 (:scope scope2)
  (eq! (bla) 1))

In the constraints, (bla) translates to the one consistent with the scope of the constraint.

Currently, I believe we can achieve this with different files for scope, but I believe is too heavy as an approach.

[DavePearce]

Hey @lorenzogentile404, I don't really understand the proposed feature. What are you trying to achieve with this? Can you show me an example in the constraints?

[lorenzogentile404]

@DavePearce in ecdata for example we have the same shorthand (internal_checks_passed) defined in different ways in different scopes. For now I implement it this way:

(defun (internal_checks_passed)
  (+ (* (transition_to_result) HURDLE)
     (* (ecrecover-hypothesis) (shift HURDLE INDEX_MAX_ECRECOVER_DATA))
     (* (ecadd-hypothesis) (shift HURDLE INDEX_MAX_ECADD_DATA))
     (* (ecmul-hypothesis) (shift HURDLE INDEX_MAX_ECMUL_DATA))
     (* (ecpairing-hypothesis) (shift HURDLE INDEX_MAX_ECPAIRING_DATA_MIN)))) 

However, if I should exactly translate how the shorthand is currently defined in the specs, we would have:

(defun (transition_to_result___internal_checks_passed)
  (HURDLE))

(defun (ecrecover___internal_checks_passed)
  (shift HURDLE INDEX_MAX_ECRECOVER_DATA))

(defun (ecadd___internal_checks_passed)
  (shift HURDLE INDEX_MAX_ECADD_DATA))

(defun (ecmul___internal_checks_passed)
  (shift HURDLE INDEX_MAX_ECMUL_DATA))

(defun (ecpairing___internal_checks_passed)
  (shift HURDLE INDEX_MAX_ECPAIRING_DATA_MIN))

With the proposed feature we would have something like:

(defun (internal_checks_passed :scope transition_to_result)
  (HURDLE))

(defun (internal_checks_passed :scope ecrecover)
  (shift HURDLE INDEX_MAX_ECRECOVER_DATA))

(defun (internal_checks_passed :scope ecadd)
  (shift HURDLE INDEX_MAX_ECADD_DATA))

(defun (internal_checks_passed :scope ecmul)
  (shift HURDLE INDEX_MAX_ECMUL_DATA))

(defun (internal_checks_passed :scope ecpairing)
  (shift HURDLE INDEX_MAX_ECPAIRING_DATA_MIN))

That may be a cleaner solution. However, by checking the constraints better, it seems we do not have that often this need. @OlivierBBB what do you think?

[lorenzogentile404]

@DavePearce here is a clearer example from oob constraints for call and create. As you can see:

;; CALL 

(defun (call___aborting_condition)
  [DATA 8])

...

(defconstraint justify-hub-predictions-call (:guard (* (standing-hypothesis) (call-hypothesis)))
  (begin (eq! (call___value_is_nonzero) (- 1 (call___value_is_zero)))
         (eq! (call___aborting_condition)
              (+ (call___insufficient_balance_abort)
                 (* (- 1 (call___insufficient_balance_abort)) (call___call_stack_depth_abort))))))

;;  CREATE

(defun (create___aborting_condition)
  [DATA 7])

...

(defconstraint justify-hub-predictions-create (:guard (* (standing-hypothesis) (create-hypothesis)))
  (begin (eq! (create___aborting_condition)
              (+ (create___insufficient_balance_abort)
                 (* (- 1 (create___insufficient_balance_abort)) (create___stack_depth_abort))))
         (eq! (create___failure_condition)
              (* (- 1 (create___aborting_condition))
                 (+ (create___has_code)
                    (* (- 1 (create___has_code)) (create___nonzero_nonce)))))))

With the proposed feature we would have something like:

;; CALL 

(defun (aborting_condition :scope call)
  [DATA 8])

...

(defconstraint justify-hub-predictions-call (:scope call :guard (* (standing-hypothesis) (call-hypothesis)))
  (begin (eq! (call___value_is_nonzero) (- 1 (call___value_is_zero)))
         (eq! (aborting_condition)
              (+ (call___insufficient_balance_abort)
                 (* (- 1 (call___insufficient_balance_abort)) (call___call_stack_depth_abort))))))

;;  CREATE

(defun (aborting_condition :scope create)
  [DATA 7])

...

(defconstraint justify-hub-predictions-create (:scope create :guard (* (standing-hypothesis) (create-hypothesis)))
  (begin (eq! (aborting_condition)
              (+ (create___insufficient_balance_abort)
                 (* (- 1 (create___insufficient_balance_abort)) (create___stack_depth_abort))))
         (eq! (create___failure_condition)
              (* (- 1 (create___aborting_condition))
                 (+ (create___has_code)
                    (* (- 1 (create___has_code)) (create___nonzero_nonce)))))))

and similarly, for the other shorthands we may avoid call___ and create___ prefixes.

[lorenzogentile404]

@DavePearce, an ever cleaner approach may be the possibility to create "submodules" within the same file, that may look like this:

(module oob)

;; global shorthand
(defun (flag_sum)
  (+ (flag_sum_inst) (flag_sum_prc)))

// call submodule
(oob.call

// local shorthand
(defun (aborting_condition)
  [DATA 8])

...

(defconstraint justify-hub-predictions-call (:guard (* (standing-hypothesis) (call-hypothesis)))
  (begin (eq! (aborting_condition) ...))

)

// create submodule
(oob.create

// local shorthand
(defun (aborting_condition)
  [DATA 7])

...

(defconstraint justify-hub-predictions-create (:guard (* (standing-hypothesis) (create-hypothesis)))
  (begin (eq! (aborting_condition) ...))
)

Potentially, submodules may be also nested.

[lorenzogentile404]

It seems with the current modules system you can already do something similar, but I am not sure how this would reflect in the definition of the modules (for example, oob should be identified as the oob module plus all its submodules) and if you can do exactly what I have in mind. @delehef any input on this would be much appreciated. Also, there is no possibility to create nested modules (but we probably do not even need that feature).

[delehef]

Why don't you create a local binding? Something like:

(defconstraint justify-hub-predictions-call (:guard (* (standing-hypothesis) (call-hypothesis)))
  (let ((aborting-condition [DATA 8]))
      (begin (eq! (call___value_is_nonzero) (- 1 (call___value_is_zero)))
             (eq! aborting-condition
                  (+ (call___insufficient_balance_abort)
                     (* (- 1 (call___insufficient_balance_abort)) (call___call_stack_depth_abort)))))))

To go further:

(defconstraint justify-hub-predictions-call (:guard (* (standing-hypothesis) (call-hypothesis)))
  (let ((aborting-condition [DATA 8])
        (value-is-non-zero (...))
        (value-is-zero (...))
        (insufficient-balance-abort (...))
        (call-stack-depth-abort (...)))
      (begin (eq! value-is-nonzero (- 1 value-is-zero))
             (eq! aborting-condition
                  (+ insufficient-balance-abort
                     (* (- 1 insufficient-balance-abort) call-stack-depth-abort))))))

[lorenzogentile404]

@delehef interesting. I did not know Corset preserved this feature of Lisp. This would work, but I could use these shorthands only inside justify-hub-predictions-call and sometimes I may need to use the same "local" shorthand inside more than one constraint.

A workaround may be creating a single huge constraint with let at the top and then a begin block. However, this would not be ideal for debugging and making code modular.

[delehef]

Or just have one let in each constraint.

[lorenzogentile404]

But then it would mean repeating the definitions every time?

[lorenzogentile404]

@DavePearce I had a conversation about this feature with @OlivierBBB and it may be helpful especially in the hub, he mentioned.

[delehef]

it would mean repeating the definitions every time?

Probably better on the long term w.r.t. maintainability to have a couple copy-paste than to contort into the language a feature used in a very specific use-case in a single module, but @DavePearce may be of an other opinion.

[lorenzogentile404]

Actually, we may have nested scopes too, but we would need a way to clearly indicate, in debugging phase, which group of constraints is failing (i.e., showing the name). However, the syntax looks heavy:

(defconstraint constraints-groups ()
  (let ((globalshorthand1 [DATA 1])             ;; global scope
        (globalshorthand2 [DATA 2]))
       (begin (let ((constraints-group-n 1)     ;; this is just to idenity the group of constraints number 1
                    (localshorthand1 [DATA 5])
                    (localshorthand2 [DATA 6])) ;; local scope 1
                   (begin (eq! localshorthand1 globalshorthand1)
                          (eq! localshorthand2 globalshorthand2)))
              (let ((constraint-group-n 2)      ;; this is just to idenity the group of constraints number 2
                    (localshorthand1 [DATA 7])
                    (localshorthand2 [DATA 8])) ;; local scope 2 (localshorthand1 and localshorthand2 are redefined here)
                   (begin (eq! localshorthand1 globalshorthand1)
                          (eq! localshorthand2 globalshorthand2))))))

[delehef]

The simplest solution would probably be to split the begin in two defconstraint, then copy-paste the required let in each.

[DavePearce]

Hi @lorenzogentile404, ok lots of ideas here. Right now, we need to stick to something simple. I think I understand roughly what you're looking for. This is really just a notational convenience.

This I would avoid:

(module oob)

(defun (aborting_condition) [DATA 8])

// create submodule
(module oob.create)

(defun (aborting_condition) [DATA 7])

This is not a great idea. Allowing an item with the same name to override another is hazardous. Programming languages normally avoid this. One way around this would be to allow items with the same name in different submodules like this:

(module oob)

(submodule oob.call)
(defun (aborting_condition) [DATA 8])

(submodule oob.create)
(defun (aborting_condition) [DATA 7])

I think this would be sufficient for your case. Maybe even a term like namespace is better than submodule.