From 3607f934d32427c5aa63352046a9b379a79e6923 Mon Sep 17 00:00:00 2001 From: Siddharth Date: Sat, 28 Sep 2024 12:47:30 -0500 Subject: [PATCH] chore: add commented set_option trace.profiler true for easy logging (#202) ### Description: Add Lean debug logging commands into MemcpyVCG. Disabled by default to prevent verbosity, but present in the codebase to allow easy benchmarking. ### Testing: What tests have been run? Did `make all` succeed for your changes? Was conformance testing successful on an Aarch64 machine? Conformance succeeded ### License: By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license. Co-authored-by: Shilpi Goel --- Proofs/Experiments/Memcpy/MemCpyVCG.lean | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/Proofs/Experiments/Memcpy/MemCpyVCG.lean b/Proofs/Experiments/Memcpy/MemCpyVCG.lean index 87af5e43..76eeff7e 100644 --- a/Proofs/Experiments/Memcpy/MemCpyVCG.lean +++ b/Proofs/Experiments/Memcpy/MemCpyVCG.lean @@ -441,6 +441,8 @@ end CutTheorems section PartialCorrectness -- set_option skip_proof.skip true in +-- set_option trace.profiler true in +-- set_option profiler true in set_option maxHeartbeats 0 in theorem Memcpy.extracted_2 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) @@ -482,6 +484,8 @@ theorem Memcpy.extracted_2 (s0 si : ArmState) -- set_option skip_proof.skip true in set_option maxHeartbeats 0 in +-- set_option trace.profiler true in +-- set_option profiler true in theorem Memcpy.extracted_0 (s0 si : ArmState) (h_si_x0_nonzero : si.x0 ≠ 0) (h_s0_x1 : s0.x1 + 0x10#64 * (s0.x0 - si.x0) + 0x10#64 = s0.x1 + 0x10#64 * (s0.x0 - (si.x0 - 0x1#64))) @@ -550,6 +554,9 @@ theorem Memcpy.extracted_0 (s0 si : ArmState) } · intros n addr hsep apply Memcpy.extracted_2 <;> assumption + +-- set_option trace.profiler true in +-- set_option profiler true in theorem partial_correctness : PartialCorrectness ArmState := by apply Correctness.partial_correctness_from_assertions