P-token tweaks

[jberthold]

• implemented Downcast projection (overwrites the variantIdx of given enum data, without checking)
• implemented unOpPtrMetadata for references to arrays and slices (returns length as usize)
• decoding zero-sized structs (returns struct with no fields, type is already set. Not checking for absence of fields atm)
• thunking for #decode: unimplemented decoding becomes a thunk with bytes and type information

This allows the p-token transfer proof to progress further without spurious branching.

Also removes the vacuous branches in symbolic-args-fail, making more progress because PtrMetadata is now available

[jberthold]

A word of warning: I had this as an [owise] rule first, and got loads of branching on the thunk default rule for Evaluations. We cannot use owise on rules over Evaluation.

[ehildenb]

This decodeConstant operates a bit differently than teh other rvalue we are evaluating (the operandConst). All teh other ones go to an Evaluation on the <k>-cell, not as a function, which means we can have a single owise rule for thunking them just because they're in sort Evaluation. Instead here, we are going straight to calling the function #decodeConstant which returns a Value instead of a TypedValue, so thunking has to be done specially for it.

Can we instead have the rule for operandConst be like (with #decodeConstant no longer a function, and have it return a full TypedValue):

  rule <k> operandConstant(constOperand(_, _, mirConst(KIND, TY, _))) 
        => #decodeConstant(KIND, {TYPEMAP[TY]}:>TypeInfo), TY) 
        ... 
      </k> 
      <types> TYPEMAP </types> 
    requires TY in_keys(TYPEMAP) 
     andBool isTypeInfo(TYPEMAP[TY]) 
    [preserves-definedness] // valid Map lookup checked 

Then we don't need a special case for thunking it.

[jberthold]

Maybe indeed decodeConstant should also return TypedValue for now.
We should also do the refactoring to make them all return Value at some point soon, but I will adapt decodeConstant for now.

[ehildenb]

Looks good overall! I'm going to open a separate PR to shorten the output, and have one question/thought about the #decodeConstant (up to you how to handle it).