From 95768d80f0a7a0ba6a9c4e6621d49922a9bc2dad Mon Sep 17 00:00:00 2001 From: mamonet Date: Mon, 3 Oct 2022 17:42:24 +0200 Subject: [PATCH] Update PowerPC modules --- .../code/arch/ppc64le/PPC64LE.Vale.Decls.fsti | 16 ++--- .../arch/ppc64le/PPC64LE.Vale.InsBasic.vaf | 72 ++++++++----------- .../code/arch/ppc64le/PPC64LE.Vale.InsMem.vaf | 2 +- .../arch/ppc64le/PPC64LE.Vale.InsVector.vaf | 52 ++++++-------- fstar/specs/hardware/PPC64LE.Semantics_s.fst | 8 ++- 5 files changed, 64 insertions(+), 86 deletions(-) diff --git a/fstar/code/arch/ppc64le/PPC64LE.Vale.Decls.fsti b/fstar/code/arch/ppc64le/PPC64LE.Vale.Decls.fsti index 69f66342..93cb3c92 100644 --- a/fstar/code/arch/ppc64le/PPC64LE.Vale.Decls.fsti +++ b/fstar/code/arch/ppc64le/PPC64LE.Vale.Decls.fsti @@ -45,13 +45,9 @@ unfold let va_state = state val va_fuel : Type0 unfold let reg_opr = reg unfold let va_operand_reg_opr = reg -unfold let va_operand_dst_reg_opr = reg -unfold let dst_reg_opr = reg unfold let va_operand_Mem64 = maddr unfold let vec_opr = vec -unfold let dst_vec_opr = vec unfold let va_operand_vec_opr = vec -unfold let va_operand_dst_vec_opr = vec val va_pbool : Type0 val va_ttrue (_:unit) : va_pbool @@ -68,11 +64,9 @@ val mul_nat_helper (x y:nat) : Lemma (x * y >= 0) // Constructors val va_fuel_default : unit -> va_fuel [@va_qattr] unfold let va_op_reg_opr_reg (r:reg) : reg_opr = r -[@va_qattr] unfold let va_op_dst_reg_opr_reg (r:reg) : dst_reg_opr = r [@va_qattr] unfold let va_op_cmp_reg (r:reg) : cmp_opr = CReg r [@va_qattr] unfold let va_const_cmp (n:imm16) : cmp_opr = CImm n [@va_qattr] unfold let va_op_vec_opr_vec (v:vec) : vec_opr = v -[@va_qattr] unfold let va_op_dst_vec_opr_vec (v:vec) : dst_vec_opr = v [@va_qattr] unfold let va_opr_code_Mem64 (r:reg) (n:int) : maddr = @@ -82,18 +76,16 @@ unfold let va_opr_code_Mem64 (r:reg) (n:int) : maddr = [@va_qattr] unfold let va_eval_reg (s:va_state) (r:reg) : GTot nat64 = eval_reg r s [@va_qattr] unfold let va_eval_Mem64 (s:va_state) (m:maddr) : GTot nat64 = eval_mem64 (eval_maddr m s) s [@va_qattr] unfold let va_eval_reg_opr (s:va_state) (r:reg_opr) : GTot nat64 = eval_reg r s -[@va_qattr] unfold let va_eval_dst_reg_opr (s:va_state) (r:dst_reg_opr) : GTot nat64 = eval_reg r s [@va_qattr] unfold let va_eval_cmp_opr (s:va_state) (o:cmp_opr) : GTot nat64 = eval_cmp_opr o s [@va_qattr] unfold let va_eval_vec_opr (s:va_state) (v:vec_opr) : GTot quad32 = eval_vec v s -[@va_qattr] unfold let va_eval_dst_vec_opr (s:va_state) (v:dst_vec_opr) : GTot quad32 = eval_vec v s // Predicates [@va_qattr] unfold let va_is_src_reg_opr (r:reg_opr) (s:va_state) = True -[@va_qattr] unfold let va_is_dst_dst_reg_opr (r:dst_reg_opr) (s:va_state) = True +[@va_qattr] unfold let va_is_dst_reg_opr (r:reg_opr) (s:va_state) = True [@va_qattr] unfold let va_is_src_Mem64 (m:maddr) (s:va_state) = valid_maddr64 m s [@va_qattr] unfold let va_is_dst_Mem64 (m:maddr) (s:va_state) = valid_maddr64 m s [@va_qattr] unfold let va_is_src_vec_opr (v:vec_opr) (s:va_state) = True -[@va_qattr] unfold let va_is_dst_dst_vec_opr (v:dst_vec_opr) (s:va_state) = True +[@va_qattr] unfold let va_is_dst_vec_opr (v:vec_opr) (s:va_state) = True // Getters [@va_qattr] unfold let va_get_ok (s:va_state) : bool = s.ok @@ -123,7 +115,7 @@ unfold let va_opr_code_Mem64 (r:reg) (n:int) : maddr = va_upd_vec x (eval_vec x sM) sK [@va_qattr] unfold -let va_update_operand_dst_reg_opr (r:reg) (sM:va_state) (sK:va_state) : va_state = +let va_update_operand_reg_opr (r:reg) (sM:va_state) (sK:va_state) : va_state = va_update_reg r sM sK [@va_qattr] unfold @@ -131,7 +123,7 @@ let va_update_operand_Mem64 (m:maddr) (sM:va_state) (sK:va_state) : va_state = va_update_maddr m sM sK [@va_qattr] unfold -let va_update_operand_dst_vec_opr (x:vec) (sM:va_state) (sK:va_state) : va_state = +let va_update_operand_vec_opr (x:vec) (sM:va_state) (sK:va_state) : va_state = va_update_vec x sM sK // Constructors for va_codes diff --git a/fstar/code/arch/ppc64le/PPC64LE.Vale.InsBasic.vaf b/fstar/code/arch/ppc64le/PPC64LE.Vale.InsBasic.vaf index 67b1a4b5..dd84221b 100644 --- a/fstar/code/arch/ppc64le/PPC64LE.Vale.InsBasic.vaf +++ b/fstar/code/arch/ppc64le/PPC64LE.Vale.InsBasic.vaf @@ -58,34 +58,24 @@ var cr0:cr0_t {:state cr0()}; var xer:xer_t {:state xer()}; var mem:memory {:state mem()}; -// Input operands of general-purpose registers +// Operands of general-purpose registers operand_type reg_opr:nat64 := -| in r0 | in r1 | in r2 | in r3 -| in r4 | in r5 | in r6 | in r7 -| in r8 | in r9 | in r10 | in r11 -| in r12 | in r13 | in r14 | in r15 -| in r16 | in r17 | in r18 | in r19 -| in r20 | in r21 | in r22 | in r23 -| in r24 | in r25 | in r26 | in r27 -| in r28 | in r29 | in r30 | in r31 -; -// Output operands of general-purpose registers -operand_type dst_reg_opr:nat64 := -| out r0 | out r1 | out r2 | out r3 -| out r4 | out r5 | out r6 | out r7 -| out r8 | out r9 | out r10 | out r11 -| out r12 | out r13 | out r14 | out r15 -| out r16 | out r17 | out r18 | out r19 -| out r20 | out r21 | out r22 | out r23 -| out r24 | out r25 | out r26 | out r27 -| out r28 | out r29 | out r30 | out r31 +| inout r0 | inout r1 | inout r2 | inout r3 +| inout r4 | inout r5 | inout r6 | inout r7 +| inout r8 | inout r9 | inout r10 | inout r11 +| inout r12 | inout r13 | inout r14 | inout r15 +| inout r16 | inout r17 | inout r18 | inout r19 +| inout r20 | inout r21 | inout r22 | inout r23 +| inout r24 | inout r25 | inout r26 | inout r27 +| inout r28 | inout r29 | inout r30 | inout r31 ; + // 64-bit Memory operand operand_type Mem64(in address:reg_opr, inline offset:int):nat64; type simm16:Type(0) := int_range((-32768), 32767); type nsimm16:Type(0) := int_range((-32767), 32768); -procedure Move(out dst:dst_reg_opr, in src:reg_opr) +procedure Move(out dst:reg_opr, in src:reg_opr) {:public} {:instruction Ins(S.Move(dst, src))} ensures @@ -94,7 +84,7 @@ procedure Move(out dst:dst_reg_opr, in src:reg_opr) } // Load from 64-bit memory to general-purpose register -procedure Load64(out dst:dst_reg_opr, in src:Mem64) +procedure Load64(out dst:reg_opr, in src:Mem64) {:public} {:instruction Ins(S.Load64(dst, src))} ensures @@ -112,7 +102,7 @@ procedure Store64(in src:reg_opr, out dst:Mem64) } // Load Immediate to general-purpose register -procedure LoadImm64(out dst:dst_reg_opr, inline src:simm16) +procedure LoadImm64(out dst:reg_opr, inline src:simm16) {:public} {:instruction Ins(S.LoadImm64(dst, src))} ensures @@ -121,7 +111,7 @@ procedure LoadImm64(out dst:dst_reg_opr, inline src:simm16) } // Load address -procedure AddLa(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16) +procedure AddLa(out dst:reg_opr, in src1:reg_opr, inline src2:simm16) {:public} {:instruction Ins(S.AddLa(dst, src1, src2))} requires @@ -132,7 +122,7 @@ procedure AddLa(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16) } // Add two general-purpose registers. Assuming the result has no carry -procedure Add(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure Add(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.Add(dst, src1, src2))} requires @@ -143,7 +133,7 @@ procedure Add(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // Add two general-purpose registers with wrapping -procedure AddWrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure AddWrap(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.Add(dst, src1, src2))} ensures @@ -152,7 +142,7 @@ procedure AddWrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // Add general-purpose register amd immediate. Assuming the result has no carry -procedure AddImm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16) +procedure AddImm(out dst:reg_opr, in src1:reg_opr, inline src2:simm16) {:public} {:instruction Ins(S.AddImm(dst, src1, src2))} requires @@ -163,7 +153,7 @@ procedure AddImm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16) } // Add general-purpose register amd immediate with wrapping -procedure AddImmWrap(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16) +procedure AddImmWrap(out dst:reg_opr, in src1:reg_opr, inline src2:simm16) {:public} {:instruction Ins(S.AddImm(dst, src1, src2))} ensures @@ -172,7 +162,7 @@ procedure AddImmWrap(out dst:dst_reg_opr, in src1:reg_opr, inline src2:simm16) } // Add two general-purpose registers plus carry with wrapping and store status of carry occurrence in XER register -procedure AddExtended(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure AddExtended(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.AddExtended(dst, src1, src2))} modifies @@ -184,7 +174,7 @@ procedure AddExtended(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // Add two general-purpose registers plus overflow with wrapping and store status of overflow occurrence in XER register -procedure AddExtendedOV(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure AddExtendedOV(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.AddExtendedOV(dst, src1, src2))} modifies @@ -196,7 +186,7 @@ procedure AddExtendedOV(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // Subtract two general-purpose registers. Assuming the result has no borrow -procedure Sub(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure Sub(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.Sub(dst, src1, src2))} requires @@ -207,7 +197,7 @@ procedure Sub(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // Subtract two general-purpose registers with wrapping -procedure SubWrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure SubWrap(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.Sub(dst, src1, src2))} ensures @@ -216,7 +206,7 @@ procedure SubWrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // Subtract general-purpose register amd immediate. Assuming the result has no borrow -procedure SubImm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:nsimm16) +procedure SubImm(out dst:reg_opr, in src1:reg_opr, inline src2:nsimm16) {:public} {:instruction Ins(S.SubImm(dst, src1, src2))} requires @@ -227,7 +217,7 @@ procedure SubImm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:nsimm16) } // Subtract general-purpose register amd immediate with wrapping -procedure SubImmWrap(out dst:dst_reg_opr, in src1:reg_opr, inline src2:nsimm16) +procedure SubImmWrap(out dst:reg_opr, in src1:reg_opr, inline src2:nsimm16) {:public} {:instruction Ins(S.SubImm(dst, src1, src2))} ensures @@ -236,7 +226,7 @@ procedure SubImmWrap(out dst:dst_reg_opr, in src1:reg_opr, inline src2:nsimm16) } // Mutiply two general-purpose registers. Assuming the product fits in 64-bit -procedure MulLow64(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure MulLow64(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.MulLow64(dst, src1, src2))} requires @@ -247,7 +237,7 @@ procedure MulLow64(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // Mutiply two general-purpose registers ans store the low 64-bit of product in the destination register -procedure MulLow64Wrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure MulLow64Wrap(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.MulLow64(dst, src1, src2))} ensures @@ -256,7 +246,7 @@ procedure MulLow64Wrap(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // Mutiply two general-purpose registers ans store the high 64-bit of product in the destination register -procedure MulHigh64U(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure MulHigh64U(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.MulHigh64U(dst, src1, src2))} ensures @@ -265,7 +255,7 @@ procedure MulHigh64U(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // XOR operation of two general-purpose registers -procedure Xor(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure Xor(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.Xor(dst, src1, src2))} ensures @@ -274,7 +264,7 @@ procedure Xor(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // AND operation of two general-purpose registers -procedure And(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) +procedure And(out dst:reg_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.And(dst, src1, src2))} ensures @@ -283,7 +273,7 @@ procedure And(out dst:dst_reg_opr, in src1:reg_opr, in src2:reg_opr) } // Shift right general-purpose register with immediate bit value -procedure Sr64Imm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:bits64) +procedure Sr64Imm(out dst:reg_opr, in src1:reg_opr, inline src2:bits64) {:public} {:instruction Ins(S.Sr64Imm(dst, src1, src2))} ensures @@ -292,7 +282,7 @@ procedure Sr64Imm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:bits64) } // Shift left general-purpose register with immediate bit value -procedure Sl64Imm(out dst:dst_reg_opr, in src1:reg_opr, inline src2:bits64) +procedure Sl64Imm(out dst:reg_opr, in src1:reg_opr, inline src2:bits64) {:public} {:instruction Ins(S.Sl64Imm(dst, src1, src2))} ensures diff --git a/fstar/code/arch/ppc64le/PPC64LE.Vale.InsMem.vaf b/fstar/code/arch/ppc64le/PPC64LE.Vale.InsMem.vaf index 50ac6263..7b844e2a 100644 --- a/fstar/code/arch/ppc64le/PPC64LE.Vale.InsMem.vaf +++ b/fstar/code/arch/ppc64le/PPC64LE.Vale.InsMem.vaf @@ -46,7 +46,7 @@ procedure Mem64_lemma(ghost address:reg_opr, ghost offset:int) } // Load from 64-bit memory to general-purpose register -procedure MemLoad64(out dst:dst_reg_opr, in src:reg_opr, inline offset:int) +procedure MemLoad64(out dst:reg_opr, in src:reg_opr, inline offset:int) {:public} reads mem; diff --git a/fstar/code/arch/ppc64le/PPC64LE.Vale.InsVector.vaf b/fstar/code/arch/ppc64le/PPC64LE.Vale.InsVector.vaf index 8c94cc6f..79413c53 100644 --- a/fstar/code/arch/ppc64le/PPC64LE.Vale.InsVector.vaf +++ b/fstar/code/arch/ppc64le/PPC64LE.Vale.InsVector.vaf @@ -73,30 +73,20 @@ var v29:quad32 {:state vec(29)}; var v30:quad32 {:state vec(30)}; var v31:quad32 {:state vec(31)}; -// Input operands of vector registers +// Operands of vector registers operand_type vec_opr:quad32 := -| in v0 | in v1 | in v2 | in v3 -| in v4 | in v5 | in v6 | in v7 -| in v8 | in v9 | in v10 | in v11 -| in v12 | in v13 | in v14 | in v15 -| in v16 | in v17 | in v18 | in v19 -| in v20 | in v21 | in v22 | in v23 -| in v24 | in v25 | in v26 | in v27 -| in v28 | in v29 | in v30 | in v31 -; -// Output operands of vector registers -operand_type dst_vec_opr:quad32 := -| out v0 | out v1 | out v2 | out v3 | out v4 -| out v5 | out v6 | out v7 | out v8 | out v9 -| out v10 | out v11 | out v12 | out v13 | out v14 -| out v15 | out v16 | out v17 | out v18 | out v19 -| out v20 | out v21 | out v22 | out v23 | out v24 -| out v25 | out v26 | out v27 | out v28 | out v29 -| out v30 | out v31 +| inout v0 | inout v1 | inout v2 | inout v3 +| inout v4 | inout v5 | inout v6 | inout v7 +| inout v8 | inout v9 | inout v10 | inout v11 +| inout v12 | inout v13 | inout v14 | inout v15 +| inout v16 | inout v17 | inout v18 | inout v19 +| inout v20 | inout v21 | inout v22 | inout v23 +| inout v24 | inout v25 | inout v26 | inout v27 +| inout v28 | inout v29 | inout v30 | inout v31 ; // Move high 64-bit of vector register to general-purpose register -procedure Mfvsrd(out dst:dst_reg_opr, in src:vec_opr) +procedure Mfvsrd(out dst:reg_opr, in src:vec_opr) {:public} {:instruction Ins(S.Mfvsrd(dst, src))} ensures @@ -105,7 +95,7 @@ procedure Mfvsrd(out dst:dst_reg_opr, in src:vec_opr) } // Move low 64-bit of vector register to general-purpose register -procedure Mfvsrld(out dst:dst_reg_opr, in src:vec_opr) +procedure Mfvsrld(out dst:reg_opr, in src:vec_opr) {:public} {:instruction Ins(S.Mfvsrld(dst, src))} ensures @@ -114,7 +104,7 @@ procedure Mfvsrld(out dst:dst_reg_opr, in src:vec_opr) } // Move joint of two general-purpose registers to vector register -procedure Mtvsrdd(out dst:dst_vec_opr, in src1:reg_opr, in src2:reg_opr) +procedure Mtvsrdd(out dst:vec_opr, in src1:reg_opr, in src2:reg_opr) {:public} {:instruction Ins(S.Mtvsrdd(dst, src1, src2))} ensures @@ -124,7 +114,7 @@ procedure Mtvsrdd(out dst:dst_vec_opr, in src1:reg_opr, in src2:reg_opr) } // XOR operation of two vector registers -procedure Vxor(out dst:dst_vec_opr, in src1:vec_opr, in src2:vec_opr) +procedure Vxor(out dst:vec_opr, in src1:vec_opr, in src2:vec_opr) {:public} {:instruction Ins(S.Vxor(dst, src1, src2))} ensures @@ -133,7 +123,7 @@ procedure Vxor(out dst:dst_vec_opr, in src1:vec_opr, in src2:vec_opr) } // Shift left word elements of vector register with correspinding bit values in word elements of vector register -procedure Vslw(out dst:dst_vec_opr, in src1:vec_opr, in src2:vec_opr) +procedure Vslw(out dst:vec_opr, in src1:vec_opr, in src2:vec_opr) {:public} {:instruction Ins(S.Vslw(dst, src1, src2))} ensures @@ -146,7 +136,7 @@ procedure Vslw(out dst:dst_vec_opr, in src1:vec_opr, in src2:vec_opr) } // Shift right word elements of vector register with corresponding bit values in word elements of vector register -procedure Vsrw(out dst:dst_vec_opr, in src1:vec_opr, in src2:vec_opr) +procedure Vsrw(out dst:vec_opr, in src1:vec_opr, in src2:vec_opr) {:public} {:instruction Ins(S.Vsrw(dst, src1, src2))} ensures @@ -159,7 +149,7 @@ procedure Vsrw(out dst:dst_vec_opr, in src1:vec_opr, in src2:vec_opr) } // Compare equal word elements of vector register and store either ones or zeros in the corresponding elements of destination register -procedure Vcmpequw(out dst:dst_vec_opr, in src1:vec_opr, in src2:vec_opr) +procedure Vcmpequw(out dst:vec_opr, in src1:vec_opr, in src2:vec_opr) {:public} {:instruction Ins(S.Vcmpequw(dst, src1, src2))} ensures @@ -172,10 +162,14 @@ procedure Vcmpequw(out dst:dst_vec_opr, in src1:vec_opr, in src2:vec_opr) } // Joint of last one word of vector register with first 3 words of vector register -procedure Vsldoi4(out dst:dst_vec_opr, in src1:vec_opr, in src2:vec_opr) +procedure Vsldoi(out dst:vec_opr, in src1:vec_opr, in src2:vec_opr, inline count:quad32bytes) {:public} - {:instruction Ins(S.Vsldoi(dst, src1, src2, 4))} + {:instruction Ins(S.Vsldoi(dst, src1, src2, count))} + requires + count == 4 || count == 8 || count == 12; ensures - dst == old(Mkfour(src2.hi3, src1.lo0, src1.lo1, src1.hi2)); + count == 4 ==> dst == old(Mkfour(src2.hi3, src1.lo0, src1.lo1, src1.hi2)); + count == 8 ==> dst == old(Mkfour(src2.hi2, src2.hi3, src1.lo0, src1.lo1)); + count == 12 ==> dst == old(Mkfour(src2.lo1, src2.hi2, src2.hi3, src1.lo0)); { } diff --git a/fstar/specs/hardware/PPC64LE.Semantics_s.fst b/fstar/specs/hardware/PPC64LE.Semantics_s.fst index 2c1a03be..3fbb3a41 100644 --- a/fstar/specs/hardware/PPC64LE.Semantics_s.fst +++ b/fstar/specs/hardware/PPC64LE.Semantics_s.fst @@ -290,11 +290,13 @@ let eval_ins (ins:ins) : st unit = update_vec dst eq_val | Vsldoi dst src1 src2 count -> - check (fun s -> count = 4);? // We only spec the one very special case we need + check (fun s -> (count = 4 || count = 8 || count = 12));; // We only spec the one very special case we need let src1_q = eval_vec src1 s in let src2_q = eval_vec src2 s in - let shifted_vec = Mkfour src2_q.hi3 src1_q.lo0 src1_q.lo1 src1_q.hi2 in - update_vec dst shifted_vec + if count = 4 then update_vec dst (Mkfour src2_q.hi3 src1_q.lo0 src1_q.lo1 src1_q.hi2) + else if count = 8 then update_vec dst (Mkfour src2_q.hi2 src2_q.hi3 src1_q.lo0 src1_q.lo1) + else if count = 12 then update_vec dst (Mkfour src2_q.lo1 src2_q.hi2 src2_q.hi3 src1_q.lo0) + else fail let run_ocmp (s:state) (c:ocmp) : state & bool = let s = run (check (valid_ocmp c)) s in