Ryan Doenges

Unclear documentation of project/workspace root

1

This is #1848 again. The documentation says `%{project_root}` is the root of your project when it's actually inside _build for hygiene reasons, and I got confused by the docs. I...

Legal to form header stacks of header unions?

3

I'm having trouble telling if header stacks `H[n]` require `H` to be a header only or if they also allow header unions. The p4c typechecker allows unions, and the original...

Division with bit<w> arguments

9

p4c permits division and modulo between bit values but the specification restricts those operations to positive `int` values. I think this is probably the spec being too restrictive rather than...

Are structure-valued expressions subject to implicit casts?

2

In the new section on structure-valued expressions, the spec says "The typeRef can be omitted if it can be inferred from context, e.g., when initializing a variable with a struct...

Vcalyx

1

This PR adds the Coq development of VCalyx including the syntax and interpreter. It also includes Fud stages for invoking the vcalyx interpreter and a few Runt tests. Not ready...