Payable specifier and call by callvalue

src/contract.md

@@ -11,13 +11,14 @@ module SOLIDITY-CONTRACT
          ...
        </contracts>
 
-  rule <k> function X ( Params ) V:VisibilitySpecifier { Body } => .K ...</k>
+  rule <k> function X ( Params ) F:FunctionSpecifiers { Body } => .K ...</k>
        <current-body> C </current-body>
        <contract-id> C </contract-id>
        <contract-fns>
          .Bag => <contract-fn>
                    <contract-fn-id> X </contract-fn-id>
-                   <contract-fn-visibility> V </contract-fn-visibility>
+                   <contract-fn-visibility> getVisibility(F) </contract-fn-visibility>
+                   <contract-fn-payable> getPayable(F) </contract-fn-payable>
                    <contract-fn-arg-types> getTypes(Params) </contract-fn-arg-types>
                    <contract-fn-param-names> getNames(Params) </contract-fn-param-names>
                    <contract-fn-body> Body </contract-fn-body>
@@ -26,13 +27,14 @@ module SOLIDITY-CONTRACT
          ...
        </contract-fns>
 
-  rule <k> function X ( Params ) V:VisibilitySpecifier returns ( Rets ) { Body } => .K ...</k>
+  rule <k> function X ( Params ) F:FunctionSpecifiers returns ( Rets ) { Body } => .K ...</k>
        <current-body> C </current-body>
        <contract-id> C </contract-id>
        <contract-fns>
          .Bag => <contract-fn>
                    <contract-fn-id> X </contract-fn-id>
-                   <contract-fn-visibility> V </contract-fn-visibility>
+                   <contract-fn-visibility> getVisibility(F) </contract-fn-visibility>
+                   <contract-fn-payable> getPayable(F) </contract-fn-payable>
                    <contract-fn-arg-types> getTypes(Params) </contract-fn-arg-types>
                    <contract-fn-param-names> getNames(Params) </contract-fn-param-names>
                    <contract-fn-return-types> getTypes(Rets) </contract-fn-return-types>
@@ -43,6 +45,18 @@ module SOLIDITY-CONTRACT
          ...
        </contract-fns>
 
+  syntax VisibilitySpecifier ::= getVisibility(FunctionSpecifiers) [function]
+  rule getVisibility(private _) => private
+  rule getVisibility(public _) => public
+  rule getVisibility(external _) => external
+  rule getVisibility(internal _) => internal
+  rule getVisibility(_ F) => getVisibility(F) [owise]
+
+  syntax Bool ::= getPayable(FunctionSpecifiers) [function]
+  rule getPayable(.FunctionSpecifiers) => false
+  rule getPayable(payable _) => true
+  rule getPayable(_ F) => getPayable(F) [owise]
+
   rule <k> constructor ( Params ) { Body } => .K ...</k>
        <current-body> C </current-body>
        <contract-id> C </contract-id>

src/expression.md

@@ -9,11 +9,12 @@ module SOLIDITY-EXPRESSION
   // new contract
   rule <k> new X:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ~> return v(ADDR, X) ; </k>
        <msg-sender> FROM => THIS </msg-sender>
+       <msg-value> VALUE => 0p256 </msg-value>
        <this> THIS => ADDR </this>
        <this-type> TYPE => X </this-type>
        <env> E => .Map </env>
        <store> S => .Map </store>
-       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE)) </call-stack>
+       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> X </contract-id>
        <contract-init> INIT </contract-init>
        <contract-fn-id> constructor </contract-fn-id>
@@ -33,11 +34,12 @@ module SOLIDITY-EXPRESSION
 
   rule <k> new X:Id ( .TypedVals ) ~> K => List2Statements(INIT) ~> return v(ADDR, X) ; </k>
        <msg-sender> FROM => THIS </msg-sender>
+       <msg-value> VALUE => 0p256 </msg-value>
        <this> THIS => ADDR </this>
        <this-type> TYPE => X </this-type>
        <env> E => .Map </env>
        <store> S => .Map </store>
-       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE)) </call-stack>
+       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> X </contract-id>
        <contract-init> INIT </contract-init>
        <live-contracts>
