lambduli/README.md Secret

## README.md

      
    Raw
  

              README.md
            
          
    Transaction ISWIM

Extend State ISWIM to support transactions. Implement Transaction
ISWIM in Redex by modifying either the CS machine or the CESK machine
(your choice).
Specifically:
Add a new form of expression: (transaction M).


If M evaluates to a function, then the transaction is committed:
evaluation continues with the store from the end of the
transaction. The result of the transaction expression is that
function.


If M evaluates to a number, then the transaction is aborted: all
changes to the store since the beginning of the transaction are
undone (that is, the store is reverted to the store from from the
start of the transaction). The result of the transaction expression
is the number.


Hint: If you modify the CS machine, you may find it helpful to add
another form of expression, such as (in-transaction ???), to help
represent intermediate states in evaluation. (The original program is
not allowed to contain such expressions.) Think carefully about your
definition of evaluation contexts.
Hint: If you modify the CESK machine, think carefully about what
information must be stored in the continuation for a transaction
expression.
Examples:
(let ([a 80])
  (let ([b 20])
    (let ([adjust ;; Invariant: a + b = 100
           (λ f1
             (λ f2
               (transaction
                 (begin (set a (f1 a))
                        (set b (f2 b))
                        (if0 (+ (+ a b) -100) (λ x x) 1)))))])
      (begin ((adjust (λ a (* a 2))) (λ b (+ b -50))) ;; abort
             ((adjust (λ a (+ a -20))) (λ b (* b 2))) ;; commit
             a))))
evaluates to 60


## iswim-t.rkt
#lang racket
(require redex)

;; ----------------------------------------
;; State ISWIM

(define-language TransactionISWIM
  [(M N) B X (λ X M) (M N) (Op1 M) (Op2 M N) (if0 M N_t N_e)
         (set X M) (let ([X N]) M) (begin M N ...) (transaction M) (in-transaction M)]
  [B integer]
  [(X Y Z) variable-not-otherwise-mentioned]
  [Op Op1 Op2]
  [Op1 add1 sub1 iszero]
  [Op2 + *]

  [(V W) B (λ X M)] ;; Note: removed X
  [Answer B function]

  ;; Standard reduction:
  [E hole (E N) (V E) (Op1 E) (Op2 E N) (Op2 V E) (if0 E N_t N_e) (set X E) (in-transaction E)]

  ;; CS machine:
  [CS-config (cs M Scs RVS)]
  [RVS (RVcs ...) ()] ;; Maybe the () is not necessary?
  [RVcs ([X V] ...)]
  [Scs ((X V) ...)] ;; Store for CS machine
)

;; ----------------------------------------
;; Free variables and substitution

(define-judgment-form TransactionISWIM
  #:mode (free-in I I)
  #:contract (free-in X M)

  [---------------------------------------- "free-in-var"
   (free-in X X)]

  [(free-in X M)
   (side-condition ,(not (equal? (term X) (term Y))))
   ---------------------------------------- "free-in-λ"
   (free-in X (λ Y M))]

  [(free-in X M_1)
   ---------------------------------------- "free-in-app1"
   (free-in X (M_1 M_2))]

  [(free-in X M_2)
   ---------------------------------------- "free-in-app2"
   (free-in X (M_1 M_2))]

  [(free-in X M)
   ---------------------------------------- "free-in-op1"
   (free-in X (Op1 M))]

  [(free-in X M_1)
   ---------------------------------------- "free-in-op2-1"
   (free-in X (Op2 M_1 M_2))]

  [(free-in X M_2)
   ---------------------------------------- "free-in-op2-2"
   (free-in X (Op2 M_1 M_2))]

  [(free-in X M)
   ---------------------------------------- "free-in-if0-condition"
   (free-in X (if0 M N_t N_e))]

  [(free-in X N_t)
   ---------------------------------------- "free-in-if0-then"
   (free-in X (if0 M N_t N_e))]

  [(free-in X N_e)
   ---------------------------------------- "free-in-if0-else"
   (free-in X (if0 M N_t N_e))]

  [---------------------------------------- "free-in-set-lhs"
   (free-in X (set X M))]

  [(free-in X M)
   ---------------------------------------- "free-in-set-rhs"
   (free-in X (set Y M))]

  [(free-in X M)
   ---------------------------------------- "free-in-transaction"
   (free-in X (transaction M))]

  [(free-in X M)
   ---------------------------------------- "free-in-in-transaction"
   (free-in X (in-transaction M))]
  )

