This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-------------------------- MODULE multi_user_wire -------------------------- | |
EXTENDS Integers, Sequences | |
CONSTANTS Users, Servers, Accounts | |
MAX_MONEY == 20 | |
AtMostOneAdminPerOrg(users, orgs) == {roles \in [users -> {"user","admin"}]: | |
\A x,y \in users: (roles[x] = "admin" /\ roles[y] = "admin") => x = y} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Rounding operations (efficient when n is a power of 2) | |
// Round down to the nearest multiple of n | |
#define ROUNDDOWN(a, n) \ | |
({ \ | |
uint32_t __a = (uint32_t) (a); \ | |
(typeof(a)) (__a - __a % (n)); \ | |
}) | |
// Round up to the nearest multiple of n | |
#define ROUNDUP(a, n) \ | |
({ \ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
private static class Vec { | |
int x, y; | |
public Vec(int x, int y) { this.x = x; this.y = y; } | |
public Vec add(Vec oth) { return new Vec(x+oth.x, y+oth.y); } | |
public Vec rot90CW() { return new Vec(y, -x); } | |
public int infDist(Vec oth) { return Math.max(x-oth.x, y-oth.y); } | |
public boolean equals.... | |
} | |
// Returns spiral pattern in a (2n+1) * (2n+1) array |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
/* Functionality: | |
* -- Activate pumps on moisture low | |
* -- If photoresistor low, and valid hours of day, then turn lights on for 10 minutes | |
* -- If water level low, then blink lights | |
*/ | |
#include <Wire.h> | |
#include <DS3231.h> | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// Before | |
xrContext.addToBindings(commonBindings, squeezeAction, "/input/squeeze/value"); | |
xrContext.addToBindings(commonBindings, triggerAction, "/input/trigger/value"); | |
xrContext.addToBindings(commonBindings, gripPoseAction, "/input/grip/pose"); | |
xrContext.addToBindings(commonBindings, aimPoseAction, "/input/aim/pose"); | |
xrContext.addToBindings(commonBindings, thumbstickAction, "/input/thumbstick"); | |
xrContext.addToBindings(commonBindings, thumbClickAction, "/input/thumbstick/click"); | |
xrContext.addToBindings(commonBindings, vibrateAction, "/output/haptic"); | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
generator int exp([int nvars, int nconsts], int bnd, int[nvars] vars, int[nconsts] consts){ | |
//In this generator, nvars is the number of variables and nconsts is the number of constants. | |
//the array vars contains the values of all the variables and the array consts of all the constants. | |
//Note that unlike problem 1, where you were generating ASTs, here you are synthesizing the actual function. | |
//Also note that you will probably need a separate generator for the boolean expressions. | |
if (bnd == 0) { | |
return {| vars[??] | consts[??] |}; | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Inductive val := | |
| ValConst (n : nat) | |
| Closure (e1 : list val) (e2 : exp) | |
with | |
exp := | |
| Var (v : var) | |
| Plus (e1 e2 : exp) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This is one of the simpler examples from a series of examples designed to be challenging to analyze by method of combining many featuress. | |
The goal of this analyzer is to verify the assertions. This example involves interplay between integer constraints and aliasing, and also requires models for the Urn functions. | |
------------------------------ | |
void func() { | |
Urn u1 = new Urn(); | |
Urn u2 = new Urn(); |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
void __thiscall army::Walk(army *ecx0, signed int dir, int last, int notFirst) | |
{ | |
int v4; // ST3C_4@78 | |
int v6; // [sp+1Ch] [bp-24h]@26 | |
int v7; // [sp+20h] [bp-20h]@80 | |
int i; // [sp+24h] [bp-1Ch]@47 | |
int v9; // [sp+28h] [bp-18h]@77 | |
signed int targCell; // [sp+30h] [bp-10h]@1 | |
int offsetY; // [sp+34h] [bp-Ch]@26 | |
int v12; // [sp+38h] [bp-8h]@26 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// SPDX-License-Identifier: AGPL-3.0-only | |
pragma solidity 0.8.19; | |
// External Libraries | |
import "solady/src/auth/Ownable.sol"; | |
import "openzeppelin-contracts-upgradeable/contracts/proxy/utils/Initializable.sol"; | |
import "openzeppelin-contracts-upgradeable/contracts/token/ERC20/IERC20Upgradeable.sol"; | |
import "openzeppelin-contracts/contracts/access/AccessControl.sol"; | |
import "openzeppelin-contracts-upgradeable/contracts/security/ReentrancyGuardUpgradeable.sol"; | |
// Interfaces |