Synergy in Scheme

The Safe

Here is the simplest addition to Scheme I know that provides efficient synergy. The safe is a new primitive type like the cons cell except there is neither car nor cdr for it. make-safe is a new primitive procedure like cons except it produces a safe instead of a cons cell. There is an op extract of two arguments. The following is always true:
(eq? (extract a (make-safe a b)) b)
(extract c (make-safe a b)) yields #f unless (eq? a c).
In other symbols the following yields true for any values of the variables, a, b:

(and (eq? (extract a (make-safe a b)) b)
     (or (not (extract b (make-safe a 42))) (eq? a b)))

The holder of a lock is able to extract the content from any safe with that lock that he finds. I declare for now that (extract a b) yields false if b is not a safe. This is contrary to Scheme style but otherwise we need a safe? predicate and users must write extra code. I am not aware of an objection to another primitive to modify the 2nd ½ of a safe but I think it is not much needed.

I discuss another pattern, called the sealer-unsealer, here. Both these proposed primitives support the other synergy patterns and each other efficiently as well.

The following defines make-safe and extract in terms of new-seal.

(define ctool (let ((s (new-seal)))
  (let ((seal (car s)) (unseal (cadr s)) (sealed? (caddr s)))
    (let ((make-safe (lambda (a b) (seal (cons a b))))
          (extract (lambda (b p) (and (sealed? p) (let ((c (unseal p)))
             (and (eq? (car c) b) (cdr c)))))))
    (cons make-safe extract)))))
(define make-safe (car ctool))
(define extract (cdr ctool))

The following defines eq? in terms of make-safe and extract:

(define (eq? a b) (extract b (make-safe a #t)))

We have now the following cyclic set of reductions:

make-safe and extract ⇛ eq?
eq? ⇛ new-seal
new-seal ⇛ make-safe and extract

The following defines new-seal in terms of make-safe and extract:

(define (new-seal) (let ((S (cons '() '()))) (list
   (lambda (rep) (make-safe S rep))
   (lambda (abs) (let ((probe (extract abs))) (or probe (error "invalid argument" abs))))
   (lambda (x) (not (not (extract x))))))) ; => (seal unseal sealed?)

Safe vs. Sealer

These primitive sets are of nearly equivalent complexity. Both are presumably easy to implement. Here are the differences I see:

The sealer has been widely discussed. The safe appeared as the domain’s brand in Keykos.
The safe apparatus must expend some uniquely generated object, such as a cons cell, to lock a variety of safes. Perhaps the sealer need not, but it might then need extra logic to recycle the required internal IDs.
The safe calls for two new primitives functions, where the sealer calls for three. I think, however, that either the Safe needs a predicate safe? or the sealer can dispense with sealed?. Which is a philosophical issue I think.

No New Primitive Needed?

Not quite. I add this in 2012, Jan.

The following would seem, at first, to be a slight modification and simplification to the safe, which is trivially implemented in current Scheme!

(define (make-safe a b) (lambda (x) (and (eq? x a) b)))

The modified Guttag definition is:
for arbitrary Scheme values a, b and x:

(let ((s (make-safe a b))) (and (eq? (s a) b) (or (not (s x)) (eq? a x)))) => #t

A problem with this must be overcome! How does the legitimate holder of the brand know that a value of uncertain provenance is confined? Perhaps it is instead (lambda (x) (set! y x)) where y is some variable in scope of the perpetrator who is attempting to open thereby safes not meant for him.

A Scheme value is a pair of behavior and state. If the behavior could be ascertained by the holder this problem would be solved. That breaks other security properties however. If it could be ascertained that the behavior was specifically “(lambda (x) (and (eq? x _) _))” then that too would solve the problem. Even that is dangerous.