Linard Arquint
Linard Arquint
@jcp19 This PR is in draft mode as the design choices are more like suggestions. Code-wise, I do not have any additional changes planned so I'd appreciate a code review....
> is the module-level json always required, even when we do not use the --config option? My expectation is that it is not, otherwise it may make it harder for...
I'm not the biggest fan of special casing the encoding for ghost structs as this seems rather confusing to users. Instead, I've implemented a type checker warning for this case...
I agree with your statement that ghost types use == like ===. My fear is related to the different semantics between a ghost struct and a struct with just ghost...
@jcp19 I've now implemented equality (`==`) for ghost structs to match `===`. Could you take a look at the most recent commit? In particular, I have the impression that type...
> No blocking issues found in SCION How come an exception is _not_ a blocking issue? ^^
> Interestingly, trying to verify the [path](https://github.com/viperproject/VerifiedSCION/tree/master/pkg/slayers/path) package in VerifiedSCION as is leads to multiple type errors (expected) and an exception (unexpected): I just checked: merging this PR with #855...
CI is currently failing as #855 must be first merged
To sequentialize the desugarer, you only have to make sure that the following promises execute sequentially. `// we place `mainPackageFut` at index 0 val allPackagesFut = Future.sequence(mainPackageFut +: importedProgramsFuts) val...
@JonasAlaif Looking a the first axiom in the encoding, it seems to me that this PR basically restricts the injectivity axiom that would normally be generated for each adt constructor....