@@ -107,11 +109,12 @@ module SOLIDITY-EXPRESSION
   context (_ . _) ( HOLE:CallArgumentList )
   rule <k> v(ADDR, TYPE') . F:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
        <msg-sender> FROM => THIS </msg-sender>
+       <msg-value> VALUE => 0p256 </msg-value>
        <this> THIS => ADDR </this>
        <this-type> TYPE => TYPE' </this-type>
        <env> E => .Map </env>
        <store> S => .Map </store>
-       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE)) </call-stack>
+       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> TYPE' </contract-id>
        <contract-fn-id> F </contract-fn-id>
        <contract-fn-param-names> PARAMS </contract-fn-param-names>
@@ -123,13 +126,40 @@ module SOLIDITY-EXPRESSION
        <contract-type> TYPE' </contract-type>
     requires isKResult(ARGS)
 
+  syntax Id ::= "value" [token]
+
+  context HOLE . _ { value: _ } ( _ )
+  context _ . _ { value: HOLE } ( _ )
+  context _ . _ { _ } ( HOLE:CallArgumentList )
+
+  rule <k> v(ADDR, TYPE') . F:Id { value: v(VALUE', uint256) } ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
+       <msg-sender> FROM => THIS </msg-sender>
+       <msg-value> VALUE => VALUE' </msg-value>
+       <this> THIS => ADDR </this>
+       <this-type> TYPE => TYPE' </this-type>
+       <env> E => .Map </env>
+       <store> S => .Map </store>
+       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
+       <contract-id> TYPE' </contract-id>
+       <contract-fn-id> F </contract-fn-id>
+       <contract-fn-payable> PAYABLE </contract-fn-payable>
+       <contract-fn-param-names> PARAMS </contract-fn-param-names>
+       <contract-fn-arg-types> TYPES </contract-fn-arg-types>
+       <contract-fn-return-types> RETTYPES </contract-fn-return-types>
+       <contract-fn-return-names> RETNAMES </contract-fn-return-names>
+       <contract-fn-body> BODY </contract-fn-body>
+       <contract-address> ADDR </contract-address>
+       <contract-type> TYPE' </contract-type>
+    requires isKResult(ARGS) andBool (PAYABLE orBool VALUE' ==MInt 0p256)
+
   // internal call
   rule <k> F:Id ( ARGS ) ~> K => bind(PARAMS, TYPES, ARGS, RETTYPES, RETNAMES) ~> BODY ~> return retval(RETNAMES); </k>
        <msg-sender> FROM </msg-sender>
+       <msg-value> VALUE </msg-value>
        <this-type> TYPE </this-type>
        <env> E => .Map </env>
        <store> S => .Map </store>
-       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE)) </call-stack>
+       <call-stack>... .List => ListItem(frame(K, E, S, FROM, TYPE, VALUE)) </call-stack>
        <contract-id> TYPE </contract-id>
        <contract-fn-id> F </contract-fn-id>
        <contract-fn-param-names> PARAMS </contract-fn-param-names>
@@ -145,6 +175,21 @@ module SOLIDITY-EXPRESSION
   // integer literal
   rule N:NumberLiteral => Number2Int(N)
 
+  // automatic variables
+  syntax Id ::= "msg" [token] | "sender" [token] | "this" [token] | "tx" [token] | "origin" [token] | "block" [token] | "timestamp" [token]
+
+  rule <k> (msg . sender)::Expression => v(FROM, address) ...</k>
+       <msg-sender> FROM </msg-sender>
+  rule <k> (msg . value)::Expression => v(VALUE, uint) ...</k>
+       <msg-value> VALUE </msg-value>
+  rule <k> this => v(THIS, TYPE) ...</k>
+       <this> THIS </this>
+       <this-type> TYPE </this-type>
+  rule <k> (tx . origin)::Expression => v(ORIGIN, address) ...</k>
+       <tx-origin> ORIGIN </tx-origin>
+  rule <k> (block . timestamp)::Expression => v(NOW, uint) ...</k>
+       <block-timestamp> NOW </block-timestamp>
+
   // basic arithmetic
   rule v(V1:Value, T)  + v(V2:Value, T) => v(add(V1, V2), T)
   rule v(V1:Value, T)  - v(V2:Value, T) => v(sub(V1, V2), T)

