Search results

provenance tracking for memory regions

Status: Open.

#162 In leanprover/LNSym;

· bollu opened on Sep 18, 2024

<code>simp_mem</code> failure with <code>GCMGmultV8</code>

Status: Open.

#154 In leanprover/LNSym;

· shigoel opened on Sep 13, 2024

Use Vector type for AES-GCM specification

Status: Open.

#146 In leanprover/LNSym;

· pennyannn opened on Sep 6, 2024

Add sections into Arm/Insts/Common.lean

Status: Open.

#139 In leanprover/LNSym;

· bollu opened on Sep 4, 2024

Elab and delab for ARM instructions

Status: Open.

#121 In leanprover/LNSym;

· bollu opened on Aug 26, 2024

Experiment: Use r for accessing the program field, which solves program being public.

Status: Open.

#55 In leanprover/LNSym;

· bollu opened on Aug 2, 2024

ELF Parser in Lean

help wantedExtra attention is neededExtra attention is needed

Status: Open.

#18 In leanprover/LNSym;

· shigoel opened on Feb 22, 2024