Lean: add support for vectors and register vectors #911

lfrenot · 2025-01-27T11:57:55Z

This also updates the lean version to have the recent updates to Vector, and adds neq and if then else support to have proper access functions.

github-actions · 2025-01-27T12:21:47Z

Test Results

12 files ±0 24 suites ±0 0s ⏱️ ±0s
754 tests +3 754 ✅ +3 0 💤 ±0 0 ❌ ±0
2 498 runs +3 2 498 ✅ +3 0 💤 ±0 0 ❌ ±0

Results for commit 2bf1cc8. ± Comparison against base commit 68c1009.

♻️ This comment has been updated with latest results.

bacam · 2025-01-27T13:58:28Z

src/sail_lean_backend/pretty_print_lean.ml

@@ -377,7 +380,9 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
      let d_args = List.map d_of_arg args in
      let fn_monadic = not (Effects.function_is_pure f ctx.global.effect_info) in
      nest 2 (wrap_with_pure (as_monadic && fn_monadic) (parens (flow (break 1) (d_id :: d_args))))
-  | E_vector vals -> failwith "vector found"
+  | E_vector vals ->
+      let vals = List.map (doc_exp false ctx) vals in


Does this work for effectful subexpressions? Tuples use d_of_arg, for example.

I have not tested that, but using the same method as tuples is probably correct, I'll change it accordingly

ineol · 2025-01-27T14:48:05Z

lib/flow.sail

