Implement "can process" for block machine.

[chriseth]

No description provided.

[chriseth]

The formatter already pays off. The current version of the code does return range constraints, but somehow, for the binary machine, the new range constraints for the inputs are unconstrained, and this is already true for the variables.

The range constraint on the input A should be derived from identity 2 on row 2, and this is how it looks:

--------------[ identity 2 on row 2: ]--------------
main_binary::A' = ((     main_binary::A      * (1 - main_binary::latch)) + (main_binary::A_byte * main_binary::FACTOR))
    <known>     =             ???                           0                       ???                16777216        
                =   [0, 16777215] & 0xffffff                                  [0, 255] & 0xff                          
main_binary::A' =                     (     main_binary::A      + (main_binary::A_byte * 16777216))                    
    <known>     =                                ???                       ???                                         
                =                      [0, 16777215] & 0xffffff      [0, 255] & 0xff  

it's unclear to me why the .solve() function does not derive a new range constraint on A', because it actually should.

[chriseth]

Ah nice! It does not consider the "only concrete is considered known" because this is only done if we fully solved the other case. The solution is to just do both, regardless of the other!

[chriseth]

Ok, that completely derives range constraints on the binary machine, but it still does not solve the vm_to_block_to_block stackable error :(