Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: rewrite semantics to not have pattern match on structure #171

Merged
merged 5 commits into from
Sep 20, 2024

Conversation

bollu
Copy link
Collaborator

@bollu bollu commented Sep 19, 2024

Issues:

This works around leanprover/lean4#5388, and removes uses of simp (config := { ground := true }) ... This makes our proof states cleaner, since we no longer see proof states involving Decidable.rec .... Peeled from #168

Testing:

What tests have been run? Did make all succeed for your changes? Was
conformance testing successful on an Aarch64 machine?

make all succeeded, conformance succeeded.

License:

By submitting this pull request, I confirm that my contribution is
made under the terms of the Apache 2.0 license.

This works around leanprover/lean4#5388,
and removes uses of `simp (config := { ground := true }) ..`.
@shigoel
Copy link
Collaborator

shigoel commented Sep 19, 2024

BTW, AddWithCarry is also used here:

./Insts/DPR/Add_sub_shifted_reg.lean:    let (result, pstate) := AddWithCarry operand1 operand2 carry
./Insts/DPR/Add_sub_carry.lean:    let (result, pstate) := AddWithCarry operand1 operand2 (read_flag PFlag.C s)

@bollu
Copy link
Collaborator Author

bollu commented Sep 20, 2024

BTW, AddWithCarry is also used here:

./Insts/DPR/Add_sub_shifted_reg.lean:    let (result, pstate) := AddWithCarry operand1 operand2 carry
./Insts/DPR/Add_sub_carry.lean:    let (result, pstate) := AddWithCarry operand1 operand2 (read_flag PFlag.C s)

@shigoel I audited these, and they're fine, because their arguments operand2 and carry don't come from a patterm match of an if...then...else:

30-                        else
31-                          (0#1, imm)
32-    let carry := carryInAndOperand2.fst
33-    let operand2 := carryInAndOperand2.snd
34-    let operand2         := BitVec.zeroExtend datasize operand2
35:    let (result, pstate) := AddWithCarry operand1 operand2 carry
36-    -- State Updates
37-    let s'            := write_pc ((read_pc s) + 4#64) s
38-    let s'            := if setflags then write_pstate pstate s' else s'
39-    let s'            := if inst.Rd = 31#5 ∧ ¬ setflags
40-                         then write_gpr datasize inst.Rd result s'

Insts/DPR/Add_sub_carry.lean
22-    let operand2      := read_gpr_zr datasize inst.Rm s
23-    let operand2      := if sub_op then
24-                          ~~~operand2
25-                         else
26-                          operand2
27:    let (result, pstate) := AddWithCarry operand1 operand2 (read_flag PFlag.C s)
28-    -- State Updates
29-    let s'            := write_pc ((read_pc s) + 4#64) s
30-    let s'            := if setflags then write_pstate pstate s' else s'
31-    let s'            := write_gpr_zr datasize inst.Rd result s'
32-    s'

Insts/DPR/Add_sub_shifted_reg.lean
27-    let operand1 := read_gpr_zr datasize inst.Rn s
28-    let operand2_unshifted := read_gpr_zr datasize inst.Rm s
29-    let operand2 := shift_reg operand2_unshifted shift_type inst.imm6
30-    let operand2 := if sub_op then ~~~operand2 else operand2
31-    let carry := if sub_op then 1 else 0
32:    let (result, pstate) := AddWithCarry operand1 operand2 carry
33-    -- State Updates
34-    let s'            := write_pc ((read_pc s) + 4#64) s
35-    let s'            := if setflags then write_pstate pstate s' else s'
36-    let s'            := write_gpr_zr datasize inst.Rd result s'
37-    s'

Consider the diff:

-    let (carry_in, operand2)
+    let carryInAndOperand2
                       := if sub_op then
                           (1#1, ~~~imm)
                         else
                           (0#1, imm)
+    let carry := carryInAndOperand2.fst
+    let operand2 := carryInAndOperand2.snd
     let operand2         := BitVec.zeroExtend datasize operand2
-    let (result, pstate) := AddWithCarry operand1 operand2 carry_in
+    let (result, pstate) := AddWithCarry operand1 operand2 carry

The issue is that we were pattern matching to extract (carry_in, operand2) from the if ... then ... else which elaborated poorly. The culprit is this pattern match, not so much the use of AddWithCarry. AddWithCarry would then try to use the carry, but any function that used carry would have lead to a problem.

@bollu
Copy link
Collaborator Author

bollu commented Sep 20, 2024

@shigoel updated.

@shigoel shigoel merged commit f69c71f into main Sep 20, 2024
4 checks passed
@shigoel shigoel deleted the adc-bitvec-rules branch September 20, 2024 21:24
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants