Add st.balance consistent with contract_balance

[satos---jp]

This MR introduces the st.balance parameter, which corresponds to the BALANCE Michelson op.
This MR adds the following codes.

• When dispatching, the assumption st.balance = c.[dst_contract_name]_balance + st.amount is added.
• The requirement st.balance = c.[contract_name]_balance + st.amount is added as the require closue of each contract_funcs.
• When processing Xfer op in the contracts, the st.balance field is initialized with the appropriate value. (For the unknown case, I initialized it with 0 for now.)

This MR also adds https://github.com/satos---jp/icon-why3/blob/satos%40add-balance/examples/test_balance.tzw which tests st.balance.

(In addition, this MR contains a commit irrelevant to st.balance, which fixes https://github.com/satos---jp/icon-why3/blob/satos%40add-balance/examples/neg/entrypoints.tzw )

[westpaddy]

I think the assumption mentioned in the first item is unnecessary since the balance field is initialized appropriately as the third item. For the unknown contract, you can put a corresponding assumption for the initializing code.
Please check if the following proposed version of intermediate code follows what you want to do, and if it is correct, could you change the implementation?

module Top
  use export int.Int
  use export int.Abs
  use export int.EuclideanDivision
  use export list.List
  use export option.Option
  use export map.Map
  use export map.Const
  
  exception Insufficient_mutez
  
  exception Terminate
  
  predicate is__tuple2_wf (is_a_wf: 'a -> bool) (is_b_wf: 'b -> bool) (ab: 
    ('a,
     'b)) =
    match ab with
    | ((a, b)) -> (is_a_wf a) /\ (is_b_wf b)
    end
  
  predicate is_list_wf ('a -> bool) (list 'a) = true
  
  predicate is_unit_wf unit = true
  
  predicate is_bool_wf bool = true
  
  predicate is_map_wf ('a -> bool) ('b -> bool) (map 'a 'b) = true
  
  predicate is_option_wf (is_a_wf: 'a -> bool) (o: option 'a) =
    match o with
    | None  -> true
    | Some a -> is_a_wf a
    end
  
  predicate is_int_wf int = true
  
  type nat = int
  
  predicate is_nat_wf (x: nat) = x >= 0
  
  type mutez = int
  
  predicate is_mutez_wf (x: mutez) = x >= 0
  
  type bytes = string
  
  predicate is_bytes_wf bytes = true
  
  type big_map 'a  'b = map 'a 'b
  
  predicate is_big_map_wf ('a -> bool) ('b -> bool) (big_map 'a 'b) = true
  
  type address = int
  
  predicate is_address_wf address = true
  
  type key_hash = int
  
  predicate is_key_hash_wf address = true
  
  type timestamp = int
  
  predicate is_timestamp_wf address = true
  
  type contract 'a = int
  
  predicate is_contract_wf ('a -> bool) (contract 'a) = true
  
  type or 'a  'b = 
      | Left 'a
      | Right 'b
  
  predicate is_or_wf (is_a_wf: 'a -> bool) (is_b_wf: 'b -> bool) (ab: 
    or
      'a 'b) =
    match ab with
    | Left a -> is_a_wf a
    | Right b -> is_b_wf b
    end
  
  type lambda 'a  'b = 'a -> 'b
  
  predicate is_lambda_wf ('a -> bool) ('b -> bool) (lambda 'a 'b) = true
  
  type step = {
             source : address;
             sender : address;
             self : address;
             amount : mutez;
             balance : mutez;
             level : nat;
             now : timestamp
             }
  
  function mk_step (source: address) (sender: address) (self: address) (amount: mutez) (balance: mutez) (level: nat) (now: timestamp) : step =
    { source = source ;
      sender = sender ;
      self = self ;
      amount = amount ;
      balance = balance ;
      level = level ;
      now = now }
  
  predicate step_wf (st: step) = (st.amount) >= 0
  
  type gparam = 
      | Gp'0default'0unit unit
      | GpUnknown
  with operation = 
      | Xfer gparam mutez address
      | Sdel (option key_hash)
  
  scope A
    type storage [@gen_wf] = { acc : mutez; diff : mutez }
    
    predicate is_storage_wf (_v: storage) =
      ((is_mutez_wf (_v.diff)) /\ ((is_mutez_wf (_v.acc)) /\ true))
    
    function addr : address
    
    predicate param_wf (gp: gparam) =
      match gp with
      | Gp'0default'0unit _p0 -> (true /\ (is_unit_wf _p0))
      | _ -> false
      end
    
    scope Spec
      predicate default (st: step) (s: storage) (ops: list operation) (s': storage) (_p: unit) =
        let acc' = (s.acc) + (st.amount) in
        let abs = fun a b-> if (a > b) then (a - b)
                            else (b - a) in
        (s' = { acc = acc' ; diff = ((s.diff) + (abs acc' (st.balance))) })
          /\
          (ops = Nil)
      end
    
    predicate spec (st: step) (gp: gparam) (s: storage) (op: list operation) (s': storage) =
      match gp with
      | Gp'0default'0unit _p0 -> Spec.default st s op s' _p0
      | _ -> false
      end
    end
  
  type ctx = { a_storage : A.storage; a_balance : mutez }
  
  predicate ctx_wf (ctx: ctx) =
    ((is_mutez_wf (ctx.a_balance)) /\
       (((ctx.a_storage).A.is_storage_wf) /\ true))
  
  predicate inv (c: ctx) =
    (c.a_storage)
    =
    A.({ acc = (c.a_balance) ; diff = 0 })
  
  predicate inv_pre (c: ctx) = inv c
  
  predicate inv_post (_c: ctx) (c': ctx) = inv c'
  
  predicate a_pre (_st: step) (_gp: gparam) (c: ctx) = inv c
  
  predicate a_post (st: step) (_gp: gparam) (c: ctx) (c': ctx) =
    ((st.balance) = ((c.a_balance) + (st.amount)))
      /\
      ((c'.a_balance) = ((c.a_balance) + (st.amount)))
      /\
      (inv c')
  
  let rec ghost unknown g c
    requires { c.ctx_wf }
    requires { c.inv_pre }
    ensures { result.ctx_wf }
    
    ensures { inv_post c result }
    raises { Terminate }
    raises { Insufficient_mutez }
    variant { g } =
    if (g < 0) then (raise Terminate)
    else
      (if (any bool) then c
       else
         (val x1 : step
            ensures { result.step_wf } in
          val x2 : gparam in
          assume {
            ((true /\ (not ((x1.source) = A.addr))) /\
               (not ((x1.sender) = A.addr))) };
          assume {
            x1.self = A.addr ->
            x1.balance = c.a_balance + x1.amount
          };
          (let x3 =
             if ((x1.self) = A.addr) then
               (assume {
                  ((x2.A.param_wf) (*/\
                     ((x1.balance) = ((c.a_balance) + (x1.amount)))*)) };
                (a_func (g - 1) x1 x2 c))
             else (unknown (g - 1) c) in
           unknown (g - 1) x3)))
  with ghost a_func g st gp c
    requires { ((st.self) = A.addr) }
    requires { c.ctx_wf }
    requires { st.step_wf }
    requires { gp.A.param_wf }
    requires { ((st.balance) = ((c.a_balance) + (st.amount))) }
    requires { a_pre st gp c }
    ensures { result.ctx_wf }
    
    ensures { a_post st gp c result }
    raises { Terminate }
    raises { Insufficient_mutez }
    variant { g } =
    if (g < 0) then (raise Terminate)
    else
      (let x4 = { c with a_balance = ((c.a_balance) + (st.amount)) } in
       val x5 : A.storage
         ensures { result.A.is_storage_wf } in
       val x6 : (list operation) in
       assume { A.spec st gp (x4.a_storage) x6 x5 };
       (let x7 = { x4 with a_storage = x5 } in
        match x6 with
        | Nil  -> x7
        | Cons x8 Nil  ->
            let x14 =
              match x8 with
              | Sdel _ -> x7
              | Xfer x9 x10 x11 ->
                  assume { is_mutez_wf x10 };
                  (if ((x7.a_balance) < x10) then (raise Insufficient_mutez)
                   else
                     (let x12 =
                        { x7 with a_balance = ((x7.a_balance) - x10) } in
                      let x13 =
                        { source = (st.source) ;
                          sender = (st.self) ;
                          self = x11 ;
                          amount = x10 ;
                          balance =
                            (if (x11 = A.addr) then ((x12.a_balance) + x10)
                             else any mutez ensures { is_mutez_wf result }(*0*)) ;
                          level = (st.level) ;
                          now = (st.now) } in
                      if ((x13.self) = A.addr) then
                        (assume {
                           ((x9.A.param_wf) (*/\
                              ((x13.balance)
                                 = ((x12.a_balance) + (x13.amount)))*)) };
                         (a_func (g - 1) x13 x9 x12))
                      else (unknown (g - 1) x12)))
              end in
            x14
        | _ -> absurd
        end))
end

[satos---jp]

As you suggested, I removed balance-related assumptions from dispatchings and added them in the unknown function as follows instead.

$ icon examples/callback.tzw 

...

 let rec ghost unknown g c

...

            assume {
            ((((true /\ (not ((x1.source) = Caller.addr))) /\
                 (not ((x1.sender) = Caller.addr))) /\
                (not ((x1.source) = Callee.addr))) /\
               (not ((x1.sender) = Callee.addr))) };
          assume {
            if ((x1.self) = Caller.addr) then
              ((x1.balance) = ((c.caller_balance) + (x1.amount)))
            else
              (if ((x1.self) = Callee.addr) then
                 ((x1.balance) = ((c.callee_balance) + (x1.amount)))
               else true) };

...