Adam T. Geller
Adam T. Geller
Hi, I'm getting the following error with the prusti-assistant (latest release version): `[Prusti internal error] There is no procedure contract for loan bw19. This could happen if you are chaining...
Hi there, I'm getting the following error: ``` error: [Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Pred(Field(FieldExpr { base: Local(Local { variable: _9: Ref(tuple2$usize$bool), position: Position { line: 0,...
Certain typing rules in the typing judgment `\vdash` in `InstructionTyping.rkt` rely on meta-function calls inside recursive calls to `\vdash` in the premise. For example: ``` [(where ((t_1 ...) -> (t_2...
We want to add documentation for every metafunction, describing the purpose and usage, as well as thorough documentation for the reduction relation, typing judgments, and typechecker. The former should make...
Supported functionality we want: 1. Instantiate and add memories 2. Set and get memory 3. Instantiate and add tables 4. Set, get, and grow tables 5. Get exported objects from...
To represent external functions: Introduce a new `cl` production rule `(host_func tf any)`. To wrap and embed external functions: Have a macro to construct ```(define/contract (f store x_1 ...) (->...
### Description Multiple functions that allocate qubits will cause `assign-wire-indices` to produce duplicate `borrow_wire` ops (i.e., two `borrow_wire` ops with the same index). This change ensures that `assign-wire-indices` refuses to...
### Description This is a draft of an analysis to determine dependency information between qubit operations in a quake program.
#3306 introduces two environment variables for testing purposes, `CUDAQ_PHASE_FOLDING` and `CUDAQ_BYPASS_PHASE_FOLDING_MINS`. Preferably, these should be part of some sort of runtime configuration instead.
### Description A version of #3306 that works on the value semantics instead of the reference semantics. Some todos: - Definitions are split across files, it would be better to...