Fix handling of logical indexing with final borrows

creusot/src/backend/program.rs

@@ -670,8 +670,7 @@ pub(crate) fn borrow_generated_id<V: std::fmt::Debug, T: std::fmt::Debug>(
             | ProjectionElem::ConstantIndex { .. }
             | ProjectionElem::Subslice { .. }
             | ProjectionElem::OpaqueCast(_) => {
-                // Should not appear, ruled out in `NotFinalPlaces::is_final_at`
-                todo!("{proj:?} not supported as final")
+                // Should only appear in logic, so we can ignore them.
             }
         }
     }

creusot/src/backend/term.rs

@@ -259,13 +259,10 @@ impl<'tcx, N: Namer<'tcx>> Lower<'_, 'tcx, N> {
             TermKind::Reborrow { cur, fin, term, projection } => {
                 let inner = self.lower_term(*term);
                 let borrow_id = borrow_generated_id(inner, &projection);
-                Exp::Record {
-                    fields: vec![
-                        ("current".into(), self.lower_term(*cur)),
-                        ("final".into(), self.lower_term(*fin)),
-                        ("addr".into(), borrow_id),
-                    ],
-                }
+                Exp::Call(
+                    Box::new(Exp::QVar("Borrow.borrow_logic".into(), Purity::Logic)),
+                    vec![self.lower_term(*cur), self.lower_term(*fin), borrow_id],
+                )
             }
             TermKind::Assert { cond } => {
                 let cond = self.lower_term(&*cond);

creusot/src/translation/pearlite.rs

@@ -918,13 +918,40 @@ impl<'a, 'tcx> ThirTerm<'a, 'tcx> {
                 Ok(res)
             }
             ExprKind::Deref { arg } => {
+                // Detect * ghost_deref & and treat that as a single 'projection'
+                if self.is_ghost_deref(*arg) {
+                    let ExprKind::Call { args, .. } = &self.thir[*arg].kind else { unreachable!() };
+                    let ExprKind::Borrow { borrow_kind: BorrowKind::Shared, arg } = self.thir[args[0]].kind else { unreachable!() };
+
+                    let (term, projections) = self.logical_reborrow_inner_project(arg)?;
+                    return Ok((
+                        term,
+                        projections,
+                    ));
+                };
+
                 let inner = self.expr_term(*arg)?;
-                if let TermKind::Var(_) = inner.kind {}
                 Ok((inner, Vec::new()))
             }
-            _ => Err(Error::new(
+            ExprKind::Call { ty: fn_ty, args, .. } if fn_ty.is_fn() => {
+                let index_logic_method = self.ctx.get_diagnostic_item(Symbol::intern("index_logic_method")).unwrap();
+
+                let TyKind::FnDef(id,_) = fn_ty.kind() else { panic!("expected function type") };
+
+                let (term, mut projections) = self.logical_reborrow_inner_project(args[0])?;
+
+                if id == &index_logic_method {
+                    let index = self.expr_term(args[1])?;
+
+                    projections.push(ProjectionElem::Index(index));
+                    Ok((term, projections))
+                } else {
+                    return Err(Error::new(span, format!("unsupported projection {id:?}")));
+                }
+            }
+            e => Err(Error::new(
                 span,
-                "unsupported logical reborrow, only simple field projections are supproted, sorry",
+                format!("unsupported logical reborrow {e:?}, only simple field projections are supported"),
             )),
         }
     }