src/solidity.md

@@ -43,6 +43,7 @@ module SOLIDITY-CONFIGURATION
               <contract-fn-param-names> .List </contract-fn-param-names>
               <contract-fn-return-types> .List </contract-fn-return-types>
               <contract-fn-return-names> .List </contract-fn-return-names>
+              <contract-fn-payable> false </contract-fn-payable>
               <contract-fn-body> .Statements </contract-fn-body>
             </contract-fn>
           </contract-fns>
@@ -60,6 +61,7 @@ module SOLIDITY-CONFIGURATION
         <msg-sender> 0p160 </msg-sender>
         <msg-value> 0p256 </msg-value>
         <tx-origin> 0p160 </tx-origin>
+        <block-timestamp> 0p256 </block-timestamp>
         <this> 0p160 </this>
         <this-type> Id </this-type>
         <env> .Map </env>
@@ -93,8 +95,8 @@ module SOLIDITY-DATA-SYNTAX
   syntax MInt{256}
 
   syntax Transactions ::= List{Transaction, ","}
-  syntax Transaction ::= txn(from: Decimal, to: Decimal, value: Decimal, func: Id, args: CallArgumentList) [function]
-  syntax Transaction ::= create(from: Decimal, value: Decimal, ctor: Id, args: CallArgumentList) [strict(4)]
+  syntax Transaction ::= txn(from: Decimal, to: Decimal, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) [function]
+  syntax Transaction ::= create(from: Decimal, value: Decimal, timestamp: Decimal, ctor: Id, args: CallArgumentList) [strict(5)]
 endmodule
 
 module SOLIDITY-DATA
@@ -157,7 +159,7 @@ module SOLIDITY-DATA
   rule getIndexed(_:TypeName indexed, Ep:EventParameters, N:Int) => SetItem(N) getIndexed(Ep, N +Int 1)
   rule getIndexed(_, Ep:EventParameters, N:Int) => getIndexed(Ep, N +Int 1) [owise]
 
-  syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id)
+  syntax Frame ::= frame(continuation: K, env: Map, store: Map, from: MInt{160}, type: Id, value: MInt{256})
   syntax Event ::= event(name: Id, args: TypedVals)
 
 endmodule

src/statement.md

@@ -12,11 +12,12 @@ module SOLIDITY-STATEMENT
   // return statement
   rule <k> return V:TypedVal ; ~> _ => V ~> K </k>
        <msg-sender> THIS => FROM </msg-sender>
+       <msg-value> _ => VALUE </msg-value>
        <this> _ => THIS </this>
        <this-type> _ => TYPE </this-type>
        <env> _ => E </env>
        <store> _ => S </store>
-       <call-stack>... ListItem(frame(K, E, S, FROM, TYPE)) => .List </call-stack>
+       <call-stack>... ListItem(frame(K, E, S, FROM, TYPE, VALUE)) => .List </call-stack>
 
   // variable declaration
   rule <k> LT:TypeName X:Id = v(V, RT) ; => .K ...</k>

src/transaction.md

@@ -7,10 +7,11 @@ module SOLIDITY-TRANSACTION
   imports INT
   imports private SOLIDITY-EXPRESSION
 