@@ -75,7 +75,7 @@ val eq_int = pure {ocaml: "eq_int", interpreter: "eq_int", lem: "eq", coq: "Z.eq

 val eq_bool = pure {ocaml: "eq_bool", interpreter: "eq_bool", lem: "eq", coq: "Bool.eqb", lean: "Eq", _: "eq_bool"} : (bool, bool) -> bool

-val neq_int = pure {lem: "neq"} : forall 'n 'm. (int('n), int('m)) -> bool('n != 'm)
+val neq_int = pure {lem: "neq", lean: "¬ Eq"} : forall 'n 'm. (int('n), int('m)) -> bool('n != 'm)


Could we use Ne instead?

ineol · 2025-01-27T14:49:58Z

lib/vector.sail

@@ -175,6 +175,7 @@ val bitvector_access = pure {
  interpreter: "access",
  lem: "access_vec_dec",
  coq: "access_vec_dec",
+  lean: "vectorAccess",


Hmmm... shouldn't bitvector access use a bitvector operation, like bv.getLsbD i instead of a vecctor operation?

Right, these edits weren't needed

ineol · 2025-01-27T14:50:04Z

lib/vector.sail

@@ -183,6 +184,7 @@ val bitvector_access = pure {
  interpreter: "access_inc",
  lem: "access_vec_inc",
  coq: "access_vec_inc",
+  lean: "vectorAccess",


Same as above

ineol · 2025-01-27T14:53:59Z

test/lean/register_vector.expected.lean

+def GPRs : Vector (RegisterRef RegisterType (BitVec 64)) 31 :=
+[Reg R30, Reg R29, Reg R28, Reg R27, Reg R26, Reg R25, Reg R24, Reg R23, Reg R22, Reg R21, Reg R20,
+  Reg R19, Reg R18, Reg R17, Reg R16, Reg R15, Reg R14, Reg R13, Reg R12, Reg R11, Reg R10, Reg R9,
+  Reg R8, Reg R7, Reg R6, Reg R5, Reg R4, Reg R3, Reg R2, Reg R1, Reg R0].toArray.toVector


I think you can use this for vector literals. #v[a, b, c] but I haven't tried

Thanks that's better

ineol · 2025-01-27T16:21:33Z

FYI, I added this function and it worked fine!

function monad_test(r : reg_index) -> bit = {
  if rX(r) == 0x0000000000000000 then
    bitone
  else if rX(r) == 0x0000000000000001 then
    bitone
  else
    bitzero
}

ineol

Looks good to me now!

ineol · 2025-01-27T14:57:22Z

test/lean/register_vector.sail

+
+val rX : reg_index -> bits(64)
+
+function rX(n) = {


I would be good to have a test with else if to exercise this part of the translation. Also, example with monadic things in the condition and in the branches (at least to see where we're at)

We could also do the whole if else thing in a separate PR

I've added Leo's monad_test function to register_vector.sail and a separate ite.sail test file for additional things.

javra · 2025-01-27T16:36:41Z

src/sail_lean_backend/pretty_print_lean.ml

  | _ -> failwith ("Expression " ^ string_of_exp_con full_exp ^ " " ^ string_of_exp full_exp ^ " not translatable yet.")

 and doc_fexp with_arrow ctx (FE_aux (FE_fexp (field, e), _)) =
  doc_id_ctor field ^^ string " := " ^^ wrap_with_left_arrow with_arrow (doc_exp false ctx e)

+and if_exp (ctxt : context) (full_env : env) (full_typ : typ) (elseif : bool) (as_monadic : bool) c t e =
+  let if_pp = string (if elseif then "else if" else "if") in
+  let c_pp = doc_exp as_monadic ctxt c in


I don't think that's right. You need to check whether c is monadic and use that as an argument to both the call of doc_exp and then add a call to wrap_with_left_arrow to pull the monadic value out in this case.

This is what I have locally as a minimal implementation, not thoroughly tested though:

| E_if (i, t, e) -> let condition_monadic = effectful (effect_of i) in nest 2 (string "if" ^^ space ^^ wrap_with_left_arrow condition_monadic (doc_exp condition_monadic ctx i)) ^^ hardline ^^ nest 2 (string "then" ^^ space ^^ doc_exp as_monadic ctx t) ^^ hardline ^^ nest 2 (string "else" ^^ space ^^ doc_exp as_monadic ctx e)

Yes you're correct, I've changed it to something closer to your implementation

javra · 2025-01-27T16:38:46Z

test/lean/register_vector.expected.lean

+  default := .Reg _PC
+
+def GPRs : Vector (RegisterRef RegisterType (BitVec 64)) 31 :=
+#v[Reg R30, Reg R29, Reg R28, Reg R27, Reg R26, Reg R25, Reg R24, Reg R23, Reg R22, Reg R21, Reg R20,


Indentation

javra · 2025-01-27T16:39:46Z

test/lean/register_vector.expected.lean

+
+open Sail
+
+def reg_index := Nat


I'd rather have abbrev RegIndex := Nat here. The def instead of abbrev will make the new type have no usable instances on it.

This is a bit out of the scope of this PR, but I have changed it

javra · 2025-01-27T16:42:40Z

src/sail_lean_backend/pretty_print_lean.ml

+        string "else" ^/^ doc_exp as_monadic ctxt (E_aux (E_internal_plet (pat, exp1, exp2), ann))
+    | _ -> prefix 2 1 (string "else") (doc_exp as_monadic ctxt e)
+  in
+  prefix 2 1 (soft_surround 2 1 if_pp c_pp (string "then")) t_pp ^^ break 1 ^^ else_pp


Is this copied over from the Coq printer? If so maybe mark it as such so we can improve it later.

Yes it was, it's not here anymore, but I have marked the other part that was copied from the Coq printer

javra · 2025-01-27T16:52:22Z

src/sail_lean_backend/sail_plugin_lean.ml

@@ -73,7 +73,7 @@ let opt_lean_output_dir : string option ref = ref None

 let opt_lean_force_output : bool ref = ref false

-let lean_version : string = "lean4:nightly-2024-09-25"
+let lean_version : string = "lean4:nightly-2025-01-22"


Why was this bumped?

It was bumped because nightly-2024-09-25 used a different implementation of Vectors

This also adds a test file for ite, and an additional test in register_vector

javra · 2025-01-28T15:11:59Z

src/sail_lean_backend/pretty_print_lean.ml

@@ -413,6 +418,14 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
      | LE_deref e' -> string "writeRegRef " ^^ doc_exp false ctx e' ^^ space ^^ doc_exp false ctx e
      | _ -> failwith ("assign " ^ string_of_lexp le ^ "not implemented yet")
    )
+  | E_if (i, t, e) ->
+      let statements_monadic = as_monadic || effectful (effect_of t) || effectful (effect_of e) in
+      nest 2 (string "if" ^^ space ^^ nest 1 (doc_exp false ctx i))


I think this still ignores the monadicity of the condition?

But yes, let's ignore that for now and fix it when we need to fix it.

It does because the condition should never be monadic (it should be a Bool and not a SailM Bool), instead the responsibility is on doc_exp, see line 352

The responsibility needs to be moved like that, because we want to be able to handle both if (Eq (← (rX r)) 0) and if (← readReg B)

add support for vectors and register vectors

Loading
Loading status checks…

16a78ae

lfrenot requested review from bacam, javra and ineol January 27, 2025 11:59

bacam approved these changes Jan 27, 2025

View reviewed changes

Fixing for effectful arguments of vectors

Loading
Loading status checks…

cd67ee8

ineol suggested changes Jan 27, 2025

View reviewed changes

lfrenot added 2 commits January 27, 2025 15:10

Leo edits

Loading
Loading status checks…

9301b62

removing a line that was committed by error

Loading
Loading status checks…

b54f179

ineol approved these changes Jan 27, 2025

View reviewed changes

javra reviewed Jan 27, 2025

View reviewed changes

lfrenot added 4 commits January 28, 2025 14:48

Fixing ite

f9f93cd

This also adds a test file for ite, and an additional test in register_vector

doc_val indentation fix

65fe108

Type abbrevs to abbrev

Loading
Loading status checks…

cad2ca9

formatting

Loading
Loading status checks…

2bf1cc8

javra reviewed Jan 28, 2025

View reviewed changes

bacam merged commit dde655a into rems-project:sail2 Jan 28, 2025
3 checks passed

lfrenot added a commit to lfrenot/sail that referenced this pull request Jan 29, 2025

Remove "Remove when rems-project#911 is merged"

Loading
Loading status checks…

c7f4879

lfrenot mentioned this pull request Jan 29, 2025

Lean: Remove "Remove when #911 is merged" #916

Merged

bacam pushed a commit that referenced this pull request Jan 29, 2025

Remove "Remove when #911 is merged" (#916)

Loading
Loading status checks…

87fb0c3

lfrenot deleted the lean-vector branch February 3, 2025 10:14

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Lean: add support for vectors and register vectors #911

Lean: add support for vectors and register vectors #911

lfrenot commented Jan 27, 2025

github-actions bot commented Jan 27, 2025 •

edited

Loading

bacam Jan 27, 2025

lfrenot Jan 27, 2025

ineol Jan 27, 2025

lfrenot Jan 27, 2025

ineol Jan 27, 2025

lfrenot Jan 27, 2025

ineol Jan 27, 2025

ineol Jan 27, 2025

lfrenot Jan 27, 2025

ineol commented Jan 27, 2025 •

edited

Loading

ineol left a comment

ineol Jan 27, 2025

javra Jan 27, 2025

lfrenot Jan 28, 2025

javra Jan 27, 2025

javra Jan 27, 2025

lfrenot Jan 28, 2025

javra Jan 27, 2025

lfrenot Jan 28, 2025

javra Jan 27, 2025

lfrenot Jan 28, 2025

javra Jan 27, 2025

lfrenot Jan 28, 2025

javra Jan 27, 2025

lfrenot Jan 28, 2025

javra Jan 28, 2025

javra Jan 28, 2025

lfrenot Jan 28, 2025 •

edited

Loading

Lean: add support for vectors and register vectors #911

Lean: add support for vectors and register vectors #911

Conversation

lfrenot commented Jan 27, 2025

github-actions bot commented Jan 27, 2025 • edited Loading

Test Results

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ineol commented Jan 27, 2025 • edited Loading

ineol left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lfrenot Jan 28, 2025 • edited Loading

Choose a reason for hiding this comment

github-actions bot commented Jan 27, 2025 •

edited

Loading

ineol commented Jan 27, 2025 •

edited

Loading

lfrenot Jan 28, 2025 •

edited

Loading