anchor.diff:      Syntax.string_of_mlpath p = "FStar.HyperStack.ST.mmmref"
       ->
         TBuf (translate_type env arg)
  +  | MLTY_Named ([arg; _; _], p) when
  +    Syntax.string_of_mlpath p = "LowStar.Monotonic.Buffer.mbuffer" -> TBuf (translate_type env arg)
     | MLTY_Named ([arg], p) when
       Syntax.string_of_mlpath p = "LowStar.Buffer.buffer" ||
       Syntax.string_of_mlpath p = "FStar.Buffer.buffer" ||
  
positive.code:       EBufCreate (Stack, translate_expr env init, EConstant (UInt32, "1"))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e2 ])
      when (string_of_mlpath p = "FStar.Buffer.createL" || string_of_mlpath p = "LowStar.Buffer.alloca_of_list") ->
        EBufCreateL (Stack, List.map (translate_expr env) (list_elements e2))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; e2 ])
      when string_of_mlpath p = "LowStar.Buffer.gcmalloc_of_list" ->
        EBufCreateL (Eternal, List.map (translate_expr env) (list_elements e2))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ _rid; init ])
  
negative.code:       EBufCreate (ManuallyManaged, translate_expr env init, EConstant (UInt32, "1"))
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _e0; e1; e2 ])
      when (string_of_mlpath p = "FStar.Buffer.rcreate_mm" || string_of_mlpath p = "LowStar.Buffer.malloc" ||
            string_of_mlpath p = "LowStar.Monotonic.Buffer.mmalloc") ->
        EBufCreate (ManuallyManaged, translate_expr env e1, translate_expr env e2)
  
    (* Only manually-managed references and buffers can be freed. *)
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e2 ]) when (string_of_mlpath p = "FStar.HyperStack.ST.rfree") ->
        EBufFree (translate_expr env e2)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e2 ]) when (string_of_mlpath p = "FStar.Buffer.rfree" || string_of_mlpath p = "LowStar.Monotonic.Buffer.free") ->
        EBufFree (translate_expr env e2)
  
    (* Generic buffer operations. *)
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; _e3 ]) when (string_of_mlpath p = "FStar.Buffer.sub" || string_of_mlpath p = "LowStar.Buffer.sub") ->
        EBufSub (translate_expr env e1, translate_expr env e2)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; _e3; _e4 ]) when string_of_mlpath p = "LowStar.Monotonic.Buffer.msub" ->
        EBufSub (translate_expr env e1, translate_expr env e2)
  
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when (string_of_mlpath p = "FStar.Buffer.join") ->
        (translate_expr env e1)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when (string_of_mlpath p = "FStar.Buffer.offset" || string_of_mlpath p = "LowStar.Buffer.offset") ->
        EBufSub (translate_expr env e1, translate_expr env e2)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; _e3 ]) when string_of_mlpath p = "LowStar.Monotonic.Buffer.moffset" ->
        EBufSub (translate_expr env e1, translate_expr env e2)
  
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; e3 ])
      when string_of_mlpath p = "FStar.Buffer.upd" || string_of_mlpath p = "FStar.Buffer.op_Array_Assignment"
      || string_of_mlpath p = "LowStar.Monotonic.Buffer.upd'" ->
        EBufWrite (translate_expr env e1, translate_expr env e2, translate_expr env e3)
    | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ])
      when string_of_mlpath p = "FStar.HyperStack.ST.op_Colon_Equals" ->
  