Make AddCarry available in Pancake

[dnezam]

I think this is best explained by the addition in the examples:

(** __add_with_carry__ becomes AddCarry at the wordLang level.
    It takes three word operands (left, right, carry-in) and produces a struct
    of two words: (sum, carry-out). Non-zero values for carry-in are interpreted
    as 1. Permitted positions are declaration RHS and assignment RHS;
    standalone, handler-attached, and tail-return calls are not supported. *)
val add_with_carry_ex = ‘
  fun {1,1} main() {
    var a = 1;
    var b = 2;
    var c = 0;
    var {1,1} r = __add_with_carry__(a, b, c);
    r = __add_with_carry__(a, b, c);
    return r;
  }’;

This is achieved by adding a Primitive node throughout the Pancake layer, which is essentially handed down as is down to wordLang. Some noteworthy things:

• We use pan_to_crep to give everything new names (hence Primitive only mentions nums starting from crep)
• Since AddCarry in wordLang overwrites the arguments, aliasing is a bit problematic. I think one could end up transporting the fact that all names are distinct from the earlier layers, but I ended up extending locals_rel in loop_to_wordProof to mention the fact that numbers are even, so we can make use of the odd numbers as scratch space

[dnezam]

If you have time @halogentlepersuasion , perhaps it would be good if you took a look at whether the changes to panStatic are alright.

[talsewell]

Looks generally OK. A few of the proofs seem a bit verbose, suggesting that "Primitive" is one of the medium-tricky constructs, when it seems on the easier side.

I suspect word_and_carry should be word_add_carry?

I'm a bit confused why the patch moves shape_val up to panLang, maybe there's a new use for it somewhere I missed.

I think I understand the bit about carrying the distinctness down from other layers better now. One option for that is to put it in the semantics: have the loop (and maybe crep) semantics fail if you try to provide overlapping register arguments to Primitive. But yeah, using funny-numbered temporaries does seem like a reasonable strategy.

[dnezam]

Thanks for the review!

Looks generally OK. A few of the proofs seem a bit verbose, suggesting that "Primitive" is one of the medium-tricky constructs, when it seems on the easier side.

I suspect part of the reason is that some of the proofs are generated by Claude. When things looked extra sketchy, I went over it myself/told it to clean up, but perhaps I missed some cases. In particular, it seems that Claude liked to do a lot of ... by ... proofs, which didn't seem harmful, so I left them be. (There is a risk that it proves unnecessary things that maybe break in the future, but hopefully that won't turn out to be a problem.)

Another reason for the verbosity could be that Primitive is quite general. For example, I think in crepLang it is the only construct using varname list, leading to some tedious lemmas relating lookups (OPT_MMAP, FLOOKUP, etc.)

Either way, if there is something especially suspicious, please let me know.

I suspect word_and_carry should be word_add_carry?

Indeed, thanks for catching that. I will fix that. Goes to show that I don't need AI to add mistakes to my PRs 🫠

I'm a bit confused why the patch moves shape_val up to panLang, maybe there's a new use for it somewhere I missed.

I think that was from the version that added AddCarry as an expression (as opposed to Primitive as prog). I could move it back (but since it is general enough, perhaps it is better off in panLang anyway?)

[halogentlepersuasion]

If you have time @halogentlepersuasion , perhaps it would be good if you took a look at whether the changes to panStatic are alright.

Sure thing, here's everything I noticed.

For panStaticScript.sml:

• Please document the new checks in the comment at the top of the file in a logical spot (though be mindful of whether another line covers it already)
• Function comments are a bit verbose, eg. primitive_idents could be "List of recognised Primitive identifiers for usage hints" or similar. Just follow the style of the other comments
• I think check_addcarry_args would be better as a more generalised check_primitive_args function to mirror the Op and Panop cases in static_check_exp, such that line 1170 becomes:

res_sb <- check_primitive_args ctxt pop esret.sh_bds

• The v argument in the Primitive case of static_check_prog should be called vname to match the name scheme in the rest of the file
• Said Primitive case could stand to be moved to a more logical spot in the case list -- being something that syntactically looks like a special kind of call, I suggest putting it after ExtCall

For panStaticExamplesScript.sml:

• The entire block of new tests has been deposited in the middle of the default shape tests for some reason? Please move them to match your additions to the panStaticScript error list (all tests follow that order and use those descriptions as section comments)
• Variables should have explicit shape declarations to match the style of the rest of the file (shapes are only defaulted in the default shape tests)
• Destination shape tests should include the new named structs as well. You can reference the AssignCall cases for the structure (you don't need a separate comment for all of them) and for named struct usage (at least until I write up the NEWS.md entry for them)
• Speaking of AssignCall, some of your comments say AssignCall instead of AddCarry. This will probably get fixed as a side effect of the first dot point
• The addcarry_global_dest test should have the global variable in the correct shape (currently defaulted to 1) else the case may pass after detecting the wrong error
• Adding tests for operand shapes would also be good (again, you can reference the relevant sections)

Also, add an example directly in the NEWS.md entry instead of pointing to panConcreteExamples.sml; we're trying to phase out the latter as a file people are pointed towards.

Otherwise, the changes seem functional :)