Feature/armv8a distilled - #5
Closed
clebreto wants to merge 74 commits into
Closed
Conversation
New architecture `-arch armv8a` targeting A64, modeled at the full 64-bit register width (reg_size = U64, X registers only). Coq: - armv8a_decl.v: registers R0..R30/RZR/RSP printed x0..x30/xzr/sp, NZCV flags, 14 condition codes, AAPCS64 calling convention, register shifts (0..63). - armv8a_instr_decl.v: 76 mnemonics with full semantics; each carries its ARM ARM (DDI 0487 M.a) documentation block (C6.2 section, page, summary, syntax and Operation pseudocode). Flag-setting forms are separate mnemonics (ADDS, ...); conditional selection (CSEL family) takes the condition as a first-class operand; loads/stores rely on the framework for the memory access and only extend values; MOVZ/MOVN/MOVK model wide immediate moves. - armv8a.v: NZCV condition evaluation and asm instance. - armv8a_extra.v: swap, add_large_imm and smart_li pseudo-instructions (smart_li expands to MOVZ/MOVK sequences; A64 has no conditional execution so there is no conditional variant). - armv8a_lowering.v (new): lowering pass; conditions via CMP/TST and NZCV, word conditional expressions via CSEL, large ADD/SUB immediates via add_large_imm, shifted-operand fusion. - armv8a_params_core.v, armv8a_params.v, armv8a_stack_zeroization.v: compiler passes parameters at U64. - arch_decl.v: new CAimmC_armv8a_shift_amount and CAimmC_armv8a_0_16_32_48 immediate checkers (other architectures reject them). OCaml: - pp_arm_v8a.ml: GNU/ELF AArch64 printer; W-register forms for narrow loads/stores, extensions and 32-bit multiplies; ADRP/ADD :lo12: for global addresses; b.cc branches and ret-based returns. - coreArchFactory retargeted to Armv8a_* modules; callstyle returns via X30. Docs: compiler/doc/armv8a_isa_docs.json machine-readable extraction of the ARM ARM instruction documentation (recording the PDF edition and hash of the source document). Tests: 14 test programs under tests/success/armv8a, wired as the `armv8a` check category (compiled, assembled with llvm-mc --triple=aarch64 and linked with ld.lld). Correctness proofs are deferred; every semantics function is total and the extraction cone contains no admitted statement.
Data-processing instructions, comparisons, conditional selection, moves and loads/stores now exist in both the 64-bit (X) and 32-bit (W) forms, selected by the new [opts_size] instruction option (intrinsic suffix _32, e.g. #ADD_32). W-form destinations zero the upper 32 bits ([MSB_CLEAR]) as in the architecture. The lowering pass lowers word operations at both sizes, including 32-bit comparisons, CSEL, MOVZ/MOVK immediate materialization, register-to-register sign/zero extensions (SXTB/SXTH/SXTW/UXTB/UXTH/UXTW) and narrow zero/sign-extending loads. Fixed-size instructions (UMULL, SMULH, ADR, LDRSW, REV32, ...) are only valid in the X form. The shared CAimmC_armv8a_shift_amount immediate checker takes the operand size (shift amounts are 0..31 in the W form).
Fixes the codegen "blind spots" that made real AArch64 output fault at run time, and documents each modeling decision against the spec. Register model (armv8a_decl.v): - Drop XZR from the register set. Field value 31 is the zero register in the X[] accessor (reads zero, ignores writes), so allocating it is unsound; it was producing `mov sp, xzr`. Like RISC-V's x0, omit it and emit ZR-operand ops (CMP, NEG, TST, ...) as dedicated mnemonics. - Drop x18: it is the platform register, reserved on Apple/Windows/SCS Linux where the OS may clobber it asynchronously (invisible to Jasmin's clobber analysis), which corrupted the saved stack pointer. Stack pointer (armv8a_params.v): - Round every frame allocation to 16 bytes and never re-align a frame to less than 16, so SP stays quadword-aligned across nested calls (AArch64 raises an SP Alignment exception otherwise). - Restore a spilled SP via a scratch register + MOV, since A64 LDR cannot target SP (its result goes through the X[] accessor, where 31 = ZR). Each decision is sourced (Arm ARM DDI0487M.a B1.2/D1.4.10.2, AAPCS64, Apple platform ABI) in the inline comments and in the new compiler/doc/armv8a_register_model.md. Validated: ML-DSA-65 compiled with -arch armv8a assembles cleanly and passes the full formosa-mldsa KAT suite (NIST DRBG, PQC, Wycheproof) natively on arm64.
Add armv8a_params_core_proof.v, mirroring arm_params_core_proof.v, with the sem_fopn_args correctness lemmas for the single-instruction core builders used by stack handling and immediate materialization: add, addi, sub, subi, mov, andi (the AND behind align), plus the smart_mov combinator. All proven, no admits. One AArch64-specific wrinkle vs ARMv7-M: SUB/AND semantics use word-scope operators (sub_word / wand) that are not definitionally equal to the ring operators in the lemma statements, so the proofs bridge with sub_wordE (ADD is fine since add_word is defeq to ring add). Deferred (documented in the file header): li and the gen_smart_opi / smart_addi / smart_subi combinators built on it. AArch64 li emits a variable-length MOVZ/MOVN/MOVK sequence over up to four 16-bit halves of a 64-bit register, whose correctness needs bit-level decomposition lemmas that do not port from ARMv7-M's fixed MOV/MOVT (two-halfword) materialization.
Add armv8a_params_common_proof.v, mirroring the portable part of arm_params_common_proof.v. Lifts the core sem_fopn_args results through the to_opn/Oarmv8a wrapper to the generic linear semantics: - sem_fopn_equiv / sem_fopns_equiv: the Oarmv8a-tagged op runs exactly as the core builder; - mov / addi / subi / align at sem_fopn_args level, and their eval_instr forms (the single-instruction builders used by allocate/free_stack_frame and set_up_sp_register); - armv8a_align_mask: the AND mask Z_mod_lnot (wsize_size al - 1) equals -wsize_size al modulo the register base, so align computes exactly align_word (proved via wrepr_wnot + ZlnotE). All proven, no admits. As in armv8a_params_core_proof.v, the li-based smart_* combinators remain deferred (AArch64 MOVZ/MOVK materialization; see that file's header).
Document why the two shift-amount checkers in caimm_checker_s carry different arguments (shift_kind for AArch32, wsize for AArch64), with verbatim spec sources: - shift_kind.v [shift_amount_bounds]: AArch32 amount range is type-dependent (LSL 0..31, LSR/ASR 1..32, ROR 1..31), from DecodeImmShift (Arm ARM DDI0487M.a, J1.2.3.7, p. J1-16079): LSR/ASR encode jasmin-lang#32 as imm5=0 and ROR #0 is RRX, so only LSL admits 0. - armv8a_decl.v [check_shift_amount]: AArch64 amount range is width-dependent and type-independent, [0, datasize), from the C6.2 shifted-register decode (p. C6-1813): shift_amount = UInt(imm6), datasize = 32 << UInt(sf), and "if sf == '0' && imm6<5> == '1' then UNDEFINED". - arch_decl.v: note at the caimm_checker_s constructors explaining the axis each is keyed on and pointing to the two predicates. Comment-only.
Replace the permissive CAimmC_none immediate checkers with predicates grounded in the Arm ARM (DDI 0487 M.a): - CAimmC_armv8a_arith_imm: imm12, optionally LSL jasmin-lang#12 (C6.2.5), for ADD/ADDS/SUB/SUBS/CMP/CMN. Same predicate as is_arith_small, which now aliases it. - CAimmC_armv8a_bitmask_imm: logical bitmask immediates (DecodeBitMasks), for AND/ANDS/ORR/EOR/TST. Executable check: replication tested as invariance under rotation by the element size, the element tested as a rotated run of ones over all (bounded) rotations. - CAimmC_armv8a_mov_imm: MOV alias immediates (wide, inverted wide, or bitmask; C6.2.192-194). - BIC/BICS and MVN have no immediate form in A64: register-only now. Non-encodable immediates (e.g. and x, x, #8380417) are now rejected at assembly generation with an error naming the constraint, instead of emitted as assembly the assembler refuses. Also settle the smart_li_args FIXME: rejecting sizes other than U64/U32 is by design (the only A64 operand widths with MOVZ/MOVK forms).
Discharge the central proof blocker of the ARMv8-A backend: correctness of ARMv8AFopn_core.li and the gen_smart_opi combinators built on it. Word level (ws-generic, reusable at U32 for the Oarmv8a_smart_li assembly-generation proof later): - wbit_n_add: bit-splitting of an n-aligned sum, requiring only that the sum fits the word (the ARMv7-M analog needs 2^n * 2^n <= wbase, which fails for the high chunks of a 64-bit word). - wor_wrepr_add: OR of an n-aligned value with a value below 2^n is addition. - wand_movk_mask_id: the MOVK keep-mask leaves a value untouched when its bits from the insertion position up are zero. - armv8a_MOVZ/MOVN/MOVK_semiE: closed forms of the wide-move semantics; MOVK inserting chunk c at position sh into a value below 2^sh yields wrepr (2^sh * c + m). Semantic level (register size): - movz/movn/movk sem_fopn_args lemmas. - li_lsem_1: the three-way case split of li (single MOVZ; single MOVN via Z_mod_lnot; general MOVZ + up-to-three conditional MOVK), the general case by the chunk-chain invariant that after treating the chunk at position sh the register holds wrepr U64 (n mod 2^(sh+16)) -- chunks skipped because they are zero preserve the invariant for free (z_mod_recombine). - gen_smart_opi_sem_fopn_args, ported from ARMv7-M now that li is available, and the ARMv8AFopnP lifts smart_addi/smart_subi and their _tmp variants in armv8a_params_common_proof.v.
…acle The linearization correctness specs (sf_correct, set_up_sp_register_correct) require lip_allocate/free_stack_frame to adjust SP by exactly the size they are given and set_up_sp_register to align by exactly the frame alignment, for any size — so the round_up_16 wrapping and the U128 alignment bump inside the ARMv8-A linearization params were unprovable as stated. Keep the params spec-exact and enforce the architectural invariant (SP alignment checking, Arm ARM DDI0487M.a D1.4.10.2) where frame shapes are decided instead: - Arch_full.Core_arch gains sp_min_align (U128 on armv8a, U8 elsewhere). - stackAlloc.ml raises every stack-using function's final alignment to sp_min_align (both the subroutine and export paths, next to the existing stack-zeroization bump). Frame sizes are rounded up to the frame alignment (stack_frame_allocation_size), so every SP adjustment becomes a multiple of 16 and the platform-guaranteed entry alignment is preserved across calls. Functions with no stack footprint keep their alignment so exports can still use SavedStackNone (which requires sf_align = U8). - armv8a_params.v: drop round_up_16 and the set_up_sp_register alignment bump; document the invariant's new home. Validated: emitted code aligns an 8-byte frame to 16 and ANDs SP with ~15 in the export prologue; all 14 armv8a tests pass; formosa-mldsa KATs pass for all three parameter sets.
New armv8a_params_proof.v, mirroring arm_params_proof.v: Stack alloc (complete, armv8a_hsaparams record built): - armv8a_mov_ofsP: the full ADR/LDR/MOV/ADD/shifted-ADD/add_large_imm/STR case analysis over mk_lea, ported from ARMv7-M (the two mov_ofs definitions are structurally identical) with the AArch64 semi unfoldings. - armv8a_immediateP: the Oarmv8a_smart_li sopn semantics is the identity, so this is immediate. - armv8a_swapP. Linearization (9 of 10 obligations): - allocate/free_stack_frame via the smart_subi/addi_tmp lemmas (tmp case) and the plain subi/addi lemmas (no-tmp case), now that the definitions are spec-exact (no rounding). - set_up_sp_register: sub-align-mov-mov chain over abstract var_i's. - lmove, lstore, lload; lstores via the generic lstores_imm_dfl_correct plus ladd_imm correctness of ARMv8AFopn_smart_addi. - lip_tmp <> lip_tmp2 and check_ws; ok_lip_tmp/tmp2 (X16/X17). - h_lower_addressing_params (identity on armv8a). Still missing: lloads_correct for the custom armv8a_lloads (SP restored through X17 + MOV since LDR cannot target SP) -- the last field of h_linearization_params -- then the lowering, asm-gen and stack-zeroization proofs before h_architecture_params can be assembled.
Prove lloads_correct for the custom armv8a_lloads and assemble the full h_linearization_params record. armv8a_lloads restores the saved stack pointer through the scratch register X17 and a MOV, since an A64 load writes through the X[] accessor for which register number 31 is ZR, not SP. The proof: - lloads_foldM_eq_ex: a restore foldM only modifies the variables it sets (induction over the restore list). - hsp: the SP-restoring tail, proven from any varmap holding the old SP, covering both the LDR-with-small-offset form and the smart_addi-through-X17 form, by direct computation of the LDR/MOV semantics. - The register-restore prefix by the generic lloads_aux_correct for the small-offset branch, and for the rebased branch an induction relating the specification's foldM (offsets from the old SP) to the rebased foldM (offsets from X17 = SP + ofs0), mirroring lloads_imm_dfl_correct's inner induction. Proof-engineering notes (the goals mix two convertible elaborations of the same instances: the asm_opI flavor from armv8a_params.v definitions and the _asmop-of-sip flavor from linearization_proof.v): cross-flavor facts cannot be rewritten directly; they are bridged with occurrence patterns folded by kernel conversion (rewrite -[X in ..]/(..)), exact:-checked restatements, and a generic bind_ok_estate/foldM_1 pair to reduce binds without simpl (whose over-reduction breaks matching).
Condition assembly (the NZCV/condition-code model): - condt_of_rflagP, condt_notP, condt_andP, condt_orP against armv8a_eval_cond, by exhaustive flag-boolean case analysis (the A64 cond-code table, C1.2.4), and the eval_assemble_cond induction over Fvar/Onot/Obeq(GE-trick)/Oand/Oor, giving assemble_cond_spec. Extra ops (assemble_extra_correct): - Oarmv8a_swap: the three-EOR sequence, via assemble_opsP. - Oarmv8a_add_large_imm: via the smart_addi correctness lemma. - Oarmv8a_smart_li at BOTH widths: U64 via li_lsem_1, and U32 via a new li_lsem_1_w32 in armv8a_params_core_proof.v (W-form MOVZ/MOVK chain of at most two chunks, reusing the ws-generic MOVZ/MOVN/MOVK_semiE word lemmas; the 32-bit value lives in the register-typed variable under the withsubword discipline and value_uincl absorbs the upper-bit clearing at the assembly level). - assemble_extra_sz, and the armv8a_hagparams record. Also armv8a_hshp (SLH is empty on armv8a) and armv8a_is_move_opP (MOV/LDR/STR/STRH/STRB all return their input truncated to the output width, proved uniformly over the operand size). Remaining before h_architecture_params: armv8a_lowering_proof.v and armv8a_stack_zeroization_proof.v.
Port arm_stack_zeroization_proof.v (781 lines). The two zeroization strategies (loop and unrolled) and their state-relation invariants carry over almost verbatim since the armv8a code generator mirrors ARMv7-M's structure and the NZCV flag semantics (nzcv_of_aluop) are shared; the differences: - store_zero_eval_instr: armv8a's STR at default_opts is 64-bit even for a 32-bit store (the Store lexpr does the truncation), so the ARM store_mn_of_wsizeP shape does not apply; proven by four-way case computation over the store width, now up to U64 (the ws <= U32 bound becomes ws <= U64 throughout, matching the armv8a command's assert). - fopn_li/fopn_movi/fopn_sub eval_instr lemmas proven locally (the armv8a wrappers live in armv8a_stack_zeroization.v itself; fopn_li is the Oarmv8a_smart_li pseudo-instruction whose sopn semantics is the identity -- its MOVZ/MOVK expansion is the already-proven assembly-generation lemma). armv8a_params_proof.v gains armv8a_hszparams. Eight of the ten h_architecture_params fields are now proven; only the lowering proof (hap_hlop) remains.
Add armv8a_lowering_proof.v (lower_callP and it_lower_callP) and build the full armv8a_h_params : h_architecture_params armv8a_params record: all ten fields are now proven. The proof is a port of arm_lowering_proof.v, generalized from ARM's single register width to the W (U32) and X (U64) forms: chk_ws_reg yields a width disjunction rather than an equation, so the operand width stays abstract and the operator resolution peels the per-operator width asserts instead of enumerating wsizes. Goal-number-based tactic selectors from the ARM proof are replaced by mnemonic-dispatched branches, which are insensitive to the goal count and order. armv8a-specific differences from the ARM proof: - Pif is lowered to CSEL (A64 has no conditional execution), with a direct semantic proof against armv8a_CSEL_semi. - The new large_arith_imm path (64-bit ADD/SUB immediates that do not fit imm12) is proven against Oarmv8a_add_large_imm. - MADD/MSUB replace MLA/MLS, with the product width pinned to the operation width by antisymmetry. - Stores only accept registers (no conditional stores), with the narrow-store accumulator width bump. - lower_mulu and the shifted three-operand class do not exist on A64 and are dropped; the shiftable unop class covers MVN and NEG. Fix a soundness gap in the shift lowering found while proving it: armv8a_shift_semi reduces the shift amount modulo the operand size (faithful to A64 register shifts), but Jasmin's source shifts clamp it, so the two disagree for amounts >= the operand size. Olsr/Olsl/Oasr now only lower compile-time-constant amounts in [0, wsize), matching the constant-only discipline of Orol and get_arg_shift; in-range constant shifts compile unchanged, while variable logical shifts (previously silently miscompiled for out-of-range amounts) are rejected. Rotates are unaffected since rotation is periodic.
Generalize the shift-amount discipline from constant-only to the x86 and RISC-V design: a logical/arithmetic shift amount is accepted if it is either a compile-time constant in [0, wsize) or an expression explicitly masked to the operand size (a & (wsize_bits - 1)). In the masked case the mask is dropped, since the A64 register shifts already reduce the amount modulo the operand size; on that range the hardware modulus and Jasmin's clamping source semantics coincide, which check_shift_exprP proves (via wand_modulo). This restores idiomatic variable shifts, x = y >> (n & 63), while keeping unmasked variable shifts a compile-time error rather than the silent miscompilation they used to be. The armv8a shift test is updated to the masked idiom. Validated: full proofs build, the armv8a test suite, and the ML-DSA KATs for all three parameter sets with the rebuilt compiler.
The backend supports both the X (u64) and W (u32) register forms and the correctness proofs are width-generic, but every test exercised u64 only. Add a u32 test covering the lowered surface at the W width: immediate materialization (MOVZ/MOVK sequences and bitmask immediates), additions and subtractions with imm12 (optionally shifted) and shifted-register operands, MUL/MADD/MSUB, UDIV/SDIV, the logical operations with 32-bit bitmask immediates, constant and masked-variable shifts, rotations by a constant and by a register, conditional selection for the four condition kinds, and 32-bit loads and stores including the narrow extending forms and stack slots. Validated beyond compilation: the generated W-form assembly was executed natively (arm64 macOS) against an independent C reference over multiple input vectors, including shift amounts beyond the operand size going through the mask, with all checks passing.
The ARMv8-A stub of the safety analyzer returned true, silently claiming every program safe. Raise a proper compilation error instead.
The same code and comment appeared twice (subroutine and export blocks); introduce enforce_sp_min_align.
Add -sp-min-align to override the per-architecture default (Core_arch.sp_min_align: u128 on armv8a, u8 elsewhere).
AArch32 and AArch64 have the same flag register: move rflag (with its instances and printer) and the flag-combination description out of arm_decl/armv8a_decl into a new arm_common module that both re-export.
The A64 condition codes are those of AArch32 (minus the always-true AL/NV, which are deliberately not modeled on either architecture: an unconditional instruction simply has no condition operand). Move condt and its instances/printer to arm_common.
arm_eval_cond and armv8a_eval_cond were identical; keep a single definition next to the shared condt type.
The alias forms ASR/LSL/LSR/ROR already accept both the register and the immediate shift amount (ak_rrr ++ ak_rr_imm_shift) with the same semantics, so the V forms were dead duplicates: the lowering only ever emits the alias mnemonics.
Pair each assembly argument with the width of the register form to print (W registers for the sources of the extensions, long multiplies and zero-extending narrow loads/stores), as x86 does, instead of patching the printed form position-by-position in the OCaml printer. Remove wform_positions: the printer now derives the W form purely from the declared width.
A64 conditions are ordinary last operands (CSEL, CSET, ...), so print them like any other argument instead of returning None and re-appending the condition after a filter_map.
Pure reorganization of armv8a_instr_decl.v, mirroring arm_instr_decl.v: every *_semi (with its ISA doc block) now sits right before the instruction description (or family helper) that uses it, so both can be reviewed together.
armv8a_params_core, armv8a_lowering and armv8a_stack_zeroization are dependencies of armv8a_params and are extracted transitively, exactly as for x86/arm/riscv; drop the redundant entries.
Same idiom as JModel_m4; CMP/CMN/TST become the flag-only aliases of SUBS/ADDS/ANDS instead of re-deriving the formulas.
Reduce the modeled mnemonics from 72 to 43, keeping exactly the instructions that the compiler pipeline can emit: the lowering pass, the load-immediate and smart-address helpers, mov_ofs (ADR), stack zeroization, and pseudo-operation expansion. Dropped: SBC, SBCS, the widening/high multiplies (UMULL, SMULL, UMADDL, SMADDL, UMULH, SMULH), ANDS, BIC, BICS, the bit-field family (BFC, BFI, BFXIL, SBFX, UBFX, EXTR), the bit-manipulation family (RBIT, REV, REV16, REV32, CLZ, CLS), CMN, and the CSEL aliases (CSINC, CSINV, CSNEG, CSET, CSETM). The mnemonic tables (has_shift_mnemonics, ror_shift_mnemonics, sized_mnemonics), the lowering binop list and its proof, the OCaml DIT table, the hardware-semantics generator, and the intrinsics tests are pruned to match. Proofs, extraction, the armv8a test categories, the hardware differential test (21442 checks) and the ML-DSA known answer tests for all three parameter sets remain green.
The CAimmC_armv8a_0_16_32_48 checker accepted shifts 32 and 48 regardless of the operand width, while the W forms of MOVZ/MOVN/MOVK cannot encode them (the hw field has one bit in the W form); the mismatch was only documented as a skip in the hardware-semantics test. Make the checker carry the operand width, like CAimmC_armv8a_shift_amount, and rename it CAimmC_armv8a_halfword_shift: the legal shifts are the multiples of 16 below the operand width. The corresponding skip note disappears from the hardware-semantics generator.
Since the descriptors forbid ROR on the shifted arithmetic instructions (shift_allowed in id_valid), the shift kinds A64 cannot encode are invalid in the model rather than accepted-but-unassemblable, so the documented skip no longer describes a model/hardware gap. Also tighten a CSEL wording left over from the distillation.
clebreto
force-pushed
the
feature/armv8a-distilled
branch
from
July 21, 2026 22:02
a5ef665 to
8d4c50f
Compare
This was referenced Jul 22, 2026
…rface Move the five armv8a immediate conditions from the removed shared inductive to an architecture-local armv8a_caimm_cond type, following the caimm_cond interface of arch_decl: eqTypeC instance, checker and error-message printer live in armv8a_decl.v, and the argument kinds wrap the conditions in Some (None being an unconditioned immediate). The other architectures no longer see the armv8a conditions at all.
Set id_doit in every instruction description and i_doit on the extra operators, transcribing the per-mnemonic OCaml table: everything in the modeled set belongs to the A64 DIT instruction list (Arm ARM DDI0487M.a, section C3.2.13) except SDIV, UDIV and ADR. mk_rrr_instr takes the classification as an argument since its users differ (MUL is DIT, the divisions are not); mk_shifted preserves the field. The hand-written is_doit_asm_op / is_doit_asm_extra tables disappear from armv8a_arch_full.ml, as on the other architectures.
…asmin-lang#1520) * attach doit info to the declaration of the instruction add a boolean field id_doit to arch_decl.instr_desc_t and a corresponding field i_doit to sopn.instruction_desc; base ops forward id_doit to i_doit (arch_extra.get_instr_desc); * fix DOIT information for VPMINS/VPMAXS Co-authored-by: Benjamin Gregoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Vincent Laporte <Vincent.Laporte@inria.fr>
…g#1536) * Linearization params: more general lload & lstore The parameters lip_lload and lip_lstore now accept as argument a wsize that describe the size of the memory access. * Linearization proof: remove redundant hypotheses * Linearization proof: make spec_lload more general * Linearization proof: make spec_lstore more general
lip_lstore and lip_lload now take the width of the transferred value (main commit "Linearization params: make lload and llstore more general"): thread it through armv8a_lstore/armv8a_lload and the custom armv8a_lloads (per-variable width for the restored registers, Uptr for the saved stack pointer), and drop the vtype hypotheses that disappeared from the correctness specifications.
Owner
Author
|
Moved upstream: jasmin-lang#1541. The review threads above stay here for reference; every remark is summarized with its resolution in the new PR description. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.