-  rule <k> create(FROM, VALUE, CTOR, ARGS) => bind(PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
+  rule <k> create(FROM, VALUE, NOW, CTOR, ARGS) => bind(PARAMS, TYPES, ARGS, .List, .List) ~> List2Statements(INIT) ~> BODY ...</k>
        <msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
        <msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
        <tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
+       <block-timestamp> _ => Int2MInt(Number2Int(NOW)) </block-timestamp>
        <this> _ => ADDR </this>
        <this-type> _ => CTOR </this-type>
        <env> _ => .Map </env>
@@ -32,10 +33,11 @@ module SOLIDITY-TRANSACTION
        <next-address> ADDR => ADDR +MInt 1p160 </next-address>
     requires isKResult(ARGS)
 
-  rule <k> create(FROM, VALUE, CTOR, .TypedVals) => List2Statements(INIT) ...</k>
+  rule <k> create(FROM, VALUE, NOW, CTOR, .TypedVals) => List2Statements(INIT) ...</k>
        <msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
        <msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
        <tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
+       <block-timestamp> _ => Int2MInt(Number2Int(NOW)) </block-timestamp>
        <this> _ => ADDR </this>
        <this-type> _ => CTOR </this-type>
        <env> _ => .Map </env>
@@ -53,13 +55,14 @@ module SOLIDITY-TRANSACTION
        <next-address> ADDR => ADDR +MInt 1p160 </next-address>
     [owise]
 
-  syntax Transaction ::= txn(from: Decimal, to: MInt{160}, value: Decimal, func: Id, args: CallArgumentList) [strict(5)]
-  rule txn(FROM, TO, VALUE, FUNC, ARGS) => txn(FROM, Int2MInt(Number2Int(TO)), VALUE, FUNC, ARGS)
+  syntax Transaction ::= txn(from: Decimal, to: MInt{160}, value: Decimal, timestamp: Decimal, func: Id, args: CallArgumentList) [strict(6)]
+  rule txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => txn(FROM, Int2MInt(Number2Int(TO)), VALUE, NOW, FUNC, ARGS)
 
-  rule <k> txn(FROM, TO, VALUE, FUNC, ARGS) => bind(PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
+  rule <k> txn(FROM, TO, VALUE, NOW, FUNC, ARGS) => bind(PARAMS, TYPES, ARGS, .List, .List) ~> BODY ...</k>
        <msg-sender> _ => Int2MInt(Number2Int(FROM)) </msg-sender>
        <msg-value> _ => Int2MInt(Number2Int(VALUE)) </msg-value>
        <tx-origin> _ => Int2MInt(Number2Int(FROM)) </tx-origin>
+       <block-timestamp> _ => Int2MInt(Number2Int(NOW)) </block-timestamp>
        <this> _ => TO </this>
        <this-type> _ => TYPE </this-type>
        <env> _ => .Map </env>

test/regression/arithmetic.ref

@@ -39,6 +39,9 @@
           <contract-fn-return-names>
             .List
           </contract-fn-return-names>
+          <contract-fn-payable>
+            false
+          </contract-fn-payable>
           <contract-fn-body>
             uint8 i8_1 = 2 ;  uint8 i8_2 = 2 ;  uint8 i32_1 = 2 ;  uint8 i32_2 = 2 ;  uint8 i112_1 = 2 ;  uint8 i112_2 = 2 ;  uint8 i256_1 = 2 ;  uint8 i256_2 = 2 ;  require ( i8_1 + i8_2 == 4 , "" , .TypedVals ) ;  require ( i32_1 + i32_2 == 4 , "" , .TypedVals ) ;  require ( i112_1 + i112_2 == 4 , "" , .TypedVals ) ;  require ( i256_1 + i256_2 == 4 , "" , .TypedVals ) ;  require ( i8_1 + 2 == 4 , "" , .TypedVals ) ;  require ( 2 + i8_2 == 4 , "" , .TypedVals ) ;  require ( 2 + 2 == 4 , "" , .TypedVals ) ;  require ( i8_1 - i8_2 == 0 , "" , .TypedVals ) ;  require ( i32_1 - i32_2 == 0 , "" , .TypedVals ) ;  require ( i112_1 - i112_2 == 0 , "" , .TypedVals ) ;  require ( i256_1 - i256_2 == 0 , "" , .TypedVals ) ;  require ( i8_1 - 2 == 0 , "" , .TypedVals ) ;  require ( 2 - i8_2 == 0 , "" , .TypedVals ) ;  require ( 2 - 2 == 0 , "" , .TypedVals ) ;  require ( i8_1 * i8_2 == 4 , "" , .TypedVals ) ;  require ( i32_1 * i32_2 == 4 , "" , .TypedVals ) ;  require ( i112_1 * i112_2 == 4 , "" , .TypedVals ) ;  require ( i256_1 * i256_2 == 4 , "" , .TypedVals ) ;  require ( i8_1 * 2 == 4 , "" , .TypedVals ) ;  require ( 2 * i8_2 == 4 , "" , .TypedVals ) ;  require ( 2 * 2 == 4 , "" , .TypedVals ) ;  require ( i8_1 / i8_2 == 1 , "" , .TypedVals ) ;  require ( i32_1 / i32_2 == 1 , "" , .TypedVals ) ;  require ( i112_1 / i112_2 == 1 , "" , .TypedVals ) ;  require ( i256_1 / i256_2 == 1 , "" , .TypedVals ) ;  require ( i8_1 / 2 == 1 , "" , .TypedVals ) ;  require ( 2 / i8_2 == 1 , "" , .TypedVals ) ;  require ( 2 / 2 == 1 , "" , .TypedVals ) ;  require ( i8_1 == i8_2 , "" , .TypedVals ) ;  require ( i32_1 == i32_2 , "" , .TypedVals ) ;  require ( i112_1 == i112_2 , "" , .TypedVals ) ;  require ( i256_1 == i256_2 , "" , .TypedVals ) ;  require ( 2 == i8_2 , "" , .TypedVals ) ;  require ( 2 == 2 , "" , .TypedVals ) ;  require ( i8_1 <= i8_2 , "" , .TypedVals ) ;  require ( i32_1 <= i32_2 , "" , .TypedVals ) ;  require ( i112_1 <= i112_2 , "" , .TypedVals ) ;  require ( i256_1 <= i256_2 , "" , .TypedVals ) ;  require ( i8_1 <= 2 , "" , .TypedVals ) ;  require ( 2 <= i8_2 , "" , .TypedVals ) ;  require ( 2 <= 2 , "" , .TypedVals ) ;  require ( i8_1 >= i8_2 , "" , .TypedVals ) ;  require ( i32_1 >= i32_2 , "" , .TypedVals ) ;  require ( i112_1 >= i112_2 , "" , .TypedVals ) ;  require ( i256_1 >= i256_2 , "" , .TypedVals ) ;  require ( i8_1 >= 2 , "" , .TypedVals ) ;  require ( 2 >= i8_2 , "" , .TypedVals ) ;  require ( 2 >= 2 , "" , .TypedVals ) ;  i8_2 = 4 ;  i32_2 = 4 ;  i112_2 = 4 ;  i256_2 = 4 ;  require ( i8_1 ** i8_2 == 16 , "" , .TypedVals ) ;  require ( i32_1 ** i32_2 == 16 , "" , .TypedVals ) ;  require ( i112_1 ** i112_2 == 16 , "" , .TypedVals ) ;  require ( i256_1 ** i256_2 == 16 , "" , .TypedVals ) ;  require ( i8_1 ** 4 == 16 , "" , .TypedVals ) ;  require ( 2 ** i8_2 == 16 , "" , .TypedVals ) ;  require ( 2 ** 4 == 16 , "" , .TypedVals ) ;  require ( i8_1 < i8_2 , "" , .TypedVals ) ;  require ( i32_1 < i32_2 , "" , .TypedVals ) ;  require ( i112_1 < i112_2 , "" , .TypedVals ) ;  require ( i256_1 < i256_2 , "" , .TypedVals ) ;  require ( i8_1 < 4 , "" , .TypedVals ) ;  require ( 2 < i8_2 , "" , .TypedVals ) ;  require ( 2 < 4 , "" , .TypedVals ) ;  require ( i8_1 != i8_2 , "" , .TypedVals ) ;  require ( i32_1 != i32_2 , "" , .TypedVals ) ;  require ( i112_1 != i112_2 , "" , .TypedVals ) ;  require ( i256_1 != i256_2 , "" , .TypedVals ) ;  require ( i8_1 != 4 , "" , .TypedVals ) ;  require ( 2 != i8_2 , "" , .TypedVals ) ;  require ( 2 != 4 , "" , .TypedVals ) ;  require ( i8_2 > i8_1 , "" , .TypedVals ) ;  require ( i32_2 > i32_1 , "" , .TypedVals ) ;  require ( i112_2 > i112_1 , "" , .TypedVals ) ;  require ( i256_2 > i256_1 , "" , .TypedVals ) ;  require ( i8_2 > 2 , "" , .TypedVals ) ;  require ( 4 > i8_1 , "" , .TypedVals ) ;  require ( 4 > 2 , "" , .TypedVals ) ;  .Statements
           </contract-fn-body>
@@ -59,6 +62,9 @@
     <tx-origin>
       1p160
     </tx-origin>
+    <block-timestamp>
+      0p256
+    </block-timestamp>
     <this>
       2p160
     </this>

test/regression/arithmetic.txn

@@ -1 +1 @@
-create(1, 0, TestArithmetic, )
+create(1, 0, 0, TestArithmetic, )

test/regression/arraystestcontract.ref

@@ -40,6 +40,9 @@
           <contract-fn-return-names>
             ListItem ( noId )
           </contract-fn-return-names>
+          <contract-fn-payable>
+            false
+          </contract-fn-payable>
           <contract-fn-body>
             return arr ;  .Statements
           </contract-fn-body>
@@ -62,6 +65,9 @@
           <contract-fn-return-names>
             .List
           </contract-fn-return-names>
+          <contract-fn-payable>
+            false
+          </contract-fn-payable>
           <contract-fn-body>
             .Statements
           </contract-fn-body>
@@ -82,6 +88,9 @@
     <tx-origin>
       1p160
     </tx-origin>
+    <block-timestamp>
+      0p256
+    </block-timestamp>
     <this>
       2p160
     </this>

test/regression/arraystestcontract.txn

@@ -1 +1 @@
-create(1, 0, TestArraysContract, )
+create(1, 0, 0, TestArraysContract, )

test/regression/block.ref

@@ -39,6 +39,9 @@
           <contract-fn-return-names>
             .List
           </contract-fn-return-names>
+          <contract-fn-payable>
+            false
+          </contract-fn-payable>
           <contract-fn-body>
             bool x = false ;  { bool x = true ;  require ( x , "" , .TypedVals ) ;  .Statements }  if ( x ) { require ( false , "" , .TypedVals ) ;  .Statements }  .Statements
           </contract-fn-body>
@@ -59,6 +62,9 @@
     <tx-origin>
       1p160
     </tx-origin>
+    <block-timestamp>
+      0p256
+    </block-timestamp>
     <this>
       2p160
     </this>

test/regression/block.txn

@@ -1 +1 @@
-create(1, 0, BlockTest, )
+create(1, 0, 0, BlockTest, )

test/regression/boolean.ref

@@ -39,6 +39,9 @@
           <contract-fn-return-names>
             .List
           </contract-fn-return-names>
+          <contract-fn-payable>
+            false
+          </contract-fn-payable>
           <contract-fn-body>
             bool x = true ;  if ( x || fail ( .TypedVals ) ) { .Statements } else { require ( false , "" , .TypedVals ) ;  .Statements }  if ( x && true ) { .Statements } else { require ( false , "" , .TypedVals ) ;  .Statements }  x = false ;  if ( x && fail ( .TypedVals ) ) { require ( false , "" , .TypedVals ) ;  .Statements }  if ( x || true ) { .Statements } else { require ( false , "" , .TypedVals ) ;  .Statements }  .Statements
           </contract-fn-body>
@@ -61,6 +64,9 @@
           <contract-fn-return-names>
             .List
           </contract-fn-return-names>
+          <contract-fn-payable>
+            false
+          </contract-fn-payable>
           <contract-fn-body>
             require ( false , "" , .TypedVals ) ;  .Statements
           </contract-fn-body>
@@ -81,6 +87,9 @@
     <tx-origin>
       1p160
     </tx-origin>
+    <block-timestamp>
+      0p256
+    </block-timestamp>
     <this>
       2p160
     </this>

test/regression/boolean.txn

@@ -1 +1 @@
-create(1, 0, BoolTest, )
+create(1, 0, 0, BoolTest, )