Add support for `dyn` in backends

[maximebuyse]

dyn was added to the engine in https://github.com/hacspec/hax/issues/296 but it still need to be treated properly in the f* backend.

dyn (A + B<C>) is translated as dyn 2 (fun z -> A z) (fun z -> B z C). We still need to:

• define dyn in f*
• resolve method calls for instances of dyn

[W95Psp]

A nice encoding in F* could be as follows:

noeq type dyn (traits: Type0 -> Type) =
  { typ: Type0
  ; value: typ
  ; interfaces: traits typ
  }

Usage example:

class foo x = {
  method: x -> int
}

let f (x: dyn (fun self -> foo self & other_trait self arg0 ... argN)) =
  let (_, _) = x.interfaces in
  method x.value

This encoding requires:

• a slight modification in the F* backend of the shape of the dyns we output;
• insert let (_, ..., _) = e.interfaces in before any calls on methods held in dyns

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[github-actions[bot]]

This issue has been closed due to a lack of activity since being marked as stale. If you believe this issue is still relevant, please reopen it with an update or comment.

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.