(module+ test
  (test-judgment-holds (free-in x (λ y (y x))))
  (test-equal (judgment-holds (free-in x (λ x x))) #f))

(define-metafunction TransactionISWIM
  subst : X N M -> M ;; M[X <- N]

  [(subst X N B) B]

  [(subst X N X) N]
  [(subst X N Y) Y] ;; X ≠ Y, otherwise previous case matches

  [(subst X N (λ X M))
   (λ X M)]

  ;; ** Do we still need the following case? **
  [(subst X N (λ Y M)) ;; X ≠ Y, otherwise previous case matches
   (λ Z (subst X N (subst Y Z M)))
   (judgment-holds (free-in Y N))
   (where Z ,(variable-not-in (term (X N)) (term Y)))]

  [(subst X N (λ Y M)) ;; X ≠ Y, Y ∉ FV(N), otherwise previous case matches
   (λ Y (subst X N M))]

  [(subst X N (M_1 M_2))
   ((subst X N M_1) (subst X N M_2))]

  [(subst X N (Op1 M))
   (Op1 (subst X N M))]

  [(subst X N (Op2 M_1 M_2))
   (Op2 (subst X N M_1) (subst X N M_2))]

  [(subst X N (if0 M N_t N_e))
   (if0 (subst X N M) (subst X N N_t) (subst X N N_e))]

  ; The CS machine only does variable renaming, not general substitution!
  ; We can change the rules above too.
  [(subst X Y (set X M))
   (set Y (subst X Y M))]

  [(subst X Y (set Z M)) ; Z != X
   (set Z (subst X Y M))]

  [(subst X Y (transaction M))
   (transaction (subst X Y M))]

  [(subst X Y (in-transaction M))
   (in-transaction (subst X Y M))]
  )

(module+ test
  (test-equal (term (subst x y x))
              (term y))
  (test-equal (term (subst x (λ y y) (λ z (x z))))
              (term (λ z ((λ y y) z))))
  (test-equal (term (subst x 5 (add1 (+ x (* 2 y)))))
              (term (add1 (+ 5 (* 2 y)))))
  ;; The following test depends on how variable-not-in picks the fresh
  ;; variable name (z1 in this example):
  (test-equal (term (subst x (y z) (λ z (x z))))
              (term (λ z1 ((y z) z1)))))


;; ----------------------------------------
;; Desugar

(define-metafunction TransactionISWIM
  desugar : M -> M

  [(desugar B) B]

  [(desugar X) X]

  [(desugar (λ X M)) (λ X (desugar M))]

  [(desugar (M N)) ((desugar M) (desugar N))]

  [(desugar (add1 M)) (+ (desugar M) 1)]

  [(desugar (sub1 M)) (+ (desugar M) -1)]

  [(desugar (Op1 M)) (Op1 (desugar M))]

  [(desugar (Op2 M N)) (Op2 (desugar M) (desugar N))]

  [(desugar (if0 M N_1 N_2)) (if0 (desugar M) (desugar N_1) (desugar N_2))]

  [(desugar (let ([X N]) M)) ((λ X (desugar M)) (desugar N))]

  [(desugar (iszero M)) (if0 (desugar M) (λ t (λ f t)) (λ t (λ f f)))]

  [(desugar (begin M)) (desugar M)]

  [(desugar (begin M N ...))
   ((λ Z (desugar (begin N ...))) (desugar M))
   (where Z ,(variable-not-in (term (N ...)) '_))]

  [(desugar (set X M)) (set X (desugar M))]

  [(desugar (transaction M)) (transaction (desugar M))]
)


;; ----------------------------------------
;; Reduction

(define delta
  (reduction-relation
   TransactionISWIM
   (--> (add1 B) ,(add1 (term B)))
   (--> (sub1 B) ,(sub1 (term B)))
   (--> (iszero 0) (λ x (λ y x)))
   (--> (iszero B) (λ x (λ y y)) (side-condition (not (zero? (term B)))))
   (--> (+ B_1 B_2) ,(+ (term B_1) (term B_2)))
   (--> (* B_1 B_2) ,(* (term B_1) (term B_2)))))

(define delta-if
  (reduction-relation
   TransactionISWIM
   (--> (if0 0 N_t N_e) N_t)
   (--> (if0 B N_t N_e) N_e (side-condition (not (zero? (term B)))))))

;; ----------------------------------------
;; CS machine

(define-metafunction TransactionISWIM
  store-lookup-cs : Scs X -> V
  [(store-lookup-cs ((X V) (Y W) ...) X) V]
  [(store-lookup-cs ((Z V) (Y W) ...) X) (store-lookup-cs ((Y W) ...) X)])

(define-metafunction TransactionISWIM
  store-update/add-cs : Scs X W -> Scs
  [(store-update/add-cs () X W) ((X W))]
  [(store-update/add-cs ((X V) (X_1 V_1) ...) X W) ((X W) (X_1 V_1) ...)]
  [(store-update/add-cs ((Z V) (X_1 V_1) ...) X W)
   ((Z V) (X_2 V_2) ...)
   (where ((X_2 V_2) ...) (store-update/add-cs ((X_1 V_1) ...) X W))])


(define-metafunction TransactionISWIM
  restore-vec-add : RVcs Y_y V_y -> RVcs
  [(restore-vec-add () Y V) ([Y V])]
  [(restore-vec-add ([X_x V_x] ...) Y_y V_y) ([Y_y V_y] [X_x V_x] ...)])

(define-metafunction TransactionISWIM
  store-revert : RVcs Scs -> Scs
  [(store-revert () Scs) Scs]
  [(store-revert ([X V] [Y W] ...) Scs) (store-revert ([Y W] ...) Scs_x)
   (where Scs_x (store-update/add-cs Scs X V))])


(module+ test
  (test-equal (term (store-lookup-cs ((x 1) (y 2)) x)) 1)
  (test-equal (term (store-lookup-cs ((x 1) (y 2)) y)) 2)
  (test-equal (term (store-update/add-cs ((x 1) (y 2)) x 5)) (term ((x 5) (y 2))))
  (test-equal (term (store-update/add-cs ((x 1) (y 2)) y 5)) (term ((x 1) (y 5))))
  (test-equal (term (store-update/add-cs ((x 1) (y 2)) z 5)) (term ((x 1) (y 2) (z 5)))))


(define :-->cs
  (reduction-relation
   TransactionISWIM
   #:domain CS-config
   (--> (cs (in-hole E ((λ X M) V)) Scs RVS)
        (cs (in-hole E M_1) (store-update/add-cs Scs Y V) RVS)
        (where Y ,(variable-not-in (term (cs (in-hole E ((λ X M) V)) Scs)) '_var_))
        (where M_1 (subst X Y M)))

   (--> (cs (in-hole E (Op B ...)) Scs RVS)
        (cs (in-hole E V) Scs RVS)
        (where (V) ,(apply-reduction-relation delta (term (Op B ...)))))

   (--> (cs (in-hole E X) Scs RVS)
        (cs (in-hole E V) Scs RVS)
        (where V (store-lookup-cs Scs X)))

   (--> (cs (in-hole E (if0 V N_t N_e)) Scs RVS)
        (cs (in-hole E M) Scs RVS)
        (where (M) ,(apply-reduction-relation delta-if (term (if0 V N_t N_e)))))

   ; TODO: modify set
   ; wrapped in at least one (in-transaction ...) expression -> update RVS
   (--> (cs (in-hole E (set X V)) Scs (RVcs_1 RVcs ...))
        (cs (in-hole E 0) Scs_1 (RVcs_2 RVcs ...))
        (where W (store-lookup-cs Scs X))
        (where RVcs_2 (restore-vec-add RVcs_1 X W))
        (where Scs_1 (store-update/add-cs Scs X V)))

   ; not wrapped in any (in-transaction ...) expression -> ignoring RVS
   (--> (cs (in-hole E (set X V)) Scs ())
        (cs (in-hole E 0) Scs_1 ())
        (where W (store-lookup-cs Scs X))
        (where Scs_1 (store-update/add-cs Scs X V)))

   ; initiate the transaction
   (--> (cs (in-hole E (transaction M)) Scs (RVcs ...))
        (cs (in-hole E (in-transaction M)) Scs (() RVcs ...)))

   ; transaction failed -> revert back the store and pop the RVcs stack
   (--> (cs (in-hole E (in-transaction B)) Scs (RVcs_1 RVcs ...))
        (cs (in-hole E B) (store-revert RVcs_1 Scs) (RVcs ...)))

   ; transaction successful -> pop the RVcs stack and proceed
   (--> (cs (in-hole E (in-transaction (λ X M))) Scs (RVcs_1 RVcs ...))
        (cs (in-hole E (λ X M)) Scs (RVcs ...)))

  ))

(define example (term ((λ x ((λ tmp1 x) (set x (add1 x)))) 4)))
;(define example (term ((λ x ((λ tmp1 x) (set x 23))) 4)))


(define small-test-term
  (term
   (desugar
    (let ([a 1])
      (let ([b 2])
        (begin
          (transaction (begin (set a 23) (set b 42) (λ x x)))
          (+ a b)))))))

(define big-test-term
  (term
   (desugar
    (let ([a 80])
      (let ([b 20])
        (let ([adjust ;; Invariant: a + b = 100
               (λ f1
                 (λ f2
                   (transaction
                    (begin (set a (f1 a))
                           (set b (f2 b))
                           (if0 (+ (+ a b) -100) (λ x x) 1)))))])
          (begin ((adjust (λ a (* a 2))) (λ b (+ b -50))) ;; abort
                 ((adjust (λ a (+ a -20))) (λ b (* b 2))) ;; commit
                 a)))))))

(module+ test
  (test-equal
   #t
   (redex-match?
    TransactionISWIM
    (cs 60 Scs RVS)
    (car (apply-reduction-relation* :-->cs (term (cs ,big-test-term () ())))))))
	#lang racket
	(require redex)

	;; ----------------------------------------
	;; State ISWIM

	(define-language TransactionISWIM
	[(M N) B X (λ X M) (M N) (Op1 M) (Op2 M N) (if0 M N_t N_e)
	(set X M) (let ([X N]) M) (begin M N ...) (transaction M) (in-transaction M)]
	[B integer]
	[(X Y Z) variable-not-otherwise-mentioned]
	[Op Op1 Op2]
	[Op1 add1 sub1 iszero]
	[Op2 + *]

	[(V W) B (λ X M)] ;; Note: removed X
	[Answer B function]

	;; Standard reduction:
	[E hole (E N) (V E) (Op1 E) (Op2 E N) (Op2 V E) (if0 E N_t N_e) (set X E) (in-transaction E)]

	;; CS machine:
	[CS-config (cs M Scs RVS)]
	[RVS (RVcs ...) ()] ;; Maybe the () is not necessary?
	[RVcs ([X V] ...)]
	[Scs ((X V) ...)] ;; Store for CS machine
	)

	;; ----------------------------------------
	;; Free variables and substitution

	(define-judgment-form TransactionISWIM
	#:mode (free-in I I)
	#:contract (free-in X M)

	[---------------------------------------- "free-in-var"
	(free-in X X)]

	[(free-in X M)
	(side-condition ,(not (equal? (term X) (term Y))))
	---------------------------------------- "free-in-λ"
	(free-in X (λ Y M))]

	[(free-in X M_1)
	---------------------------------------- "free-in-app1"
	(free-in X (M_1 M_2))]

	[(free-in X M_2)
	---------------------------------------- "free-in-app2"
	(free-in X (M_1 M_2))]

	[(free-in X M)
	---------------------------------------- "free-in-op1"
	(free-in X (Op1 M))]

	[(free-in X M_1)
	---------------------------------------- "free-in-op2-1"
	(free-in X (Op2 M_1 M_2))]

	[(free-in X M_2)
	---------------------------------------- "free-in-op2-2"
	(free-in X (Op2 M_1 M_2))]

	[(free-in X M)
	---------------------------------------- "free-in-if0-condition"
	(free-in X (if0 M N_t N_e))]

	[(free-in X N_t)
	---------------------------------------- "free-in-if0-then"
	(free-in X (if0 M N_t N_e))]

	[(free-in X N_e)
	---------------------------------------- "free-in-if0-else"
	(free-in X (if0 M N_t N_e))]

	[---------------------------------------- "free-in-set-lhs"
	(free-in X (set X M))]

	[(free-in X M)
	---------------------------------------- "free-in-set-rhs"
	(free-in X (set Y M))]

	[(free-in X M)
	---------------------------------------- "free-in-transaction"
	(free-in X (transaction M))]

	[(free-in X M)
	---------------------------------------- "free-in-in-transaction"
	(free-in X (in-transaction M))]
	)

	(module+ test
	(test-judgment-holds (free-in x (λ y (y x))))
	(test-equal (judgment-holds (free-in x (λ x x))) #f))

	(define-metafunction TransactionISWIM
	subst : X N M -> M ;; M[X <- N]

	[(subst X N B) B]

	[(subst X N X) N]
	[(subst X N Y) Y] ;; X ≠ Y, otherwise previous case matches

	[(subst X N (λ X M))
	(λ X M)]

	;; Do we still need the following case?
	[(subst X N (λ Y M)) ;; X ≠ Y, otherwise previous case matches
	(λ Z (subst X N (subst Y Z M)))
	(judgment-holds (free-in Y N))
	(where Z ,(variable-not-in (term (X N)) (term Y)))]

	[(subst X N (λ Y M)) ;; X ≠ Y, Y ∉ FV(N), otherwise previous case matches
	(λ Y (subst X N M))]

	[(subst X N (M_1 M_2))
	((subst X N M_1) (subst X N M_2))]

	[(subst X N (Op1 M))
	(Op1 (subst X N M))]

	[(subst X N (Op2 M_1 M_2))
	(Op2 (subst X N M_1) (subst X N M_2))]

	[(subst X N (if0 M N_t N_e))
	(if0 (subst X N M) (subst X N N_t) (subst X N N_e))]

	; The CS machine only does variable renaming, not general substitution!
	; We can change the rules above too.
	[(subst X Y (set X M))
	(set Y (subst X Y M))]

	[(subst X Y (set Z M)) ; Z != X
	(set Z (subst X Y M))]

	[(subst X Y (transaction M))
	(transaction (subst X Y M))]

	[(subst X Y (in-transaction M))
	(in-transaction (subst X Y M))]
	)

	(module+ test
	(test-equal (term (subst x y x))
	(term y))
	(test-equal (term (subst x (λ y y) (λ z (x z))))
	(term (λ z ((λ y y) z))))
	(test-equal (term (subst x 5 (add1 (+ x (* 2 y)))))
	(term (add1 (+ 5 (* 2 y)))))
	;; The following test depends on how variable-not-in picks the fresh
	;; variable name (z1 in this example):
	(test-equal (term (subst x (y z) (λ z (x z))))
	(term (λ z1 ((y z) z1)))))


	;; ----------------------------------------
	;; Desugar

	(define-metafunction TransactionISWIM
	desugar : M -> M

	[(desugar B) B]

	[(desugar X) X]

	[(desugar (λ X M)) (λ X (desugar M))]

	[(desugar (M N)) ((desugar M) (desugar N))]

	[(desugar (add1 M)) (+ (desugar M) 1)]

	[(desugar (sub1 M)) (+ (desugar M) -1)]

	[(desugar (Op1 M)) (Op1 (desugar M))]

	[(desugar (Op2 M N)) (Op2 (desugar M) (desugar N))]

	[(desugar (if0 M N_1 N_2)) (if0 (desugar M) (desugar N_1) (desugar N_2))]

	[(desugar (let ([X N]) M)) ((λ X (desugar M)) (desugar N))]

	[(desugar (iszero M)) (if0 (desugar M) (λ t (λ f t)) (λ t (λ f f)))]

	[(desugar (begin M)) (desugar M)]

	[(desugar (begin M N ...))
	((λ Z (desugar (begin N ...))) (desugar M))
	(where Z ,(variable-not-in (term (N ...)) '_))]

	[(desugar (set X M)) (set X (desugar M))]

	[(desugar (transaction M)) (transaction (desugar M))]
	)


	;; ----------------------------------------
	;; Reduction

	(define delta
	(reduction-relation
	TransactionISWIM
	(--> (add1 B) ,(add1 (term B)))
	(--> (sub1 B) ,(sub1 (term B)))
	(--> (iszero 0) (λ x (λ y x)))
	(--> (iszero B) (λ x (λ y y)) (side-condition (not (zero? (term B)))))
	(--> (+ B_1 B_2) ,(+ (term B_1) (term B_2)))
	(--> (* B_1 B_2) ,(* (term B_1) (term B_2)))))

	(define delta-if
	(reduction-relation
	TransactionISWIM
	(--> (if0 0 N_t N_e) N_t)
	(--> (if0 B N_t N_e) N_e (side-condition (not (zero? (term B)))))))

	;; ----------------------------------------
	;; CS machine

	(define-metafunction TransactionISWIM
	store-lookup-cs : Scs X -> V
	[(store-lookup-cs ((X V) (Y W) ...) X) V]
	[(store-lookup-cs ((Z V) (Y W) ...) X) (store-lookup-cs ((Y W) ...) X)])

	(define-metafunction TransactionISWIM
	store-update/add-cs : Scs X W -> Scs
	[(store-update/add-cs () X W) ((X W))]
	[(store-update/add-cs ((X V) (X_1 V_1) ...) X W) ((X W) (X_1 V_1) ...)]
	[(store-update/add-cs ((Z V) (X_1 V_1) ...) X W)
	((Z V) (X_2 V_2) ...)
	(where ((X_2 V_2) ...) (store-update/add-cs ((X_1 V_1) ...) X W))])


	(define-metafunction TransactionISWIM
	restore-vec-add : RVcs Y_y V_y -> RVcs
	[(restore-vec-add () Y V) ([Y V])]
	[(restore-vec-add ([X_x V_x] ...) Y_y V_y) ([Y_y V_y] [X_x V_x] ...)])

	(define-metafunction TransactionISWIM
	store-revert : RVcs Scs -> Scs
	[(store-revert () Scs) Scs]
	[(store-revert ([X V] [Y W] ...) Scs) (store-revert ([Y W] ...) Scs_x)
	(where Scs_x (store-update/add-cs Scs X V))])


	(module+ test
	(test-equal (term (store-lookup-cs ((x 1) (y 2)) x)) 1)
	(test-equal (term (store-lookup-cs ((x 1) (y 2)) y)) 2)
	(test-equal (term (store-update/add-cs ((x 1) (y 2)) x 5)) (term ((x 5) (y 2))))
	(test-equal (term (store-update/add-cs ((x 1) (y 2)) y 5)) (term ((x 1) (y 5))))
	(test-equal (term (store-update/add-cs ((x 1) (y 2)) z 5)) (term ((x 1) (y 2) (z 5)))))


	(define :-->cs
	(reduction-relation
	TransactionISWIM
	#:domain CS-config
	(--> (cs (in-hole E ((λ X M) V)) Scs RVS)
	(cs (in-hole E M_1) (store-update/add-cs Scs Y V) RVS)
	(where Y ,(variable-not-in (term (cs (in-hole E ((λ X M) V)) Scs)) '_var_))
	(where M_1 (subst X Y M)))

	(--> (cs (in-hole E (Op B ...)) Scs RVS)
	(cs (in-hole E V) Scs RVS)
	(where (V) ,(apply-reduction-relation delta (term (Op B ...)))))

	(--> (cs (in-hole E X) Scs RVS)
	(cs (in-hole E V) Scs RVS)
	(where V (store-lookup-cs Scs X)))

	(--> (cs (in-hole E (if0 V N_t N_e)) Scs RVS)
	(cs (in-hole E M) Scs RVS)
	(where (M) ,(apply-reduction-relation delta-if (term (if0 V N_t N_e)))))

	; TODO: modify set
	; wrapped in at least one (in-transaction ...) expression -> update RVS
	(--> (cs (in-hole E (set X V)) Scs (RVcs_1 RVcs ...))
	(cs (in-hole E 0) Scs_1 (RVcs_2 RVcs ...))
	(where W (store-lookup-cs Scs X))
	(where RVcs_2 (restore-vec-add RVcs_1 X W))
	(where Scs_1 (store-update/add-cs Scs X V)))

	; not wrapped in any (in-transaction ...) expression -> ignoring RVS
	(--> (cs (in-hole E (set X V)) Scs ())
	(cs (in-hole E 0) Scs_1 ())
	(where W (store-lookup-cs Scs X))
	(where Scs_1 (store-update/add-cs Scs X V)))

	; initiate the transaction
	(--> (cs (in-hole E (transaction M)) Scs (RVcs ...))
	(cs (in-hole E (in-transaction M)) Scs (() RVcs ...)))

	; transaction failed -> revert back the store and pop the RVcs stack
	(--> (cs (in-hole E (in-transaction B)) Scs (RVcs_1 RVcs ...))
	(cs (in-hole E B) (store-revert RVcs_1 Scs) (RVcs ...)))

	; transaction successful -> pop the RVcs stack and proceed
	(--> (cs (in-hole E (in-transaction (λ X M))) Scs (RVcs_1 RVcs ...))
	(cs (in-hole E (λ X M)) Scs (RVcs ...)))

	))

	(define example (term ((λ x ((λ tmp1 x) (set x (add1 x)))) 4)))
	;(define example (term ((λ x ((λ tmp1 x) (set x 23))) 4)))



	(define small-test-term
	(term
	(desugar
	(let ([a 1])
	(let ([b 2])
	(begin
	(transaction (begin (set a 23) (set b 42) (λ x x)))
	(+ a b)))))))

	(define big-test-term
	(term
	(desugar
	(let ([a 80])
	(let ([b 20])
	(let ([adjust ;; Invariant: a + b = 100
	(λ f1
	(λ f2
	(transaction
	(begin (set a (f1 a))
	(set b (f2 b))
	(if0 (+ (+ a b) -100) (λ x x) 1)))))])
	(begin ((adjust (λ a (* a 2))) (λ b (+ b -50))) ;; abort
	((adjust (λ a (+ a -20))) (λ b (* b 2))) ;; commit
	a)))))))

	(module+ test
	(test-equal
	#t
	(redex-match?
	TransactionISWIM
	(cs 60 Scs RVS)
	(car (apply-reduction-relation* :-->cs (term (cs ,big-test-term () ())))))))