MavenRain

PageForge Privacy Policy

PageForge processes all PDF documents entirely on your device using WebAssembly. No document data, text content, or personal information is collected, transmitted, or stored on any server. The extension uses browser local storage solely to remember your UI preferences (such as summary length). No analytics, tracking, or third-party services are used.

Contact: pageforge@isurvivable.cv Last updated: 2026.03.28

MavenRain

How Cats Effect Uses Category Theory to Increase Programming Productivity

Cats Effect borrows a handful of category theory ideas and turns them into practical guardrails and building blocks for concurrent/effectful Scala code. Here's the gist:

The core trick: IO as a Monad

Side effects (network calls, file I/O, random numbers) are the enemy of composability. The IO type wraps these effects into inert descriptions of work. Because IO forms a monad, you get flatMap/for-comprehensions to sequence these descriptions like assembling Lego bricks. Nothing actually runs until you explicitly "interpret" the whole chain at the program's edge.

Productivity payoff: You can reason about, refactor, and test effectful code the same way you reason about pure functions. No hidden surprises.

MavenRain

Lean 4 Proof Export Backend for hevm: Technical Overview

The Idea in One Paragraph

hevm performs symbolic execution and SMT-based verification of smart contracts, but when it reports "no counterexample found," that result is bounded by path depth and solver timeout, and it produces no persistent artifact. This project builds a pipeline that captures hevm's symbolic execution traces, translates them into Lean 4 proof obligations, and (where possible) automatically generates machine-checked proofs. When full automation isn't feasible, it produces partial proof skeletons with explicit sorry gaps that a human can complete. The end result: hevm's output goes from "we searched and found no bugs" to "here is a machine-checked proof."

Architecture

The system has three layers, designed to minimize the footprint inside hevm itself:

MavenRain

impl Solution {
    pub fn compress(chars: &mut Vec<char>) -> i32 {
        use std::iter::{once, repeat};

        let n = chars.len();

        // Iterator that yields (char, length) for each group
        let groups = (0..n)
            .scan((Option::<char>::None, 0usize), |(prev, count), i| {
                let ch = chars[i];

MavenRain

module Main exposing (main)

import Html exposing (text)

import Array exposing (Array)

findAnagrams : String -> String -> List Int
findAnagrams s p =
    let
        toIdx c =

MavenRain

use std::array;

#[allow(dead_code)]
struct Solution;

impl Solution {
    #[allow(dead_code)]
    pub fn find_anagrams(s: String, p: String) -> Vec<i32> {
        fn build_freq(it: impl Iterator<Item = u8>) -> [i32; 26] {
            it.fold([0i32; 26], |acc, byte| {

MavenRain

module Main exposing (main)

import Html exposing (text)

type alias Max =
    Maybe Int

combine : Max -> Max -> Max
combine mx my =
    case ( mx, my ) of

MavenRain

struct Solution;
#[derive(Clone)]
enum StackNode {
    Empty,
    Cons {
        size: i32,
        prefix_max: i32,
        elem: i32,
        tail: Box<StackNode>,
    },

MavenRain

module Main exposing (main)

import Html exposing (text)

flip : (a -> b -> c) -> b -> a -> c
flip f =
    \x y -> f y x


scanl : (a -> b -> b) -> b -> List a -> List b

MavenRain

use std::iter::successors;

struct Solution;
impl Solution {
    pub fn product_except_self(nums: Vec<i32>) -> Vec<i32> {
        let n = nums.len();

        // Build left prefix products using successors (anamorphism)
        // State: (index, current_product)
        // Starts with product before first element (1), then multiplies successively