Use `function` instead of `method`

[DavePearce]

For example, the following proof takes 20M resource usage.

    method Test_IR_03(x: u8, y: u8) returns (z:u8)
    requires x >= y
    ensures z <= x
    {
        var vm := EVM.Init(gas := INITGAS);
        //
        vm := Bytecode.Push1(vm,y);
        vm := Bytecode.Push1(vm,x);
        vm := Bytecode.Sub(vm); // x - y
        assert vm.Peek(0) == (x as u256) - (y as u256);
        vm := Bytecode.Push1(vm,0);
        vm := Bytecode.MStore(vm);
        vm := Bytecode.Push1(vm,0x1);
        vm := Bytecode.Push1(vm,0x1F);
        vm := Bytecode.Return(vm);
        //  read one byte from vm.data starting at 0
        return ByteUtils.ReadUint8(vm.data,0);
    }

In contrast, this equivalent version takes only 11M:

    /**
     *  Subtract `y` from `x` and return result in `z`.
     */
    function Test_IR_03b(x: u8, y: u8) : (z:u8)
    requires x >= y
    ensures z <= x
    {
        var vm0 := EVM.Init(gas := INITGAS);
        //
        var vm1 := Bytecode.Push1(vm0,y);
        var vm2 := Bytecode.Push1(vm1,x);
        var vm3 := Bytecode.Sub(vm2); // x - y
        assert vm3.Peek(0) == (x as u256) - (y as u256);
        var vm4 := Bytecode.Push1(vm3,0);
        var vm5 := Bytecode.MStore(vm4);
        var vm6 := Bytecode.Push1(vm5,0x1);
        var vm7 := Bytecode.Push1(vm6,0x1F);
        var vm8 := Bytecode.Return(vm7);
        //  read one byte from vm.data starting at 0
        ByteUtils.ReadUint8(vm8.data,0)
    }

This transformation should always work.